sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/issues2018-09-16T15:09:50Zhttps://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 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.
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 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?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)
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\]).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/136Incorrect answer with PB Solver2018-07-07T05:11:54ZAnithaIncorrect answer with PB SolverI am seeing a strange issue with solving a PBO problem using SAT4J: version NIGHTLY.v20151101
Attached are 2 opb files: min-nonbuggy.opb and min.opb
Differences between the files: Both files differ from line 18 onwards. "min.opb" is an extension of min-nonbuggy.opb. Note that both files have same objective function that needs to be minimized.
The first file ("min-nonbuggy.opb") returns correct answer with optimum value as "4" with x12=0, x14 = 0 and x17=0. I agree with this answer. I also verified this by manually solving the constraints and objective function.
The second file ("min.opb") returns answer with optimum value as "5" with x12=1, x14=0 and x17=0. I think this is wrong.
(I am interested in values that appear in objective function only)
This is quite surprising given that - no additional constraint involving "x12" appears in "min.opb". So x12 should be 0 regardless of value of x17. Isn't it? Why is the answer returned as x12=1?
I am seeing a strange issue with solving a PBO problem using SAT4J: version NIGHTLY.v20151101
Attached are 2 opb files: min-nonbuggy.opb and min.opb
Differences between the files: Both files differ from line 18 onwards. "min.opb" is an extension of min-nonbuggy.opb. Note that both files have same objective function that needs to be minimized.
The first file ("min-nonbuggy.opb") returns correct answer with optimum value as "4" with x12=0, x14 = 0 and x17=0. I agree with this answer. I also verified this by manually solving the constraints and objective function.
The second file ("min.opb") returns answer with optimum value as "5" with x12=1, x14=0 and x17=0. I think this is wrong.
(I am interested in values that appear in objective function only)
This is quite surprising given that - no additional constraint involving "x12" appears in "min.opb". So x12 should be 0 regardless of value of x17. Isn't it? Why is the answer returned as x12=1?
https://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 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.
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/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/133Support XCSP 3 format2018-07-07T05:11:53ZDaniel Le BerreSupport XCSP 3 formatA new version of XCSP has just been released.
http://xcsp.org/
The most important part of the new format is available in available in a subset of the spec, XCSP 3.0 core:
http://xcsp.org/core/menuCore.html
Sat4j CSP should implement it to be used in the classroom with master students.A new version of XCSP has just been released.
http://xcsp.org/
The most important part of the new format is available in available in a subset of the spec, XCSP 3.0 core:
http://xcsp.org/core/menuCore.html
Sat4j CSP should implement it to be used in the classroom with master students.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 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
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/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 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.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 +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.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/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
+ (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.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/128PB solver finds wrong optimal solution when a unit clause appears in the inpu...2018-07-07T05:11:53ZDaniel Le BerrePB solver finds wrong optimal solution when a unit clause appears in the input fileWhen running the functional tests on PB12 benchmarks, the solvers return incorrectly on a few benchmarks, e.g. normalized-PB06/OPT-SMALLINT/submitted-PB06/manquiho/bounded_golomb_rulers/normalized-bogr_7.opb.
Those benchmarks contain unit clauses.
It might be the case that a propagation by one learned constraint is removed incorrectly (e.g. a PB constraint propagates x which is also a unit clause).
We may need to check in the PB constraint when we remove it if the literals are not propagated by a unit clause, or simply to remove that literal from the PB constraint.When running the functional tests on PB12 benchmarks, the solvers return incorrectly on a few benchmarks, e.g. normalized-PB06/OPT-SMALLINT/submitted-PB06/manquiho/bounded_golomb_rulers/normalized-bogr_7.opb.
Those benchmarks contain unit clauses.
It might be the case that a propagation by one learned constraint is removed incorrectly (e.g. a PB constraint propagates x which is also a unit clause).
We may need to check in the PB constraint when we remove it if the literals are not propagated by a unit clause, or simply to remove that literal from the PB constraint.https://gitlab.ow2.org/sat4j/sat4j/issues/127OPBSolver exports files with empty objectives2018-11-12T16:07:10ZGhost UserOPBSolver exports files with empty objectivesI tried the OPBSolverDecorator for exporting .opb files. In some cases, my objective function is empty because I am solving a pure SAT instance (using the PB solver because of "at most 1"-constraints).
In these cases, the OPBSolverDecorator outputs a .opb format that the command line sat4j-pb.jar does not understand. The text opb file then contains the following line:
min: ;
This is because the "toString()" method does a null-check on the objective function, but it does no empty-check on it. I think my fix for it is suboptimal:
```
if (this.obj != null) {
String objStr = obj.toString();
if (objStr.trim().length() > 0) {
tmp.append("\n");
tmp.append("min: ");
tmp.append(this.obj);
tmp.append(";");
}
}
```I tried the OPBSolverDecorator for exporting .opb files. In some cases, my objective function is empty because I am solving a pure SAT instance (using the PB solver because of "at most 1"-constraints).
In these cases, the OPBSolverDecorator outputs a .opb format that the command line sat4j-pb.jar does not understand. The text opb file then contains the following line:
min: ;
This is because the "toString()" method does a null-check on the objective function, but it does no empty-check on it. I think my fix for it is suboptimal:
```
if (this.obj != null) {
String objStr = obj.toString();
if (objStr.trim().length() > 0) {
tmp.append("\n");
tmp.append("min: ");
tmp.append(this.obj);
tmp.append(";");
}
}
```https://gitlab.ow2.org/sat4j/sat4j/issues/126How do I do an industry standard export for Partial Weighted MaxSat problems?2018-07-07T05:11:53ZGhost UserHow do I do an industry standard export for Partial Weighted MaxSat problems?I have filed this as question, but it might result in a change request:
I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constraints. If I do not want to convert them to CNF constraints, I cannot export a wcnf file but must export something other.
I think the .opb format is suitable for that case. Am I right?
I tried to create .opb output using the OPBStringSolver or the LPStringSolver. Both have the same problem:
The WeightedMaxSatDecorator calls the method "registerLiteral(int p)" on the decorated solver. Since both the OPBStringSolver and the LPStringSolver extend the DimacsStringSolver, the method DimacsStringSolver.registerLiteral(int p) is called, which throws an UnsupportedOperationException.
So, if one of these StringSolvers is suitable for my problem: Would it be a solution to override the method in that suitable solver so that it does not do anything?
An, if none of these StringSolvers is suitable: Is there another way of exporting all input that the WeightedMaxSatDecorator got into a standard file format?I have filed this as question, but it might result in a change request:
I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constraints. If I do not want to convert them to CNF constraints, I cannot export a wcnf file but must export something other.
I think the .opb format is suitable for that case. Am I right?
I tried to create .opb output using the OPBStringSolver or the LPStringSolver. Both have the same problem:
The WeightedMaxSatDecorator calls the method "registerLiteral(int p)" on the decorated solver. Since both the OPBStringSolver and the LPStringSolver extend the DimacsStringSolver, the method DimacsStringSolver.registerLiteral(int p) is called, which throws an UnsupportedOperationException.
So, if one of these StringSolvers is suitable for my problem: Would it be a solution to override the method in that suitable solver so that it does not do anything?
An, if none of these StringSolvers is suitable: Is there another way of exporting all input that the WeightedMaxSatDecorator got into a standard file format?https://gitlab.ow2.org/sat4j/sat4j/issues/125CP solver provides incorrect results when performing Lexico-optimization2018-07-07T05:11:53ZDaniel Le BerreCP solver provides incorrect results when performing Lexico-optimizationOnce issue #124 has been fixed, the parallel solver res+cp solver still provides a wrong solution (ignore unit clauses in 3 cases) or wrong optimum (in 10 cases) out of the 2688 benchmarks.
It is likely that such issue is related to former #113 issue, i.e. incorrect handling of unit clause removal in case of unsatisfiability.Once issue #124 has been fixed, the parallel solver res+cp solver still provides a wrong solution (ignore unit clauses in 3 cases) or wrong optimum (in 10 cases) out of the 2688 benchmarks.
It is likely that such issue is related to former #113 issue, i.e. incorrect handling of unit clause removal in case of unsatisfiability.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 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.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 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.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.6