sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/issues2020-05-07T08:02:15Zhttps://gitlab.ow2.org/sat4j/sat4j/issues/161Bug with the CuttingPlanes strategy2020-05-07T08:02:15ZJo DevriendtBug with the CuttingPlanes strategyIn the latest commit (94b8f65350e7e365cf2ed64666adc5b67136776c), the attached pseudo-Boolean (PB) instance from the PB competition is solved as satisfiable with the "CuttingPlanes" strategy. I'm reasonably sure the instance is unsatisfiable, which is confirmed by Sat4J's default configuration (without "CuttingPlanes" strategy).
[uclid_pb_benchmarks_normalized-43s.smv.opb](/uploads/77bd9969739e32bd9e863d7b2cb3f565/uclid_pb_benchmarks_normalized-43s.smv.opb)In the latest commit (94b8f65350e7e365cf2ed64666adc5b67136776c), the attached pseudo-Boolean (PB) instance from the PB competition is solved as satisfiable with the "CuttingPlanes" strategy. I'm reasonably sure the instance is unsatisfiable, which is confirmed by Sat4J's default configuration (without "CuttingPlanes" strategy).
[uclid_pb_benchmarks_normalized-43s.smv.opb](/uploads/77bd9969739e32bd9e863d7b2cb3f565/uclid_pb_benchmarks_normalized-43s.smv.opb)https://gitlab.ow2.org/sat4j/sat4j/issues/157IBB removes blocking constraint2019-10-16T12:18:37ZJonas Bollgrünapothecarius@web.deIBB removes blocking constraintThe IBB algorithm to compute Backbones (org.sat4j.core/src/main/java/org/sat4j/tools/Backbone.java) removes it's blocking constraint in every iteration (Line 214) which leads to the learned clauses being flushed indirectly.
Without the line, the next blocking clause would subsume the previous one, so I *think* that that line is unnecessary.
Otherwise, is there a unit test case where flushing learned clauses is required to not induce invalid backbone literals.The IBB algorithm to compute Backbones (org.sat4j.core/src/main/java/org/sat4j/tools/Backbone.java) removes it's blocking constraint in every iteration (Line 214) which leads to the learned clauses being flushed indirectly.
Without the line, the next blocking clause would subsume the previous one, so I *think* that that line is unnecessary.
Otherwise, is there a unit test case where flushing learned clauses is required to not induce invalid backbone literals.https://gitlab.ow2.org/sat4j/sat4j/issues/154Sat4j cannot be built using maven 3.6.02019-01-28T12:27:27ZDaniel Le BerreSat4j cannot be built using maven 3.6.0When compiling current code of Sat4j using maven 3.6.0, the following error occurs:
```
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-javadoc-plugin:3.0.0-M1:jar (attach-javadocs) on project org.ow2.sat4j.core: Execution attach-javadocs of goal org.apache.maven.plugins:maven-javadoc-plugin:3.0.0-M1:jar failed.: NullPointerException -> [Help 1]
```When compiling current code of Sat4j using maven 3.6.0, the following error occurs:
```
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-javadoc-plugin:3.0.0-M1:jar (attach-javadocs) on project org.ow2.sat4j.core: Execution attach-javadocs of goal org.apache.maven.plugins:maven-javadoc-plugin:3.0.0-M1:jar failed.: NullPointerException -> [Help 1]
```https://gitlab.ow2.org/sat4j/sat4j/issues/152Degradation in OPB solver from 2.3.5 to current version2018-12-15T21:28:32ZMiguel NevesDegradation in OPB solver from 2.3.5 to current versionHi Daniel,
I am observing a performance degradation from version 2.3.5 to the current version in my particular application.
Find attached 2 .opb files (test.opb and test2.opb) for which the degradation is evident.
- test.opb: solved by 2.3.5 in 5 seconds, current version requires more than 4 minutes.
- test2.opb: solved by 2.3.5 in less than 8 minutes, current version failed to solve it in 2 hours.
[test.opb](/uploads/2588bbb5b8a6e8cfe3595ac764f3b074/test.opb)
[test2.opb](/uploads/f41f62a73d6a73fda78f13b0f176b4e2/test2.opb)
I can provide more examples like these if desired.
Best regards,
Miguel NevesHi Daniel,
I am observing a performance degradation from version 2.3.5 to the current version in my particular application.
Find attached 2 .opb files (test.opb and test2.opb) for which the degradation is evident.
- test.opb: solved by 2.3.5 in 5 seconds, current version requires more than 4 minutes.
- test2.opb: solved by 2.3.5 in less than 8 minutes, current version failed to solve it in 2 hours.
[test.opb](/uploads/2588bbb5b8a6e8cfe3595ac764f3b074/test.opb)
[test2.opb](/uploads/f41f62a73d6a73fda78f13b0f176b4e2/test2.opb)
I can provide more examples like these if desired.
Best regards,
Miguel Neveshttps://gitlab.ow2.org/sat4j/sat4j/issues/151Map returned by getStat() is empty2018-12-07T19:19:33ZMiguel NevesMap returned by getStat() is emptyHello Daniel,
Title is self explanatory. Here is an example program that replicates the bug.
```
import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
public class EmptyStatsBug {
public static void main(String[] args) throws ContradictionException, TimeoutException {
IVecInt lits = new VecInt(new int[] { 1, 2, 3 });
IVec<BigInteger> coeffs = new Vec<BigInteger>(new BigInteger[] {
BigInteger.ONE,
BigInteger.ONE,
BigInteger.ONE
});
IPBSolver solver = SolverFactory.newDefault();
solver.newVar(3);
IConstr constr = null;
solver.addAtMost(lits, 2);
System.out.println(solver.getStat().keySet().size());
solver.isSatisfiable();
System.out.println(solver.getStat().keySet().size());
}
}
```
The above program produces the following output:
```
0
0
```
Best regards,
Miguel NevesHello Daniel,
Title is self explanatory. Here is an example program that replicates the bug.
```
import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
public class EmptyStatsBug {
public static void main(String[] args) throws ContradictionException, TimeoutException {
IVecInt lits = new VecInt(new int[] { 1, 2, 3 });
IVec<BigInteger> coeffs = new Vec<BigInteger>(new BigInteger[] {
BigInteger.ONE,
BigInteger.ONE,
BigInteger.ONE
});
IPBSolver solver = SolverFactory.newDefault();
solver.newVar(3);
IConstr constr = null;
solver.addAtMost(lits, 2);
System.out.println(solver.getStat().keySet().size());
solver.isSatisfiable();
System.out.println(solver.getStat().keySet().size());
}
}
```
The above program produces the following output:
```
0
0
```
Best regards,
Miguel Neveshttps://gitlab.ow2.org/sat4j/sat4j/issues/147Rare NullPointerException with time based timeout2018-11-12T15:03:36ZMiguel NevesRare NullPointerException with time based timeoutHi Daniel,
It's quite rare, but sometimes I get a NullPointerException at line 1782 of Solver.java when solving a large sequence of easy formulas and using time based timeouts. Possibly a race condition with line 1831?
Best regards,
Miguel NevesHi Daniel,
It's quite rare, but sometimes I get a NullPointerException at line 1782 of Solver.java when solving a large sequence of easy formulas and using time based timeouts. Possibly a race condition with line 1831?
Best regards,
Miguel Neveshttps://gitlab.ow2.org/sat4j/sat4j/issues/145ParseInstance does not work properly on Windows2018-11-10T12:41:35ZDaniel Le BerreParseInstance does not work properly on WindowsThe following issue was reported by Tobias Barth by email:
The class "org.sat4j.reader.InstanceReader" is not compatible with Windows fully qualified path names. On my machine, they start with "C:", and the method "parseInstance" in class InstanceReader, line 108, splits a String like "EZCNF:C:\projects\bla\testcomments.cnf" into "EZCNF", "C" and "\projects\bla\testcomments.cnf", but uses "C" as filename. I suggest you add a splitting limit to line 108:
String[] parts = filename.split(":", 2);
This will split only at the first ":".The following issue was reported by Tobias Barth by email:
The class "org.sat4j.reader.InstanceReader" is not compatible with Windows fully qualified path names. On my machine, they start with "C:", and the method "parseInstance" in class InstanceReader, line 108, splits a String like "EZCNF:C:\projects\bla\testcomments.cnf" into "EZCNF", "C" and "\projects\bla\testcomments.cnf", but uses "C" as filename. I suggest you add a splitting limit to line 108:
String[] parts = filename.split(":", 2);
This will split only at the first ":".Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/issues/144Issue when removing unit propagated literals with a PB constraint2018-11-12T15:04:15ZDaniel Le BerreIssue when removing unit propagated literals with a PB constraintIt looks like adding a constraint which propagates it's literals (e.g. x1+x2+2*x3>=4) then the constraint cannot be removed.
The issue was reported by Vasco Manquinho's team.It looks like adding a constraint which propagates it's literals (e.g. x1+x2+2*x3>=4) then the constraint cannot be removed.
The issue was reported by Vasco Manquinho's team.https://gitlab.ow2.org/sat4j/sat4j/issues/143A link is down on website2018-09-16T15:06:44ZThIbault FalqueA link is down on websiteHi,
The link of SAT4J@Objectweb is down in the documentation text.
http://www.sat4j.org/doc.phpHi,
The link of SAT4J@Objectweb is down in the documentation text.
http://www.sat4j.org/doc.phphttps://gitlab.ow2.org/sat4j/sat4j/issues/2Allow iteration on MUS2018-05-11T12:15:13ZDaniel Le BerreAllow iteration on MUSOne new feature of release 2.3.0 is to compute minimal unsatisfiable subformulas. It is currently possible to compute on MUS. In some cases, it would make sense to compute all of them.
One specific iterator is needed for that purpose. One new feature of release 2.3.0 is to compute minimal unsatisfiable subformulas. It is currently possible to compute on MUS. In some cases, it would make sense to compute all of them.
One specific iterator is needed for that purpose. https://gitlab.ow2.org/sat4j/sat4j/issues/3Allow computation of prime implicants instead of models2018-05-11T12:15:13ZDaniel Le BerreAllow computation of prime implicants instead of modelsThe solver currently returns a model, i.e. a complete assignment of the boolean variables of the problem, that satisfies the constraints.
In some cases, a partial assignment that satisfies those constraints is needed (i.e. a prime implicant).
Providing a utility class that computes a prime implicant from a model could be a good way to provide that new feature to end users.The solver currently returns a model, i.e. a complete assignment of the boolean variables of the problem, that satisfies the constraints.
In some cases, a partial assignment that satisfies those constraints is needed (i.e. a prime implicant).
Providing a utility class that computes a prime implicant from a model could be a good way to provide that new feature to end users.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/4Provide a representation of pseudo boolean constraints with primitive type lo...2018-05-11T12:15:13ZDaniel Le BerreProvide a representation of pseudo boolean constraints with primitive type long instead of BigIntegerPseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those constraints, to efficiently propagate truth values.
One could choose either int or long for that.
long is probably a good tradeoff between the space required to store the information and the number of cases in which it will apply. Since we are going to 64 bits arch, long should be handled natively by the JVMs at some point.Pseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those constraints, to efficiently propagate truth values.
One could choose either int or long for that.
long is probably a good tradeoff between the space required to store the information and the number of cases in which it will apply. Since we are going to 64 bits arch, long should be handled natively by the JVMs at some point.2.3.0https://gitlab.ow2.org/sat4j/sat4j/issues/5Global timeout not properly taken into account when optimizing solutions2018-05-11T12:15:13ZDaniel Le BerreGlobal timeout not properly taken into account when optimizing solutionsWhen optimizing a solution, the timeout should be global, not for each call to the issatisfiable() method.
This is taken into account thanks to the boolean parameter global in isSatisfiable(). If it is true, the timeout will not be reset at each time.
It looks like a problem appears when optimizing Eclipse solutions:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=336967
When optimizing a solution, the timeout should be global, not for each call to the issatisfiable() method.
This is taken into account thanks to the boolean parameter global in isSatisfiable(). If it is true, the timeout will not be reset at each time.
It looks like a problem appears when optimizing Eclipse solutions:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=336967
2.3.0https://gitlab.ow2.org/sat4j/sat4j/issues/7Allow the addition of soft cardinality constraints2018-05-11T12:15:13ZDaniel Le BerreAllow the addition of soft cardinality constraintsThe MaxSat decorator allows the user to add hard and soft clauses. It also allows the user to add hard cardinality constraints.
To be complete, it would be nice to have also the possibility to add soft cardinality constraints:
http://forge.ow2.org/forum/message.php?msg_id=24229The MaxSat decorator allows the user to add hard and soft clauses. It also allows the user to add hard cardinality constraints.
To be complete, it would be nice to have also the possibility to add soft cardinality constraints:
http://forge.ow2.org/forum/message.php?msg_id=242292.3.0https://gitlab.ow2.org/sat4j/sat4j/issues/8Allow iterating over optimal solutions2018-05-11T12:15:13ZDaniel Le BerreAllow iterating over optimal solutionsThe solver is not properly cleaned up once an optimal solution is found.
Literals propagated at decision level 0 by pseudo boolean constraints used during the optimization are not properly removed.
While this does not affect our major tools (PB or MAXSAT solvers) since they aim only at finding one optimal solution, it is an issue when one wants to find several optimal solutions. See TestLonca to see the problem in action.The solver is not properly cleaned up once an optimal solution is found.
Literals propagated at decision level 0 by pseudo boolean constraints used during the optimization are not properly removed.
While this does not affect our major tools (PB or MAXSAT solvers) since they aim only at finding one optimal solution, it is an issue when one wants to find several optimal solutions. See TestLonca to see the problem in action.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/9Trivial inconsistency in cardinality constraints not properly handled2018-05-11T12:15:13ZDaniel Le BerreTrivial inconsistency in cardinality constraints not properly handledWhen doing optimization with cardinality constraints (at least), at some point the degree of the constraint is strictly bigger than the number of literals in the constraints. In that case, the constraint cannot be satisfied:
x& + x2 + x3 >= 4 cannot be satisfied.
As such, sat4j should throw a ContradictionException when that constraint is created.
While it is the case in the AtLeast implementation of the card constraint, it is not the case for MaxWatchPb and MinWatchPb. When doing optimization with cardinality constraints (at least), at some point the degree of the constraint is strictly bigger than the number of literals in the constraints. In that case, the constraint cannot be satisfied:
x& + x2 + x3 >= 4 cannot be satisfied.
As such, sat4j should throw a ContradictionException when that constraint is created.
While it is the case in the AtLeast implementation of the card constraint, it is not the case for MaxWatchPb and MinWatchPb. 2.3.0https://gitlab.ow2.org/sat4j/sat4j/issues/10allow ability to clone a solver2018-05-11T12:15:13Zemmanuel lonca emmanuel loncaallow ability to clone a solverneed to clone a solver to launch multiple instances of a solver to compute best utility on some optimization function for a single optimization problemneed to clone a solver to launch multiple instances of a solver to compute best utility on some optimization function for a single optimization problem2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/11Allow creation of ManyCore solver from a list/array of existing solvers inste...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of ManyCore solver from a list/array of existing solvers instead of their name in a factoryIt is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.It is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/12Use List instead of IVec in DependencyHelper.getSolution()2018-05-11T12:15:13ZDaniel Le BerreUse List instead of IVec in DependencyHelper.getSolution()Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to interact with that class.
We could use for instance a java.util.List object instead of an IVec.
The main issue here is that it would break the API: the DependencyHelper class exists since Sat4j 2.1.
Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to interact with that class.
We could use for instance a java.util.List object instead of an IVec.
The main issue here is that it would break the API: the DependencyHelper class exists since Sat4j 2.1.
2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/13Compute minimal size unsat core2018-05-11T12:15:13ZDaniel Le BerreCompute minimal size unsat coreIt is currently possible to compute subset minimal unsat cores.
Some users would like to compute a size minimal unsat core.
It should not be too difficult to implement: just another strategy for the Xplain class.It is currently possible to compute subset minimal unsat cores.
Some users would like to compute a size minimal unsat core.
It should not be too difficult to implement: just another strategy for the Xplain class.2.3.3