[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Bug-glpk] glp_minisat1() issue

From: Chris Matrakidis
Subject: [Bug-glpk] glp_minisat1() issue
Date: Fri, 20 Nov 2015 10:39:54 +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." 

The attached patch checks the return value of solver_addclause() and returns GLP_NOFEAS in case it is 0.

Best Regards,

Chris Matrakidis

Attachment: glp_minisat1.patch
Description: Binary data

reply via email to

[Prev in Thread] Current Thread [Next in Thread]