Solver raises assert in debug mode with some inputs

[marco-calautti]

Hi, sorry for disappearining. We are using EvalMaxSat with Cadical for our experiments, and we are using it in incremental mode.
In some cases, in debug mode I get the following error:

EvalMaxSAT/lib/EvalMaxSAT/src/EvalMaxSAT.h:393: bool EvalMaxSAT<SAT_SOLVER>::solve() [with SAT_SOLVER = Solver_cadical]: Assertion _cardToAdd.size() == 0' failed

In release mode the solver keeps working, but of course reports wrong optimal cost/solution.

I will try to come up with a small example to reproduce the issue, since I get this problem with some complex formulas.
Anyway, the error happens after a couple of iterative additions of hard and soft clauses

[marco-calautti]

This is the smallest example I could find. Unfortunately still has some hundreds of variables and clauses. You can find attached the initial CNF formula (which has only hard clauses), and then 3 iterations where I logged the hard and soft clauses we add: each iteration adds a single hard clause, and then a certain number of soft clauses of size 1 and weight 1 (essentially the hard clause + the soft clauses are a hard blocking clause, and one soft clause for each literal in the blocking clause).

At the third iteration, we obtain an optimum of 33, while the optimum should be 34 (by optimum I mean the sum of the weights of all soft clauses that are true). This is consistent with the semantics of the problem we are encoding, and also with the optimum we get using another incremental MaxSAT solver (UwrMaxSAT).

• The log starts with "Optimum found: 0" as this logs the first execution of the solver with the initial cnf which has no soft clauses.
• The added hard and soft clauses are all 0-terminated.
• strangely, this example does not make the solver crash in debug mode, but the optimum is again 1 less than the correct one, as in the crashing example.

I hope this would be helpful. We really would like to use EvalMaxSAT for our experiments, since it is generally faster for our problem w.r.t. UwrMaxSAT. So, if you could have a look, we would really appreciate it!

initial_cnf.txt
iterations_log.txt

[FlorentAvellaneda]

Thanks for reporting the bug.
I tried your example file on my side, but it seems to work fine. Are you using the latest committed version? And with the incremental mode (monMaxSat->setIncremental(true)) enabled?