Andrew, 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."
The attached patch checks the return value of solver_addclause() and returns GLP_NOFEAS in case it is 0. Best Regards, Chris Matrakidis
glp_minisat1.patch
Description: Binary data
_______________________________________________ Bug-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/bug-glpk
