SAT4J issueshttps://gitlab.ow2.org/groups/sat4j/-/issues2021-10-07T05:52:49Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/55Fix memory leak in case of repeated use of Sat4j in an application2021-10-07T05:52:49ZDaniel Le BerreFix memory leak in case of repeated use of Sat4j in an applicationIn an application creating new solvers on user's action, the consumption of memory is growing.
It looks like there is a memory leak somewhere.In an application creating new solvers on user's action, the consumption of memory is growing.
It looks like there is a memory leak somewhere.2.3.2https://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/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/70Allow the possibility to compute counter models (negate a formula)2019-01-03T09:55:38ZDaniel Le BerreAllow the possibility to compute counter models (negate a formula)In some cases, it is necessary to compute counter examples of a formula (i;e. models of the negation of the formula).
It is easy to do that using the Plaisted-Greenbaum transformation, i.e. by adding a new fresh variable zi per constrai...In some cases, it is necessary to compute counter examples of a formula (i;e. models of the negation of the formula).
It is easy to do that using the Plaisted-Greenbaum transformation, i.e. by adding a new fresh variable zi per constraint, creating binary clauses -zi \lor -lj for each clause, and adding a new clause containing all zi.
This could be performed easily in a decorator.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/69Fix the value returned by the MAXSAT solver2019-01-03T09:55:38ZDaniel Le BerreFix the value returned by the MAXSAT solverThe maxsat solver currently displays a value for maxsat which is an upper bound of the real value until an optimal solution is found, because some selector variables may be satisfied while the corresponding clause is not falsified.
Whil...The maxsat solver currently displays a value for maxsat which is an upper bound of the real value until an optimal solution is found, because some selector variables may be satisfied while the corresponding clause is not falsified.
While it does not make the solver incorrect, computing a correct value might help finding faster an optimal solution.https://gitlab.ow2.org/sat4j/sat4j/-/issues/68Allow computing all MUSes using two calls to the SAT solver2019-01-03T09:55:38ZDaniel Le BerreAllow computing all MUSes using two calls to the SAT solverSat4j can currently compute one MUS.
It is possible to compute all MUSes using two calls to a SAT solver: the first one to detect all P-prime M-implicant of the formula (see my ECAI 96 paper or my PhD - in french- for details), the secon...Sat4j can currently compute one MUS.
It is possible to compute all MUSes using two calls to a SAT solver: the first one to detect all P-prime M-implicant of the formula (see my ECAI 96 paper or my PhD - in french- for details), the second one to compute a minimal hitting set (here it is mandatory to compute prime implicants).
The main issue will be to perform the second step: the first one can be performed by applying MAXSAT SAT several times, and preventing the same solutions to appear by adding blocking clauses.
2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/67Concurrent calls to isSatisfiable2019-01-03T09:55:38ZAlexey VoronovConcurrent calls to isSatisfiableIt would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under th...It would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under the hood, which resulted in very misleading exceptions until I realised that there was a concurrency problem.
An easy solution would be to simply add Synchronized to isSatisfiable() functions. The drawback of this will be that the call to model() after isSatisfiable() might give the model for the assumptions of another thread.
Another solution is to add ConcurrentModificationException if isSatisfiable is called while another call to isSatisfiable is in progress. This will not solve problems with model() after isSatisfiable(), but at least might hint early on that there is a concurrency problem.
A great solution would be to allow multiple calls to isSatisfiable (with different sets of assumptions) to be executed in parallel. I’m not sure that this is achievable by any simple code modification, but my thoughts are as following. Whatever is kept in the solver between consecutive calls can be readily shared between two parallel calls. And whatever is removed between consecutive calls should be private to each call of isSatisfiable. API would change, since models would be different for each call to isSatisfiable, but isSatisfiable itself could return the model if there exist one (using some java variant of Haskell’s Maybe or Scala’s Option class).
Parallel calls would create all sorts of problems, for example, what happens if a clause is added to the solver while a call to isSatisfiable() is in progress in another thread. But maybe such issues can be separated somehow.
I don’t yet know what would be the simplest---yet user-friendly--- solution. All ideas welcome :)2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/66Incorrect explanations in PB2019-01-03T09:55:38ZAlexey VoronovIncorrect explanations in PBWhen 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 ...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<IPBSolver> 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.
2.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/65Fix the value of the objective function in maxsat when some constraints are ...2019-01-03T09:55:38ZDaniel Le BerreFix the value of the objective function in maxsat when some constraints are satisfiedIt looks like the value of the objective function in maxsat is not correct when some (say k) constraints are trivially satisfied.
In that case, the value of the objective function is l+k instead of l.It looks like the value of the objective function in maxsat is not correct when some (say k) constraints are trivially satisfied.
In that case, the value of the objective function is l+k instead of l.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/64Allow the solver to keep hot between successive calls2019-01-03T09:55:38ZDaniel Le BerreAllow the solver to keep hot between successive callsIn some cases, it may be interesting to keep the SAT solver in a state where the heuristics is not reset at each call.
As such, there is basically no difference between a restart and stopping the solver and starting it again (phase savin...In some cases, it may be interesting to keep the SAT solver in a state where the heuristics is not reset at each call.
As such, there is basically no difference between a restart and stopping the solver and starting it again (phase saving would be kept too).
Note that is does not look to pay off for optimization but might be useful for other uses.https://gitlab.ow2.org/sat4j/sat4j/-/issues/63Make Java 1.5 binaries instead of 1.42019-01-03T09:55:38ZDaniel Le BerreMake Java 1.5 binaries instead of 1.4Eclipse 4.2 will stop support for 1.4 VM as such it now requires 1.5 bycote instead of 1.4 one:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=369145
Sat4j is written in Java 5 but is downcompiled to Java 1.4 bytecode using JSR 14 target...Eclipse 4.2 will stop support for 1.4 VM as such it now requires 1.5 bycote instead of 1.4 one:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=369145
Sat4j is written in Java 5 but is downcompiled to Java 1.4 bytecode using JSR 14 target.
Starting with Sat4j 2.3.2, Sat4j will be compiled with target 1.5 instead of jsr14.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/61non linear constraints report incorrect results when conjuncts appear multipl...2019-01-03T09:55:38ZDaniel Le Berrenon linear constraints report incorrect results when conjuncts appear multiple times.The following problem was reported for Sat4j 2.3.0.
In the file:
* #variable= 11 #constraint= 1
-1 x1 -2 x9 x4 -3 x10 x4 -4 x11 x4 +5 x8 x4 -6 x9 x4 -7 x10 x4 -8 x11 x4 +9
x8 x4 -10 x9 x4 -11 x10 x4 -12 x11 x4 +13 x8 x4 -14 x9 x4 -15 x...The following problem was reported for Sat4j 2.3.0.
In the file:
* #variable= 11 #constraint= 1
-1 x1 -2 x9 x4 -3 x10 x4 -4 x11 x4 +5 x8 x4 -6 x9 x4 -7 x10 x4 -8 x11 x4 +9
x8 x4 -10 x9 x4 -11 x10 x4 -12 x11 x4 +13 x8 x4 -14 x9 x4 -15 x10 x4 -16 x11
x4 +17 x8 x4 -18 x9 x4 -19 x10 x4 -20 x11 x4 +21 x8 x4 = 9;
the solver answers unsat, while there is a solution.
x1 x4 x8 -x9 x10 -x11 for instance.
The problem comes from the constraint being build with conjuncts that appear several times.
Merging the conjuncts solves the problem:
* #variable= 11 #constraint= 1
-1 x1 -50 x9 x4 -55 x10 x4 -60 x11 x4 +65 x8 x4 = 9;
In competition settings, this case is not going to appear.
However, it can happen when Sat4j is used in an application.
Thus we need to sort it out.https://gitlab.ow2.org/sat4j/sat4j/-/issues/60ClassCastException when a class implements Propagatable but not Constr watche...2019-01-03T09:55:37ZPablo AbadClassCastException when a class implements Propagatable but not Constr watches a conflicting literalWhile experimenting with some new constraint types I've run into the situation where a constraint looks at several gruop of literals.
For that, each group has it's own class that watches for propagation and undo of their literals.
Since...While experimenting with some new constraint types I've run into the situation where a constraint looks at several gruop of literals.
For that, each group has it's own class that watches for propagation and undo of their literals.
Since watches require that a class implements interface Propagatable, everything looks fine, but I'm havng problems when one of the watched literals is identidfied as part of a conflict.
The offending lines are located in Solver.java around line 1025:
{noformat}
public Constr propagate() {
...
qhead = ltrail.size(); // propQ.clear();
// FIXME enlever le transtypage
return (Constr) lwatched.get(i);
...
}
{noformat}
There, a Propagatable from the watch list is cast to Constr to return the conflicting clause.
As a workaround, I've added a new method to Propagatable:
{noformat}
/**
* Returns the associated constraint with this object. Used for conflict analisys
*/
Constr associatedConstraint();
{noformat}
then I modified all the existing clauses to define this method as returning this:
{noformat}
public Constr associatedConstraint() {
return this;
}
{noformat}
and finally modified Solver to use the new method.
{noformat}
public Constr propagate() {
...
qhead = ltrail.size(); // propQ.clear();
return lwatched.get(i).associatedConstraint();
...
}
{noformat}
This works fine for the ocnstraints I'm defining, but it will be great if SAT4J can support this case by default, as the API implies.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/59Use package-info.java instead of package.html for package JavaDoc2019-01-03T09:55:37ZDaniel Le BerreUse package-info.java instead of package.html for package JavaDocThere are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move t...There are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move the current package documentation inside package-info.java files.
See http://docs.oracle.com/javase/6/docs/technotes/tools/solaris/javadoc.html#packagecomment for details.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/56Allow the end user to visualize the search of the solvers2019-01-03T09:55:37ZDaniel Le BerreAllow the end user to visualize the search of the solversIt is possible to hook SearchListener s to the solver in order to see what's going on inside the solver.
However, this need to be done using the API. There is currently no easy way to allow the command line user to trace the behavior of ...It is possible to hook SearchListener s to the solver in order to see what's going on inside the solver.
However, this need to be done using the API. There is currently no easy way to allow the command line user to trace the behavior of the solver.
It would be nice to provide a default tracing scheme to monitor the solver's behavior.2.3.2https://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 Neves