CaDiCaL usage for Incremental BMC

[genkrpzh]

Hi,

I am currently developing a tiny hardware bounded model checker and have some questions regarding the use of CaDiCaL for this specific purpose.

At the moment, I am encountering an issue that I believe stems from my misuse of CaDiCaL. Some of the counterexample traces returned when I use CaDiCaL as the backend are invalid, whereas this does not happen when I use PicoSAT.

My current approach is to add the clauses corresponding to the transition relation to the solver incrementally using the add method, clause by clause, at each model checking step. From my understanding, the problem arises because CaDiCaL internally simplifies the states more aggressively than I expect after adding each clause within the same step (and also more than PicoSAT). I have tried to control or block this simplification using various combinations of settings and configurations, but I have not been able to prevent the generation of spurious counterexample traces.

What I would like to achieve is to temporarily disable simplification/elimination when adding clauses related to the same step, and then re-enable it just before checking for satisfiability. However, I have not found the right combination of options or commands to do this.

Do you have any advice on using CaDiCaL in this context?

Best, and thanks a lot for maintaining this tool :) !

Félix

[Froleyks]

Just a wild guess, BVA generated variables are tripping him up.

…

On Wed, Sep 10, 2025, 14:06 Félix Ridoux ***@***.***> wrote: Hi, I am currently developing a tiny hardware bounded model checker and have some questions regarding the use of CaDiCaL for this specific purpose. At the moment, I am encountering an issue that I believe stems from my misuse of CaDiCaL. Some of the counterexample traces returned when I use CaDiCaL as the backend are invalid, whereas this does not happen when I use PicoSAT. My current approach is to add the clauses corresponding to the transition relation to the solver incrementally using the add method, clause by clause, at each model checking step. From my understanding, the problem arises because CaDiCaL internally simplifies the states more aggressively than I expect after adding each clause within the same step (and also more than PicoSAT). I have tried to control or block this simplification using various combinations of settings and configurations, but I have not been able to prevent the generation of spurious counterexample traces. What I would like to achieve is to temporarily disable simplification/elimination when adding clauses related to the same step, and then re-enable it just before checking for satisfiability. However, I have not found the right combination of options or commands to do this. Do you have any advice on using CaDiCaL in this context? Best, and thanks a lot for maintaining this tool :) ! Félix — Reply to this email directly, view it on GitHub <#142>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACF2LLR7QYHH4IFJKBQ746D3SAH55AVCNFSM6AAAAACGEAYB2WVHI2DSMVQWIX3LMV43ERDJONRXK43TNFXW4OZYHA3TMMBXGQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[genkrpzh]

Thanks for your reply! Do you know if there is any way to disable BVA to test this hypothesis? I haven’t been able to find any related option in options.hpp.

Best,

Félix

[m-fleury]

The option is called factor.

[m-fleury]

That being said incorrect factor use would lead to contract violation, not incorrect counter examples.

My guess is that your encoding is wrong, but it only triggers with rephasing, which picosat does not have.

[genkrpzh]

Okay, thanks a lot for your suggestions, I will have a look !

Best,

Félix

[m-fleury]

Oh and BVA is only implemented in 2.2-rc2, not in the 2.1 release.

[Froleyks]

It's called "factor" in cadical.

…

On Wed, Sep 10, 2025, 15:22 Félix Ridoux ***@***.***> wrote: Thanks for your reply! Do you know if there is any way to disable BVA to test this hypothesis? I haven’t been able to find any related option in options.hpp. Best, Félix — Reply to this email directly, view it on GitHub <#142 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACF2LLS6HRGMNTJDRAY3ML33SAQYXAVCNFSM6AAAAACGEAYB2WVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTIMZWGI4TMNA> . You are receiving this because you commented.Message ID: ***@***.***>