sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-09-16T14:55:52Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/146ModelIteratorTest.testGlobalTimeoutCounter makes build instable2018-09-16T14:55:52ZDaniel Le BerreModelIteratorTest.testGlobalTimeoutCounter makes build instableThe test case ModelIteratorTest.testGlobalTimeoutCounter uses a timeout, which makes the test fail if it is reached.
The issue is that such timeout may be reached depending of the load of the computer running the tests.
So the same cod...The test case ModelIteratorTest.testGlobalTimeoutCounter uses a timeout, which makes the test fail if it is reached.
The issue is that such timeout may be reached depending of the load of the computer running the tests.
So the same code may pass or not pass the tests depending of the load of the runner ...https://gitlab.ow2.org/sat4j/sat4j/-/issues/142Java 9 modularization?2022-03-09T14:39:30ZMark RaynsfordJava 9 modularization?Hello.
Are there any plans to modularize `sat4j` as Java 9 modules?Hello.
Are there any plans to modularize `sat4j` as Java 9 modules?3.0https://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/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/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...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/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...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 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/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 un...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 OPBSolverDecor...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 constrai...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 for...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/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/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/102API for using an OPB string spec2018-07-07T05:11:52ZMihai BarbuceanuAPI for using an OPB string specHi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going throug...Hi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going through the command line.
Many Thanks,
Mihaihttps://gitlab.ow2.org/sat4j/sat4j/-/issues/97Allow Sat4j statistics to be visible using JMX2018-07-07T05:11:52ZDaniel Le BerreAllow Sat4j statistics to be visible using JMXJava allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we c...Java allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we could at least use it for providing an access to the solver statistics while the solver is running.https://gitlab.ow2.org/sat4j/sat4j/-/issues/93Find a way to factorize the various settings for the solvers2018-07-07T05:11:52ZDaniel Le BerreFind a way to factorize the various settings for the solversThe PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not...The PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not have any dependency to commons CLI, so is a bit different from the two others.
However, we need to find a central class to perform the configuration of solvers: note that in sat package, the configuration of the solvers is done twice, one in DetailedCommandPanel and one in Launcher.