Re: [Bug-glpk] glp_minisat1() issue

[Chris Matrakidis]

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