> > glp_minisat1() calls minisat's solver_addclause() with an assert. This is > unnecessarily restrictive, since according to the "An Extensible > SAT-solver" paper ( http://minisat.se/downloads/MiniSat.pdf ) "Trivial > conflicts ... can be detected by AddClause(), in which case it returns > FALSE." >
I found the log file from the run where I first noticed the issue and created the minimal test case attached. The problem obviously has no solution, but running: glpsol --minisat --lp test.lp ends with the assertion because solver_addclause() returns 0, while with the patch from the previous email it works correctly. Best Regards, Chris Matrakidis
test.lp
Description: Binary data
_______________________________________________ Bug-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/bug-glpk
