[Top][All Lists]

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

Re: [Bug-glpk] glp_minisat1() issue

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." 

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

Attachment: test.lp
Description: Binary data

reply via email to

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