|
From: | Chris Matrakidis |
Subject: | Re: [Bug-glpk] glp_minisat1() issue |
Date: | Wed, 25 Nov 2015 21:57:31 +0200 |
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."
test.lp
Description: Binary data
[Prev in Thread] | Current Thread | [Next in Thread] |