|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."
Description: Binary data
|[Prev in Thread]||Current Thread||[Next in Thread]|