Errors in the code

[AloneKami]

I believe there is an error with general_multi_level_opt and its related parts. The code fails to pass the Regression Suite tests for small examples under this year's new competition rules when the -no-scip parameter is used. I suspect that the error lies in lines 785-786. This section makes assumptions that lead to subsequent errors.

[AloneKami]

testSolver.py 2024 by Tobias Paxian; run with --help for more information.
Checks a list of wcnfs (with the expected o-value) if the solver runs without errors.

STARTING IN MSE 2024 --> the solver must return one of the following exit codes:
0 if it cannot find a solution satisfying the hard clauses or prove unsatisfiability.
10 if the solver finds a solution satisfying the hard clauses but does not prove it to be unsatisfiabe.
20 if it finds that the hard clauses are unsatisfiable.
30 if it finds an optimal solution.

Skipping files due to: upper_bound_violation: 30;

Start searching in 249 instances for issues.

COUNTER: [238/249], next: MSE22Unique/9d81041e30889b71e2df4bab7f16970a4c3a2b0849de3ba81b414aadaa7d9968.wcnf

ERROR DETECTED:
	Solver claims OPTIMUM FOUND but model-value==o-value=7 represent a different value than the certified solution 6.

Solver call to reproduce error: 
	./uwrmaxsat -v0 -no-bin -no-sat -m -bm /home/wyy/psw/MaxSATRegressionSuite/MSE22Unique/9d81041e30889b71e2df4bab7f16970a4c3a2b0849de3ba81b414aadaa7d9968.wcnf

Overall Evaluation:
Found Errors in 1/249 instances:
Solver claims OPTIMUM FOUND but model-value and o-value represent a different value than the certified optimum.: 1
Found Issues in 2/249 instances:
exit code 0 --> should be 30 (new MSE24 rules), as solver claims OPTIMUM FOUND.: 2

Total runtime of script: 7.35s

[marekpiotrow]

Hi,

I have just pushed my recent commits. They contain a fix to the problem found by testSolver.py. The change is in lines 597-607 of MsSolver.cc. The exit codes are also modified as required by the new MSE2024 rules.

Best regards,

Marek

[marekpiotrow]

Hi,

after running testSolver.py with different parameters I found a few other problems with the code and pushed a fix to them.

Regards,

Marek

[AloneKami]

normalized-par16-1-c.opb.zip
When using the CaDiCaL solver as the SAT solver for this PBO example, if SCIP is used in conjunction, SCIP returns incorrect results. However, if SCIP is not used, the correct results are obtained. Why might this be happening?

[marekpiotrow]

The function setFrozen in CadicalWrap.h has to be fixed and really freeze variables in CaDiCaL.

I have already commited the fix.

Best regards,
Marek

[AloneKami]

I hope this message finds you well.

I have identified a small bug in the SCIP checker within the solver that is relatively straightforward to fix. The issue lies in the condition:
UB_goalval * goal_gcd < Int(uint64_t(1) << std::numeric_limits::digits - 4).

In reality, if all soft clause weights are negative, this condition is inevitably met because UB_goalval += fixed_goalval. Consequently, when all soft clause weights are negative, precision problems may arise, and if dealing with large integers, it can lead to errors.

Additionally, I've encountered another issue. While reading the PBO file, if the memory usage exceeds the limit, it results in misalignment without ending the output correctly, meaning it does not output "UNKNOWN".

Could you please provide guidance on how to address these issues?

[AloneKami]

I'm glad you were able to respond to me promptly before. The issue with negative weights for soft clauses in SCIP is relatively easy to improve. Since I am currently working on a PBO problem, I noticed that the new version of the PBO example has added two parameters in the first line. You can refer to the example I provided in my previous question. One parameter is "equal," which indicates how many constraints there are with the "=" sign. The other parameter is "intsize," which represents the number of bits in the binary representation of the sum of the absolute values of all coefficients. This parameter should be quite helpful in addressing this bug in PBO problems.

[AloneKami]

Dear Marek,

I hope this email finds you well.

I am writing to report a bug I encountered while using Cadical for solving problems. The issue arises during the binary search process. Specifically, the line of code:

bool clear_assump = (cnt * 3 >= assump_ps.size());
use_base_assump = clear_assump;

This can cause use_base_assump to become true. As a result, after initiating a new round of SAT solving, the code executes:

addUnitClause(base_assump[i]);

If the solver returns a SAT result while using Cadical, it triggers:

solver->add(lit2val(p));

When Cadical executes the add function, it performs a transition_to_steady_state() call, changing the state to steady. Consequently, when subsequently calling sat_solver.modelValue(x), Cadical expects the state to be SATISFIED:

REQUIRE(state() == SATISFIED, "can only get value in satisfied state");

This results in the following error message:

cadical: fatal error: invalid API usage of 'int CaDiCaL::Solver::val(int)' in '/mnt/e/product/c/UwrMaxSat/cadical/src/solver.cpp': can only get value in satisfied state.

I hope this information helps in identifying and fixing the bug. Please let me know if you need any further details or if there is anything else I can assist with.

Best regards,
Shiwei Pan

[marekpiotrow]

I hope I have fixed the problems you described. I have just started my holidays, so I have no spare time to test them well.

Best regards,
Marek