sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2019-01-28T12:27:27Zhttps://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...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/153Bug when mixing constraint removal and constraints satisfied by unit propagation2019-01-27T15:32:36ZMiguel NevesBug when mixing constraint removal and constraints satisfied by unit propagationHi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation.
In particular, the bug is triggered by the following sequence of operations:
- add constra...Hi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation.
In particular, the bug is triggered by the following sequence of operations:
- add constraints (x1 + x2 + x3 <= 2), (x1 + x2 >= 2) and (not(x2) v not(x3))
- check satisfiability: formula is SAT, as expected
- remove (x1 + x2 >= 2)
- add (x2 + x3 >= 2): this should contradict (not(x2) v not(x3)), but no exception is thrown
- check satisfiability: formula should be UNSAT, but SAT is returned instead
I have attached a small Java program that follows this sequence of operations, triggering the bug.
Best regards,
Miguel Neves
[SatByUnitBug.java](/uploads/f36125668baadf4011b0cf998bac3a42/SatByUnitBug.java)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...Hi 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 empty2021-10-06T01:02:17ZMiguel 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....Hello 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/150Update code base to Java 72018-11-13T06:56:33ZDaniel Le BerreUpdate code base to Java 7The original source code of Sat4j was Java 1.5 down compiled to 1.4.
The 2.3.6 release will be compatible with Java 7.
As such, new syntactic structures are available (try with resources, multiple exceptions).
We need to take care pro...The original source code of Sat4j was Java 1.5 down compiled to 1.4.
The 2.3.6 release will be compatible with Java 7.
As such, new syntactic structures are available (try with resources, multiple exceptions).
We need to take care properly of that.
SonarQube can help us for that.2.3.6Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/149Instability of timeout based tests2018-11-10T11:03:13ZDaniel Le BerreInstability of timeout based testsIt is painful to have timeout based tests failing from time to time, breaking builds while there is no problem.
Just occurred today in https://gitlab.ow2.org/sat4j/sat4j/-/jobs/8082
We need to either find out why those tests do not take...It is painful to have timeout based tests failing from time to time, breaking builds while there is no problem.
Just occurred today in https://gitlab.ow2.org/sat4j/sat4j/-/jobs/8082
We need to either find out why those tests do not take consistently the same time or get rid off the timeout!https://gitlab.ow2.org/sat4j/sat4j/-/issues/148ArrayIndexOutOfBound exception on non normalized WBO opb file2018-10-29T16:44:23ZDaniel Le BerreArrayIndexOutOfBound exception on non normalized WBO opb fileIn WBO, non normalized constraints cause an ArrayIndexOutOfBoundsException:
```
java -jar dist/CUSTOM/sat4j-pb.jar CuttingPlanes ~/Downloads/bugpourevocrash2.opb
```
```
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsExcepti...In WBO, non normalized constraints cause an ArrayIndexOutOfBoundsException:
```
java -jar dist/CUSTOM/sat4j-pb.jar CuttingPlanes ~/Downloads/bugpourevocrash2.opb
```
```
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 6
at org.sat4j.core.Vec.get(Vec.java:239)
at org.sat4j.pb.constraints.pb.InternalMapPBStructure.get(InternalMapPBStructure.java:102)
at org.sat4j.pb.constraints.pb.ConflictMap.isImplyingLiteral(ConflictMap.java:621)
at org.sat4j.pb.constraints.pb.ConflictMap.isAssertive(ConflictMap.java:583)
at org.sat4j.pb.core.PBSolverCP.analyzeCP(PBSolverCP.java:141)
at org.sat4j.pb.core.PBSolverCP.analyze(PBSolverCP.java:129)
at org.sat4j.minisat.core.Solver.search(Solver.java:1320)
at org.sat4j.minisat.core.Solver.isSatisfiable(Solver.java:1824)
at org.sat4j.tools.SolverDecorator.isSatisfiable(SolverDecorator.java:115)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:179)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:172)
at org.sat4j.OptimizationMode.solve(OptimizationMode.java:121)
at org.sat4j.AbstractLauncher.solve(AbstractLauncher.java:318)
at org.sat4j.AbstractLauncher.run(AbstractLauncher.java:257)
at org.sat4j.pb.LanceurPseudo2007.main(LanceurPseudo2007.java:97)
```
[bugpourevocrash.opb](/uploads/3a9ca6ffde44f1a136d337ba86ded8c5/bugpourevocrash.opb)https://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,...Hi 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/146ModelIteratorTest.testGlobalTimeoutCounter makes build instable2018-09-16T14:55:52ZDaniel Le BerreModelIteratorTest.testGlobalTimeoutCounter makes build instableThe test case ModelIteratorTest.testGlobalTimeoutCounter uses a timeout, which makes the test fail if it is reached.
The issue is that such timeout may be reached depending of the load of the computer running the tests.
So the same cod...The test case ModelIteratorTest.testGlobalTimeoutCounter uses a timeout, which makes the test fail if it is reached.
The issue is that such timeout may be reached depending of the load of the computer running the tests.
So the same code may pass or not pass the tests depending of the load of the runner ...https://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 cla...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/142Java 9 modularization?2022-03-09T14:39:30ZMark RaynsfordJava 9 modularization?Hello.
Are there any plans to modularize `sat4j` as Java 9 modules?Hello.
Are there any plans to modularize `sat4j` as Java 9 modules?3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/1Use a specific data structure for binary clauses compatible with reason simpl...2018-05-11T12:15:13ZDaniel Le BerreUse a specific data structure for binary clauses compatible with reason simplificationThe support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because th...The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.https://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 impli...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 const...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 rese...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/6Allow iterating over all prime impliquants2018-05-11T12:15:13ZDaniel Le BerreAllow iterating over all prime impliquantsissue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover...issue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover, not all prime implicants.
something specific need to be implemented for that task.https://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://fo...The 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.0