SEGFAULT on conflict analysis when using IPASIR-UP API

[idan0610]

Hello,

We are working on integrating CDCL into the Marabou DNN verification framework (https://arxiv.org/abs/2401.14461), while using CaDiCaL as the backend SAT solver, by implementing the IPASIR-UP API, as explained in (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.8)

When using CaDiCaL, we noticed that occasionally it throws SEGFAULT in file src/analyze.cpp, line 227 (method Internal::bump_clause()):

225    inline void Internal::bump_clause (Clause *c) {
226      LOG (c, "bumping");
227      unsigned used = c->used; // <- Segmentation Fault happens here
228      c->used = 1;

It seems to us that this happens when CaDiCaL is analyzing conflicts, specifically after detecting that the UIP is the current decision literal, and thus has no reason clause. This led us to believe that we might be using CaDiCaL not as intended, or alternatively that it contains a bug. We would be glad if you can help understand the cause of this error, and whether it originates in faulty clauses added to CaDiCaL externally.

We attach below the full CaDiCaL log that exemplifies this SEGFAULT error. cadical_log.txt

[m-fleury]

Thanks for the small log file!

c LOG 2 API call 'vars ()' started
c LOG 2 API call 'vars ()' returns '19'
c LOG 2 search assign -4 @ 2 irredundant size 0 clause[0]
c LOG 2 notify external propagator about new assignments
c LOG 2 propagating -4
c ----------------------------------------------------------------------------
c LOG 2 API call 'vars ()' started
c LOG 2 API call 'vars ()' returns '19'
c LOG 2 search assign 15 @ 2 irredundant size 0 clause[0]
c LOG 2 notify external propagator about new assignments
c LOG 2 propagating 15
...
c LOG 2 new pointer 0x55555614e730 irredundant size 5 clause[8] 15 -18 -17 -16 10
...
c LOG 2 new pointer 0x555556152670 irredundant size 7 clause[10] 8 -18 -17 -16 -15 4 10
...
c LOG 2 analyzing 15 reason irredundant size 5 clause[7] 15 -18 -17 -16 10
...
c LOG 2 analyzing -4 reason irredundant size 6 clause[10] -4 -18 -17 -16 -15 10

The clause [10] 8 -18 -17 -16 -15 4 10 is not propagating 4, because -15 is not set yet (it is only set later). So you need to set -15 before 4.

In technical terms: The reason for the literal 4 depends on literal 15 which is set later, breaking the topological ordering on the trail. When setting a literal, the reason is only allowed to reference literals set earlier, not some set later.

@kfazekas could we add a check a debug mode, that for all literals in the reason var(lit).trail <= var(propagated_ilit).trail (in learn_external_reason_clause)?

[kfazekas]

Thank for the finding @idan0610!

@m-fleury: sure, good idea, I will add more checks to the most recent version before merge.