Incorrect explanations in PB
When forgetting to call newVar, explanations become wrong, since clauses are being added with wrong explanation keys.
A more user-friendly solution would be to throw an exception when adding a clause with undeclared variables, instead of silently accepting the clause and returning incorrect results afterwards.
Here is a working example:
package test;
import org.sat4j.core.VecInt; import org.sat4j.specs.ContradictionException; import org.sat4j.specs.IVecInt; import org.sat4j.pb.IPBSolver; import org.sat4j.pb.SolverFactory; import org.sat4j.pb.tools.XplainPB; import org.sat4j.tools.xplain.Xplain;
class Test { public static void main(String[] args) throws ContradictionException { Xplain solver = new XplainPB(SolverFactory.newDefault()); IVecInt clause = new VecInt(); clause.push(-1).push(-2); System.out.println("adding clause " + clause.toString()); solver.addClause(clause); System.out.println("clause added as " + clause.toString()); } }
The output of this program is as following:
adding clause -1,-2 clause added as -1,-2,1
Here, literal "1" was used as an explanation key, which conflicts with the variable used in the clause.
A workaround for the wrong explanations is to never forget to call newVar for all variables before adding any clauses.