sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2021-09-26T19:04:49Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/168Compatibility issues with Maven 3.8.12021-09-26T19:04:49ZRomain WALLONCompatibility issues with Maven 3.8.1When running the tests of Sat4j with Maven 3.8.1, the build fails because some dependencies are not resolved:
```
Failed to execute goal on project org.ow2.sat4j.sat:
Could not resolve dependencies for project org.ow2.sat4j:org.ow2.sat4...When running the tests of Sat4j with Maven 3.8.1, the build fails because some dependencies are not resolved:
```
Failed to execute goal on project org.ow2.sat4j.sat:
Could not resolve dependencies for project org.ow2.sat4j:org.ow2.sat4j.sat:jar:3.0.0-SNAPSHOT:
Failed to collect dependencies at org.ow2.sat4j:org.ow2.sat4j.core:jar:3.0.0-SNAPSHOT:
Failed to read artifact descriptor for org.ow2.sat4j:org.ow2.sat4j.core:jar:3.0.0-SNAPSHOT:
Could not transfer artifact org.ow2.sat4j:org.ow2.sat4j.pom:pom:3.0.0-SNAPSHOT from/to maven-default-http-blocker (http://0.0.0.0/):
Blocked mirror for repositories: [ow2-snapshot (http://repository.ow2.org/nexus/content/repositories/snapshots, default, snapshots)]
```
It seems that this is because [Maven no longer allows the use of HTTP for repositories](https://maven.apache.org/docs/3.8.1/release-notes.html#how-to-fix-when-i-get-a-http-repository-blocked).
@leberre, do you know whether it is possible to use HTTPS for the `ow2-snapshot` repository, and how to configure Maven accordingly?
**Important remark**:
The issue only occurs if the dependencies have never been downloaded with a previous version of Maven, as they would have been cached in this case.https://gitlab.ow2.org/sat4j/sat4j/-/issues/164learnt literals not displayed in prime implicants using org.sat4j.core.jar co...2021-03-02T07:13:32ZDaniel Le Berrelearnt literals not displayed in prime implicants using org.sat4j.core.jar command line (launcher)Sat4j does not report learnt literals as part of the computed prime implicant.
Here is an example provided by a user:
```
p cnf 5 6
-1 -2 3 0
-1 2 3 0
1 -2 3 0
1 2 3 0
-4 5 0
4 5 0
```
This gives
```
s SATISFIABLE
c returning a prim...Sat4j does not report learnt literals as part of the computed prime implicant.
Here is an example provided by a user:
```
p cnf 5 6
-1 -2 3 0
-1 2 3 0
1 -2 3 0
1 2 3 0
-4 5 0
4 5 0
```
This gives
```
s SATISFIABLE
c returning a prime implicant ...
c prime implicant computation statistics BRESIL (reverse = false)
c implied: 0, decision: 5, removed 4 (+0), propagated 1, time(ms):0
c removed 4 literals
c pi computation time: 4 ms
v 3 0
```
But literal 5 should also be in the prime.
The issue is that Sat4j inherits from Minisat 1 it's management of unit clauses, which are not real constraints: they only live on the trail, not on the list of constraints.
We need to make sure that:
- either we use a specific data structure representing UnitClause in the solver
- or we simply add learnt literals to the prime implicantDaniel Le BerreDaniel Le Berrehttps://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 unsatisfia...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 ...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...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...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/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/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/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/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.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 t...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...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 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.1