sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2019-08-20T08:36:34Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/158Fix new violation considered as a bug in SonarQube2019-08-20T08:36:34ZDaniel Le BerreFix new violation considered as a bug in SonarQubeA recent update of SonarQube has introduced a new violation considered as a bug:
https://sonarqube.ow2.org/project/issues?id=org.ow2.sat4j%3Aorg.ow2.sat4j.pom&resolved=false&types=BUG
Refactor this code so that the Iterator supports mul...A recent update of SonarQube has introduced a new violation considered as a bug:
https://sonarqube.ow2.org/project/issues?id=org.ow2.sat4j%3Aorg.ow2.sat4j.pom&resolved=false&types=BUG
Refactor this code so that the Iterator supports multiple traversal, aka iterator() method should not return this.
There are three cases in which it happens, related to multi-criteria optimization. It would be nice to fix this before 2.3.6 release.Emmanuel LoncaEmmanuel Loncahttps://gitlab.ow2.org/sat4j/sat4j/-/issues/156some small problems in fileName-handling2019-06-23T16:22:04ZDieter von Holtensome small problems in fileName-handlinga recent message in Twitter '... the upcoming new release of Sat4J ... ' activated me to throw in a fix from my codebase:
in method `parseInstance()` there are two small problems - see comments in lines 107 - 117.
[InstanceReader.java]...a recent message in Twitter '... the upcoming new release of Sat4J ... ' activated me to throw in a fix from my codebase:
in method `parseInstance()` there are two small problems - see comments in lines 107 - 117.
[InstanceReader.java](/uploads/1247974b5e53b73bc9b132f0e5329890/InstanceReader.java)https://gitlab.ow2.org/sat4j/sat4j/-/issues/155Provide a way to serialize constraints in files2023-03-11T18:46:20ZDaniel Le BerreProvide a way to serialize constraints in filesThe current `toString()` method is mainly used for debugging purpose. We need currently a way to dump constraints in a textual format which can be used to recover the constraint later on.
The proposal is to add a new method `dump()` in ...The current `toString()` method is mainly used for debugging purpose. We need currently a way to dump constraints in a textual format which can be used to recover the constraint later on.
The proposal is to add a new method `dump()` in `IConstr` and in `IProblem` to allow dumping an object to either a Dimacs of OPB file.
There are a lot of corner cases, especially regarding unit clauses.
It will require a lot of testing before being released.https://gitlab.ow2.org/sat4j/sat4j/-/issues/153Bug when mixing constraint removal and constraints satisfied by unit propagation2019-01-27T15:32:36ZMiguel NevesBug when mixing constraint removal and constraints satisfied by unit propagationHi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation.
In particular, the bug is triggered by the following sequence of operations:
- add constra...Hi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation.
In particular, the bug is triggered by the following sequence of operations:
- add constraints (x1 + x2 + x3 <= 2), (x1 + x2 >= 2) and (not(x2) v not(x3))
- check satisfiability: formula is SAT, as expected
- remove (x1 + x2 >= 2)
- add (x2 + x3 >= 2): this should contradict (not(x2) v not(x3)), but no exception is thrown
- check satisfiability: formula should be UNSAT, but SAT is returned instead
I have attached a small Java program that follows this sequence of operations, triggering the bug.
Best regards,
Miguel Neves
[SatByUnitBug.java](/uploads/f36125668baadf4011b0cf998bac3a42/SatByUnitBug.java)https://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/148ArrayIndexOutOfBound exception on non normalized WBO opb file2018-10-29T16:44:23ZDaniel Le BerreArrayIndexOutOfBound exception on non normalized WBO opb fileIn WBO, non normalized constraints cause an ArrayIndexOutOfBoundsException:
```
java -jar dist/CUSTOM/sat4j-pb.jar CuttingPlanes ~/Downloads/bugpourevocrash2.opb
```
```
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsExcepti...In WBO, non normalized constraints cause an ArrayIndexOutOfBoundsException:
```
java -jar dist/CUSTOM/sat4j-pb.jar CuttingPlanes ~/Downloads/bugpourevocrash2.opb
```
```
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 6
at org.sat4j.core.Vec.get(Vec.java:239)
at org.sat4j.pb.constraints.pb.InternalMapPBStructure.get(InternalMapPBStructure.java:102)
at org.sat4j.pb.constraints.pb.ConflictMap.isImplyingLiteral(ConflictMap.java:621)
at org.sat4j.pb.constraints.pb.ConflictMap.isAssertive(ConflictMap.java:583)
at org.sat4j.pb.core.PBSolverCP.analyzeCP(PBSolverCP.java:141)
at org.sat4j.pb.core.PBSolverCP.analyze(PBSolverCP.java:129)
at org.sat4j.minisat.core.Solver.search(Solver.java:1320)
at org.sat4j.minisat.core.Solver.isSatisfiable(Solver.java:1824)
at org.sat4j.tools.SolverDecorator.isSatisfiable(SolverDecorator.java:115)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:179)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:172)
at org.sat4j.OptimizationMode.solve(OptimizationMode.java:121)
at org.sat4j.AbstractLauncher.solve(AbstractLauncher.java:318)
at org.sat4j.AbstractLauncher.run(AbstractLauncher.java:257)
at org.sat4j.pb.LanceurPseudo2007.main(LanceurPseudo2007.java:97)
```
[bugpourevocrash.opb](/uploads/3a9ca6ffde44f1a136d337ba86ded8c5/bugpourevocrash.opb)https://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/1Use a specific data structure for binary clauses compatible with reason simpl...2018-05-11T12:15:13ZDaniel Le BerreUse a specific data structure for binary clauses compatible with reason simplificationThe support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because th...The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.https://gitlab.ow2.org/sat4j/sat4j/-/issues/6Allow iterating over all prime impliquants2018-05-11T12:15:13ZDaniel Le BerreAllow iterating over all prime impliquantsissue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover...issue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover, not all prime implicants.
something specific need to be implemented for that task.https://gitlab.ow2.org/sat4j/sat4j/-/issues/19Allow creation of clauses, cardinality and pseudo boolean constraints using a...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of clauses, cardinality and pseudo boolean constraints using arrays of primitive typeWhen creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.When creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.https://gitlab.ow2.org/sat4j/sat4j/-/issues/20Allow creation of soft constraints in a specific GateTranslator2018-05-11T12:15:13ZDaniel Le BerreAllow creation of soft constraints in a specific GateTranslatorSat4j provides a utility class GateTranslator to translate logical gate to CNF.
Some people would like to be able to use a similar class to produce weighted CNF, to be solved with a MAXSAT solver.
It should not be difficult to create a...Sat4j provides a utility class GateTranslator to translate logical gate to CNF.
Some people would like to be able to use a similar class to produce weighted CNF, to be solved with a MAXSAT solver.
It should not be difficult to create a subclass of GateTranslator to provide that functionality in the maxsat package.https://gitlab.ow2.org/sat4j/sat4j/-/issues/22DependencyHelper (the solvers in general) behave differently when units are s...2018-05-11T12:15:13ZDaniel Le BerreDependencyHelper (the solvers in general) behave differently when units are set first or set lastThe DependencyHelper behavior can look strange to newcomer since its behavior depends of the order of the constraints.
SAT power users use that order to let the solver perform as much simplification as possible.
Here, we receive an exc...The DependencyHelper behavior can look strange to newcomer since its behavior depends of the order of the constraints.
SAT power users use that order to let the solver perform as much simplification as possible.
Here, we receive an exception when the constraints are simplified.
Several options are available:
- do not fix, its a feature, not a bug
- fix be ignoring simplified constraints => no more control of what's going on in the helper, might be error prone
- fix by delegating unit to be the last thing added to the solver: the helper acts as a proxy here. => no more power user control of the helper.
Need to think about it.https://gitlab.ow2.org/sat4j/sat4j/-/issues/24Add statistics about SAT/UNSAT calls2018-05-11T12:15:13ZDaniel Le BerreAdd statistics about SAT/UNSAT callsWhen doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.When doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.https://gitlab.ow2.org/sat4j/sat4j/-/issues/25Allow input string to be read properly using InputStream or Reader2018-05-11T12:15:13ZDaniel Le BerreAllow input string to be read properly using InputStream or ReaderFor the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is ...For the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is not supported in some readers.
Not a big deal to fix, but need to be done properly.https://gitlab.ow2.org/sat4j/sat4j/-/issues/28Allow easy explanation for OPB file2022-04-09T17:42:39ZDaniel Le BerreAllow easy explanation for OPB fileCurrently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to...Currently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to easily display the unsat core in terms of constraints number (might not be that good because an equality constraint is splitted into 2 constraints).https://gitlab.ow2.org/sat4j/sat4j/-/issues/46Add an API to reduce the value of the objective function in case of optimization2018-05-11T12:15:13ZDaniel Le BerreAdd an API to reduce the value of the objective function in case of optimizationWhen we do optimization using strengthening, we decrease the value of an atMostK constraint, corresponding to the best upper bound of the objective function.
When using CNF translation of AtMostK, this is done only by setting some boole...When we do optimization using strengthening, we decrease the value of an atMostK constraint, corresponding to the best upper bound of the objective function.
When using CNF translation of AtMostK, this is done only by setting some boolean variables.
It is currently not easy to know when that value is reduced, thus it is not possible to take advantage of the CNF translation.
https://gitlab.ow2.org/sat4j/sat4j/-/issues/47Fix NPE when solver is killed by the competition framework while the solver c...2018-05-11T12:15:13ZDaniel Le BerreFix NPE when solver is killed by the competition framework while the solver cleans up the learned clausesWhen the competition framework stops the solver, a new thread is created, which displays some stats about learned clauses.
If the solver is cleaning up the set of learned clauses at that moment, the solver will throw an NPE, because the...When the competition framework stops the solver, a new thread is created, which displays some stats about learned clauses.
If the solver is cleaning up the set of learned clauses at that moment, the solver will throw an NPE, because the iterator on the learned clauses will try to access a constraint that has been removed.
We need to find a nice fix for that problem that will not slows down the solver during the search.
The issue mainly appears in the MAXSAT evaluation, in which the size of the benchmarks is small, thus the cleaning of the learned constraints very frequent because of the "wall" feature.https://gitlab.ow2.org/sat4j/sat4j/-/issues/49Allow the creation of a new variable with a hint for preferred branching pola...2018-05-11T12:15:13ZDaniel Le BerreAllow the creation of a new variable with a hint for preferred branching polarityCurrently, the user can ask for the creation of a new variable in the solver using nextFreeVarId().
In some cases, depending of what the variable represents, it might help to give a hint to the solver of the truth value to branch first o...Currently, the user can ask for the creation of a new variable in the solver using nextFreeVarId().
In some cases, depending of what the variable represents, it might help to give a hint to the solver of the truth value to branch first on.
overloading the nextFreeVarId() method to provide such feature would be nice.https://gitlab.ow2.org/sat4j/sat4j/-/issues/52Add usage of Lower bounding to MaxSat2018-05-11T12:15:13ZDaniel Le BerreAdd usage of Lower bounding to MaxSatA lower bounding procedure is available in Sat4j API since release 2.3.1.
It would be nice to have the ability to use it on the command line of the maxsat solver.A lower bounding procedure is available in Sat4j API since release 2.3.1.
It would be nice to have the ability to use it on the command line of the maxsat solver.https://gitlab.ow2.org/sat4j/sat4j/-/issues/53Allow both lower and upper bounding on the ManyCore solvers.2018-05-11T12:15:13ZDaniel Le BerreAllow both lower and upper bounding on the ManyCore solvers.We already shipped parallel solvers with both Resolution and Cutting Planes. It would be nice to have both Lower Bound and Upper Bounding done in parallel. This is not possible currently, since parallel optimizers do cooperate to compute...We already shipped parallel solvers with both Resolution and Cutting Planes. It would be nice to have both Lower Bound and Upper Bounding done in parallel. This is not possible currently, since parallel optimizers do cooperate to compute the best upper bound currently. The parallelization need to move to a higher level to allow this.