sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-11-13T06:56:33Zhttps://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/140Add support for parity constraints2018-09-16T15:09:50ZDaniel Le BerreAdd support for parity constraintsSome applications require Boolean exploration of spaces defined using clauses, pseudo-Boolean constraints but also parity constraints.
Sat4j supports already clauses, cardinality and pseudo-Boolean constraints. Parity constraints suppor...Some applications require Boolean exploration of spaces defined using clauses, pseudo-Boolean constraints but also parity constraints.
Sat4j supports already clauses, cardinality and pseudo-Boolean constraints. Parity constraints support could be added to Sat4j core the same way as the cardinality constraints: by providing a concise representation of those constraints but still using the resolution proof system.
2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/139Invalid multiple solutions with call to isSatisfiable(true) in ModelIterator2018-04-13T11:56:15ZMark EngelbergInvalid multiple solutions with call to isSatisfiable(true) in ModelIteratorI am generating multiple solutions for a sat problem in the following way:
Create the default solver.
Call the newVar method with exactly the number of variables in my problem.
Call the setExpectedNumberOfClauses method with exactly the...I am generating multiple solutions for a sat problem in the following way:
Create the default solver.
Call the newVar method with exactly the number of variables in my problem.
Call the setExpectedNumberOfClauses method with exactly the number of clauses (not including the added "exactly" constraint).
Call addClause multiple times to add all the clauses.
Call addExactly to add one "exactly" constraint.
Call isSatisfiable(true) and when this returns true, call model() to get one of the solutions to my problem.
Then, I use addBlockingClause to add the exact opposite of the solution (i.e., negating all the numbers in the solution) to the solver.
I continue by again calling isSatisfiable(true) and if this returns true, call model() to get the next solution to my problem.
I repeat this process until isSatisfiable(true) returns false.
What I am finding is that subsequent calls to isSatisfiable after the first solution is found and I call addBlockingClause to block that solution *do not* respect the "exactly" constraint I have imposed on the solver.
Is this a known problem? Is my strategy for getting multiple solutions sound? Is there a workaround, for example, should I re-assert the exact constraints each time I add a blocking clause?2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/138Fix WBO issue found during PB 20162018-07-07T05:11:54ZDaniel Le BerreFix WBO issue found during PB 2016A problem with WBO has been discovered during PB16. It seems that the top costs are ignored.A problem with WBO has been discovered during PB16. It seems that the top costs are ignored.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/137DependencyHelper corrupts existing constraints2018-04-13T11:56:14ZRobert GiegerichDependencyHelper corrupts existing constraintsOriginally I added constraints directly with methods of the solver object. As I want to add implications with more comfort, I tried to switch to DependencyHelper.
```
FOREACH ASSIGNMENT:
solver.addExactly(new VecInt(zap.toArray), 1)
FO...Originally I added constraints directly with methods of the solver object. As I want to add implications with more comfort, I tried to switch to DependencyHelper.
```
FOREACH ASSIGNMENT:
solver.addExactly(new VecInt(zap.toArray), 1)
FOREACH TEACHER:
solver.addAtLeast(new VecInt(vars.toArray), new VecInt(weights.toArray), number)
solver.addAtLeast(new VecInt(vars.toArray), new VecInt(weights.toArray), number)
{code}
becomes
{code:title=Solution invalid}
FOREACH ASSIGNMENT:
depHelper.atLeast("Require at least one teacher for " + key, 1, zap.toArray:_*)
depHelper.atMost("Require at most one teacher for " + key, 1, zap.toArray:_*)
FOREACH TEACHER:
depHelper.atLeast("Hours at least " + number + " of " + variables, number, weightedVariables:_*)
depHelper.atMost("Hours at most " + number+ " of " + variables, number, weightedVariables:_*)
```
Now the solver presents an invalid solution, breaking some "Exactly one assignment"-constraints in both ways: Sometimes no teacher is assigned, sometimes several teachers are. When I leave out the constraints limiting the teacher's work hours, the solution is valid.
The DependencyHelper is of type \[Int,String\], but i also found this result when using my own type as "T" (\[DecisionVar,String\]).2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/135Sat4j not terminating2015-11-09T16:03:01ZAnithaSat4j not terminatingI am using pseudo boolean solver to find minimize an objective function. sat4j worked fine for small examples. However, with the attached testcase, it runs indefinitely. Moreover, whats confusing is: After 1hr or so, it gives segmentatio...I am using pseudo boolean solver to find minimize an objective function. sat4j worked fine for small examples. However, with the attached testcase, it runs indefinitely. Moreover, whats confusing is: After 1hr or so, it gives segmentation fault 11 in my terminal but the process still runs in background. I am confused.
23230 ttys001 67:08.18 /usr/bin/java -jar /Users/.../sat4j/sat4j-pb.jar min.opb
Attaching testcase in opb format. It consists of non-linear constraints. I am not sure if something is wrong with the testcase. It looks fine to me.
Appreciate reply as soon as possible.
2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/131Sat4j maxsat does not pick the right reader with an arbitrary extension2018-04-13T11:56:14ZDaniel Le BerreSat4j maxsat does not pick the right reader with an arbitrary extensionWhen a new user of sat4j tries to solve a partial weighted maxsat problem, it is likely that the extension used may not be the expected wcnf.
In that case, the default solver is the cnf one, which will wrongly interpret the content of t...When a new user of sat4j tries to solve a partial weighted maxsat problem, it is likely that the extension used may not be the expected wcnf.
In that case, the default solver is the cnf one, which will wrongly interpret the content of the file, i.e. will treat the first number, the weight, as a literal.
There are several ways to solve this:
- do not use the extension to decide of the reader
- display an error message if the wncf extension is seen by the classical Dimacs reader.
The latter is probably the best option.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/130Support unused variables in the objective function when the optimization prob...2018-04-13T11:56:16ZDaniel Le BerreSupport unused variables in the objective function when the optimization problem is trivialDuring the PB15, an issue was discovered when variables not used in the CNF appear in the objective function and that the optimal solution is found directly.
Here is a simple test case:
[code]
* #variable= 3 #constraint= 1
min: +1 x1 +...During the PB15, an issue was discovered when variables not used in the CNF appear in the objective function and that the optimal solution is found directly.
Here is a simple test case:
[code]
* #variable= 3 #constraint= 1
min: +1 x1 +1 x2 +1 x3 ;
+1 x3 +1 x2 = 1;
[/code]
The solver will find a first model x2 -x3 for instance which satisfes the constraint.
The solver adds a constraint x1 + x2 +x3 < 1 which makes the formula UNSAT.
As such, the previous model, without mention of x1 is returned.
We need to detect that case, and to complete the model by falsifying the literals found in the objective function.
Detecting that situation is easy. Fixing properly the model requires a bit of work.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/124Lexico-Optimization does not work with ManyCore (parallel) solvers.2015-01-15T09:23:22ZDaniel Le BerreLexico-Optimization does not work with ManyCore (parallel) solvers.During the LION 9 challenge, two versions of Sat4j was used.
That challenge is about solving multi-objective boolean functions, in that case lexicographic one.
The pure resolution based one worked fine while the one using the parallel ...During the LION 9 challenge, two versions of Sat4j was used.
That challenge is about solving multi-objective boolean functions, in that case lexicographic one.
The pure resolution based one worked fine while the one using the parallel solver Both answered sub-optimal solutions.
The parallel solver has been used successfully for years on PB benchmarks.
The main issue with lexicographic optimization is that an UNSAT answer is not final contrariwise to the mono-objective optimization.
Initial investigation of the problem shows that the parallel solvers always answer UNSAT after a while.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/121Initialization of org.sat4j.minisat.core.Solver calls Runtime.getRuntime().fr...2018-04-13T11:56:14ZGhost UserInitialization of org.sat4j.minisat.core.Solver calls Runtime.getRuntime().freeMemory()The class Solver in the sat4j core package initializes a variable called "memoryTimer" with an anonymous inner class of type ConflictTimerAdapter.
This inner class statically initializes a variable called "memorybound":
final long memor...The class Solver in the sat4j core package initializes a variable called "memoryTimer" with an anonymous inner class of type ConflictTimerAdapter.
This inner class statically initializes a variable called "memorybound":
final long memorybound = Runtime.getRuntime().freeMemory() / 10;
This is an expensive operation which seems to slow down the entire system for counting the available memory. In a multi-threaded scenary with many small partial weighted maxsat instances, it can lead to the machine being occupied with calculating the free memory again and again.
And: The initial class is not necessarily needed at all, e.g. when running a WeightedMaxSatDecorator with the default solver:
maxSatSolver = new WeightedMaxSatDecorator(SolverFactory.newDefault());
I propose to implement another kind of initialization that is only computing the amount of available memory when it is really needed. There are some usages of the variable "solver.memory_based" insat4j-core and sat4j-pb, and I think this could be replaced by a getter method that does the initialization when it is needed.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/120Remove call to System.gc in solver2018-04-13T11:56:12ZGhost UserRemove call to System.gc in solverI did some performance tests with the partial weighted maxsat solver called in many (up to 150) threads. After a while, tens of threads stuck in the call to "System.gc" in the class "org.sat4j.minisat.core.Solver", method "reduceDB()". T...I did some performance tests with the partial weighted maxsat solver called in many (up to 150) threads. After a while, tens of threads stuck in the call to "System.gc" in the class "org.sat4j.minisat.core.Solver", method "reduceDB()". This was a major performance bottleneck.
I downloaded the source, removed the call to "System.gc", compiled the sat4j-core and started the performance test again. The bottleneck was gone.
I think this call to System.gc should be removed. If there is really a need for this call, it could be made configurable (via an API call), so that it can be switched off if sat4j is used in multithreaded applications.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/119Iterators can be created at each conflict2018-04-13T11:56:15ZBenoƮt HoessenIterators can be created at each conflictWhenever the ConflictTimerContainer is used, an iterator on Vec is created.
```
public void newConflict() {
Iterator<ConflictTimer> it = this.timers.iterator();
while (it.hasNext()) {
it.next().newConfli...Whenever the ConflictTimerContainer is used, an iterator on Vec is created.
```
public void newConflict() {
Iterator<ConflictTimer> it = this.timers.iterator();
while (it.hasNext()) {
it.next().newConflict();
}
}
{code}
This could be easily changed to a version using no iterator to avoid object creation/destruction
{code:title=ConflictTimerContainer.java|borderStyle=solid}
public void newConflict() {
for(int i =0; i<this.timers.size(); i++){
this.timers.get(i).newConflict();
}
}
```
This, applied to a small instance like velev-engi-uns-1.0-4nd.cnf can reduce the number of created object by 92594 (= 311936 B)2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/118Crashes with NPE after call to unsatExplanation()2018-04-13T11:56:17ZRobert StelzmannCrashes with NPE after call to unsatExplanation()- created a solver with SolverFactory.newLight() respectively SolverFactory.newDefault()
- ran it via isSatisfiable()
-> call to unsatExplanation() leads to a NPE, since unsatExplanationInTermsOfAssumptions is null.- created a solver with SolverFactory.newLight() respectively SolverFactory.newDefault()
- ran it via isSatisfiable()
-> call to unsatExplanation() leads to a NPE, since unsatExplanationInTermsOfAssumptions is null.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/117Timers are not correctly released when performing optimization2018-04-13T11:56:14ZDaniel Le BerreTimers are not correctly released when performing optimizationIan Bull reported that using Sat4j 2.3.5 with eclipse, when calling thousands of time Sat4j, most timers were not released.
Ian Bull reported that using Sat4j 2.3.5 with eclipse, when calling thousands of time Sat4j, most timers were not released.
2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/113Lower bounding optimization does not work for maxsat2018-04-13T11:56:13ZDaniel Le BerreLower bounding optimization does not work for maxsatWhen using the lower bounding technique on a maxsat problem, the solver does not stop when the formula becomes satisfiable.
The enclosed wcnf has an optimal solution of 400, found using upper bounding, but not found using lower bounding.When using the lower bounding technique on a maxsat problem, the solver does not stop when the formula becomes satisfiable.
The enclosed wcnf has an optimal solution of 400, found using upper bounding, but not found using lower bounding.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/112Integrate faster prime implicant computation2018-04-13T11:56:11ZDaniel Le BerreIntegrate faster prime implicant computationWe propose in a paper to be presented in FMCAD 2013 a new algorithm for computing prime implicants in a CDCL solver. The code of that paper is available on a specific branch (BRESIL). We need to move that code to the main branch now, and...We propose in a paper to be presented in FMCAD 2013 a new algorithm for computing prime implicants in a CDCL solver. The code of that paper is available on a specific branch (BRESIL). We need to move that code to the main branch now, and to make a release of Sat4j including that new feature before presenting that work at FMCAD.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/110Remove propagated literals when removing a PB constraint2018-04-13T11:56:17ZDaniel Le BerreRemove propagated literals when removing a PB constraintIt may happen in some cases that a PB constraint propagates literals at decision zero.
In case of clauses or cardinality constraints, a unit clause of a set of unit clauses are returned, so when those constraints are removed, they are re...It may happen in some cases that a PB constraint propagates literals at decision zero.
In case of clauses or cardinality constraints, a unit clause of a set of unit clauses are returned, so when those constraints are removed, they are removed from the trail.
In the case of PB constraints, the propagated literals are not associated to unit clauses. As such, the remove method in PB constraint should take care to remove from the trail the implied literals (the ones pushed at decision level 0).
The issue was discovered by Yacoub in the context of maxsat solving using lower bounding.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/109Allow iterating on a part of a model (subset of its variables)2018-04-13T11:56:13ZDaniel Le BerreAllow iterating on a part of a model (subset of its variables)In some cases, it may be useful to iterate over a subset of the variables
(over decisions variables for instance).
The idea is to simply restrict the use of the model iterator (using blocking clauses) to a subset of the variables only.
...In some cases, it may be useful to iterate over a subset of the variables
(over decisions variables for instance).
The idea is to simply restrict the use of the model iterator (using blocking clauses) to a subset of the variables only.
We require for this a new class, for efficiency reason, instead of generalizing the code of the actual ModelIterator class.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/106release jars do not include debug information2018-04-13T11:56:16ZDaniel Le Berrerelease jars do not include debug informationThe jar currently produced by our ant script does not provide jars with debug information included. As such, if an error occurs, there is not reference to the line number in the stack trace.The jar currently produced by our ant script does not provide jars with debug information included. As such, if an error occurs, there is not reference to the line number in the stack trace.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/105o line is incorrect for internal optimizer2018-04-13T11:56:13ZDaniel Le Berreo line is incorrect for internal optimizerDuring the testing phase, the organizers of the MAXSAT evaluation discovered that the internal optimizer was not displaying the correct o line for the certificate displayed for the optimal solution.
(the latter is correct, while the form...During the testing phase, the organizers of the MAXSAT evaluation discovered that the internal optimizer was not displaying the correct o line for the certificate displayed for the optimal solution.
(the latter is correct, while the former is an upper bound of the optimal solution).2.3.6