sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2024-03-19T21:13:55Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/175Internal model enumeration provides incorrect results on this specific input ...2024-03-19T21:13:55ZDaniel Le BerreInternal model enumeration provides incorrect results on this specific input fileThe internal model enumeration does not provide the correct 2 models for the enclosed cnf file:
```
p cnf 10 23
1 3 6 0
2 5 0
4 5 0
5 0
-7 3 6 0
-3 7 0
-6 7 0
-1 -7 0
-2 -5 0
-8 1 6 0
-1 8 0
-6 8 0
-3 -8 0
-4 -5 0
-9 0
-5 -2 -4 -9 0
-10...The internal model enumeration does not provide the correct 2 models for the enclosed cnf file:
```
p cnf 10 23
1 3 6 0
2 5 0
4 5 0
5 0
-7 3 6 0
-3 7 0
-6 7 0
-1 -7 0
-2 -5 0
-8 1 6 0
-1 8 0
-6 8 0
-3 -8 0
-4 -5 0
-9 0
-5 -2 -4 -9 0
-10 1 3 0
-1 10 0
-3 10 0
-6 -10 0
-1 -2 0
-3 -4 0
-5 -6 0
```
It returns 11 models, which is incorrect (only the first two are corrects) :
```
c Found solution #1 (0,01)s
v -1 -2 3 -4 5 -6 7 -8 -9 10 0
c Found solution #2 (0,02)s
v 1 -2 -3 -4 5 -6 -7 8 -9 10 0
c Found solution #3 (0,02)s
v 1 2 -3 -4 5 -6 -7 8 -9 10 0
c Found solution #4 (0,02)s
v 1 -2 -3 4 5 -6 -7 8 -9 10 0
c Found solution #5 (0,02)s
v 1 2 -3 4 5 -6 -7 8 -9 10 0
c Found solution #6 (0,02)s
v 1 2 -3 4 -5 -6 -7 8 -9 10 0
c Found solution #7 (0,02)s
v 1 2 -3 4 5 -6 -7 8 9 10 0
c Found solution #8 (0,02)s
v 1 -2 -3 4 5 -6 -7 8 9 10 0
c Found solution #9 (0,02)s
v 1 2 -3 -4 5 -6 -7 8 9 10 0
c Found solution #10 (0,02)s
v 1 -2 -3 -4 5 -6 -7 8 9 10 0
c Found solution #11 (0,02)s
v 1 2 -3 4 -5 -6 -7 8 9 10 0
```
The external model enumeration provides the expected result.Daniel 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/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/134Throw IllegalStateException when calling unsatExplanation to avoid NPE.2018-07-07T05:11:53ZDaniel Le BerreThrow IllegalStateException when calling unsatExplanation to avoid NPE.If a user calls unsatExplanation() on a SAT problem, or before the solver has run, he will get an NPE.
One should throw an IllegalStateException with an appropriate message instead.If a user calls unsatExplanation() on a SAT problem, or before the solver has run, he will get an NPE.
One should throw an IllegalStateException with an appropriate message instead.https://gitlab.ow2.org/sat4j/sat4j/-/issues/132nesting atmost/atleast constraints into other constrains when using the gate ...2018-07-07T05:11:53ZMihai Barbuceanunesting atmost/atleast constraints into other constrains when using the gate translatorHi Daniel,
I've noticed that when using the GateTranslator, atleat/atmost constraints can only be specified globally for the gate. E.g. I can not say something like
if x then (atmost 1 y z w)
The atmost would apply globally to the ga...Hi Daniel,
I've noticed that when using the GateTranslator, atleat/atmost constraints can only be specified globally for the gate. E.g. I can not say something like
if x then (atmost 1 y z w)
The atmost would apply globally to the gate, not conditionally on x being true.
Is there a way to achieve this with the current GT, or is this a feature than can be introduced?
Many thanks,
Mihai
https://gitlab.ow2.org/sat4j/sat4j/-/issues/129Timeout should be in ms, not s2018-11-12T16:04:57ZDaniel Le BerreTimeout should be in ms, not sReceived from Arnaud Malapert:
Je crois qu'il y a une erreur dans le message de la TimeoutException.
Dans la classe Solver :
```
if (!undertimeout) {
String message = " Timeout (" + timeout
+ (timeBase...Received from Arnaud Malapert:
Je crois qu'il y a une erreur dans le message de la TimeoutException.
Dans la classe Solver :
```
if (!undertimeout) {
String message = " Timeout (" + timeout
+ (timeBasedTimeout ? "s" : " conflicts") + ") exceeded";
throw new TimeoutException(message); //$NON-NLS-1$//$NON-NLS-2$
}
```
Il me semble que timeout est en millisecondes plutôt qu'en secondes.https://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/123Does Sat4j provide model counting capability?2018-07-07T05:11:53ZMouhammad SakrDoes Sat4j provide model counting capability?https://gitlab.ow2.org/sat4j/sat4j/-/issues/122Allow the definitions of levels of the heuristic2018-07-07T05:11:53ZDaniel Le BerreAllow the definitions of levels of the heuristicIn some cases, domain knowledge allow the user of the solver to rank the variables to guide the solver.
It would be nice to provide a way to provide such information to Sat4j users.In some cases, domain knowledge allow the user of the solver to rank the variables to guide the solver.
It would be nice to provide a way to provide such information to Sat4j users.3.0https://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/116Implement decision conflict replacement proposed by Knuth2018-07-07T05:11:53ZDaniel Le BerreImplement decision conflict replacement proposed by KnuthDonald Knuth proposes in SAT13 to swap a regular conflict by a conflict clause containing only decision variables under certain conditions. It is not clear if such proposal works in practice.
All details available here:
http://www-cs-fac...Donald Knuth proposes in SAT13 to swap a regular conflict by a conflict clause containing only decision variables under certain conditions. It is not clear if such proposal works in practice.
All details available here:
http://www-cs-faculty.stanford.edu/~uno/programs/sat13.whttps://gitlab.ow2.org/sat4j/sat4j/-/issues/115Fix issue in Minisat Expensive Simplification2018-07-07T05:11:53ZDaniel Le BerreFix issue in Minisat Expensive SimplificationThe minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?).
The code...The minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?).
The code of minisat available in github contains the fix. We might want to implement our own.
It might be the case that such issue arrises when using cardinality constraints. Need to investigate further.https://gitlab.ow2.org/sat4j/sat4j/-/issues/114Implement reusable trail2018-07-07T05:11:52ZDaniel Le BerreImplement reusable trailReusable trail is proven to be efficient (used in Lingeling and Knuth SAT13 CDCL solver).
In order to implement future improvements in Sat4j, implementing such feature becomes mandatory.
All details are available here:
http://jsat.ewi.tu...Reusable trail is proven to be efficient (used in Lingeling and Knuth SAT13 CDCL solver).
In order to implement future improvements in Sat4j, implementing such feature becomes mandatory.
All details are available here:
http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_11_vanderTak.pdfhttps://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/111Iteration through all possible solutions didn't find all possible solutions2018-04-13T11:56:15ZSascha El-sharkawyIteration through all possible solutions didn't find all possible solutionsHello,
I downloaded a dimacs translation of the Linux kernel 2.6.33 (http://formulas.linux-variability-analysis-tools.googlecode.com/hg/2.6.33.3-2var.dimacs, I removed the 2 blank lines at the end of the file). And tried it to reason it ...Hello,
I downloaded a dimacs translation of the Linux kernel 2.6.33 (http://formulas.linux-variability-analysis-tools.googlecode.com/hg/2.6.33.3-2var.dimacs, I removed the 2 blank lines at the end of the file). And tried it to reason it with Sat4j 2.3.4 (http://forge.ow2.org/project/download.php?group_id=228&file_id=19075). I tried 2 different possibilities to iterate through all possible solutions:
1. With a loop over problem.isSatisfiable() (c.f. http://www.sat4j.org/howto.php#models).
2. With the ModelIterator (c.f http://www.sat4j.org/maven21/org.sat4j.core/apidocs/org/sat4j/tools/ModelIterator.html).
I saved all found solutions to my hard disk and compared each other with a diff tool. Only the first 6 solutions are different, all other models are equal to the 6st solution.
I tried also another possibility; iterating through all variables and adding a constraint to the complete model, that this variable must be true. Excerpt from my code:
```
Reader reader = new DimacsReader(solver);
for (int i = 1; i <= problem.nVars(); i++) {
int[] varAssignment = {i};
int configNo = 0;
List<int[]> foundSolutions = new ArrayList<int[]>();
try {
solver.addClause(new VecInt(varAssignment));
if(solver.isSatisfiable()) {
System.out.println("Created Configuration No. " + configNo);
int[] newModel = problem.model();
if (!compareSolutions(foundSolutions, newModel)) {
saveModel(folder, configNo);
foundSolutions.add(newModel);
configNo++;
}
}
} catch (ContradictionException e) {
System.out.println("Empty clause added. This model will be skipped.");
}
reader.parseInstance(filename); // Reset model
}
```
The third options find more than 6 different solutions. Can anybody explain my why the documented iterators only find 6 solutions? I guess this is a bug, or did I used sat4J wrong?
Best regards,
Sascha El-Sharkawy