SAT4J issueshttps://gitlab.ow2.org/groups/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/174Cardinality detector statistics are incorrect2023-10-12T10:23:39ZDaniel Le BerreCardinality detector statistics are incorrectWhen launching DetectCards on a PHP 200 instance, the solve provides the following output:
```
c declared #vars 40200
c #constraints 201
c constraints type
c org.sat4j.pb.constraints.pb.OriginalHTClausePB => 201
c 201 constraints ...When launching DetectCards on a PHP 200 instance, the solve provides the following output:
```
c declared #vars 40200
c #constraints 201
c constraints type
c org.sat4j.pb.constraints.pb.OriginalHTClausePB => 201
c 201 constraints processed.
c launching cardinality constraint revelation process
c remaining constraints: 0/4020000
c cardinality constraints found (preprocessing): 200
c cardinality search time (preprocessing): 14648ms
c found 200 at-most cardinality constraint of degree 200 and size 201
c solver contains 401 constraints
```
The main issue is that the at-most cardinality constraint should be of degree 1, not 200. Internally, the constraint is an AtLeastCard, so the degree should be size-degree to fix that. However, changing the computation of the degree in PreprocCardConstrLearningSolver line 348 does not seem to fix the problem.
Another (small) issue is that the number of constraints is not correct. According to the logs, there was 4020000 clauses originally. This is the number with would have expected instead of 201.Emmanuel LoncaEmmanuel Loncahttps://gitlab.ow2.org/sat4j/sat4j/-/issues/173Unnecessary code to remove in the DAC_meanLearnedDegree branch2023-01-30T10:38:35ZAlain KemgueUnnecessary code to remove in the DAC_meanLearnedDegree branchUnnecessary [code](https://gitlab.ow2.org/sat4j/sat4j/-/blob/DAC_meanLearnedDegree/train_dqn.py#L643-L659) to remove in the next push.Unnecessary [code](https://gitlab.ow2.org/sat4j/sat4j/-/blob/DAC_meanLearnedDegree/train_dqn.py#L643-L659) to remove in the next push.https://gitlab.ow2.org/sat4j/sat4j/-/issues/172Fix manifest metadata to contain only the one applicable2022-07-31T06:31:36ZDaniel Le BerreFix manifest metadata to contain only the one applicableThe current jars files of Sat4j used as osgi bundles or as executable jar files are currently sharing the same static manifest files.
The osgi bundles are generated using maven.
The executable jar files using ant.
The latter requires ...The current jars files of Sat4j used as osgi bundles or as executable jar files are currently sharing the same static manifest files.
The osgi bundles are generated using maven.
The executable jar files using ant.
The latter requires a classpath entry which currently generates warnings in eclipse build (see [issue 146](https://github.com/eclipse-platform/eclipse.platform.releng.aggregator/issues/416)).
To avoid this, the manifest files should be adapted to the target usage of the jar files.Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/171Make Sat4j 3.0 a set of Java modules2023-04-29T18:01:55ZDaniel Le BerreMake Sat4j 3.0 a set of Java modulesWith release 3.0, we want to deliver Sat4j as separate Java modules.
The main issue is to be able to build executable jars for the end users of SAT, PB or MAXSAT solvers.
#142 has initiated the discussion 3 years ago.
This work will b...With release 3.0, we want to deliver Sat4j as separate Java modules.
The main issue is to be able to build executable jars for the end users of SAT, PB or MAXSAT solvers.
#142 has initiated the discussion 3 years ago.
This work will be performed on a separate branch by @romain_wallon and @lonca until we find a reasonable solution (i.e. easy to use jar files from the command line for the end user).https://gitlab.ow2.org/sat4j/sat4j/-/issues/169Global time-based timer are not canceled2021-10-07T05:52:49ZDaniel Le BerreGlobal time-based timer are not canceledin #55 @puzzler reported memory out when creating many Sat4j solvers with a model iterator.
After investigation, the issue is that the model iterator enforces a global timeout in the solver. In that case, the internal Timer object is ne...in #55 @puzzler reported memory out when creating many Sat4j solvers with a model iterator.
After investigation, the issue is that the model iterator enforces a global timeout in the solver. In that case, the internal Timer object is never canceled, which prevents Sat4j objects to be garbage collected.
The workaround is to use a conflict based timeout in that case.
To prevent similar issue in the future, we could:
- use a conflict-based timer by default
- do not force global timeout for model iterator
- ...
The issue requires further investigation.Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/167Fix displayed information when revealing cardinality constraints2021-03-30T08:38:34ZDaniel Le BerreFix displayed information when revealing cardinality constraintsWhen revealing cardinality constraints, the information displayed is not accurate.
See e.g. for a pigeon hole 3-4 problem:
```
c solving ph3-4.cnf
c reading problem ...
c ... done. Wall clock time 0.01s.
c declared #vars 12
c #con...When revealing cardinality constraints, the information displayed is not accurate.
See e.g. for a pigeon hole 3-4 problem:
```
c solving ph3-4.cnf
c reading problem ...
c ... done. Wall clock time 0.01s.
c declared #vars 12
c #constraints 0
c constraints type
c 0 constraints processed.
c launching cardinality constraint revelation process
c remaining constraints: 4/22
c cardinality constraints found (preprocessing): 3
c cardinality search time (preprocessing): 11ms
c found 3 at-most cardinality constraint of degree 1 and size 4
c solver contains 7 constraints
```
The `#constraints` and `constraints processed` are not accurate.https://gitlab.ow2.org/sat4j/sat4j/-/issues/166Add a way to reveal the cardinality constraints found by DetectCards2021-03-30T08:35:51ZDaniel Le BerreAdd a way to reveal the cardinality constraints found by DetectCardsThe only way current to display those constraints is to use a specific launcher:
```
java -Dprintcards=true -cp sat4j-pb.jar org.sat4j.pb.CardConstrLearningSolverLauncher file.cnf
```
It would be nice to have that information displayed...The only way current to display those constraints is to use a specific launcher:
```
java -Dprintcards=true -cp sat4j-pb.jar org.sat4j.pb.CardConstrLearningSolverLauncher file.cnf
```
It would be nice to have that information displayed using the more classical
```
java -jar sat4j-pb.jar DetectCards file.cnf
```https://gitlab.ow2.org/sat4j/sat4j/-/issues/165Missing negated literals in dedicated watch structure for computing prime imp...2021-03-03T06:53:03ZDaniel Le BerreMissing negated literals in dedicated watch structure for computing prime implicantsIn the enclosed CNF file, the default prime implicant computation strategy displays as prime implicant
v 2 3 4 5 6 0
while the two others display
v 2 3 4 5 6 -21 -22 -24 -25 -26 -27 0
All output should always be the same.
[Q3inK08.c...In the enclosed CNF file, the default prime implicant computation strategy displays as prime implicant
v 2 3 4 5 6 0
while the two others display
v 2 3 4 5 6 -21 -22 -24 -25 -26 -27 0
All output should always be the same.
[Q3inK08.cnf](/uploads/2a9c1cb835ee96b61f66655dbe116ef2/Q3inK08.cnf)Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/163MaxHSLike solver won't launch from command line2021-02-19T21:06:16ZRomain WALLONMaxHSLike solver won't launch from command lineCurrently, the way the `MaxHSLike` solver is instantiated and initialized in the MaxSAT launcher does not allow the solver to be fed with the constraints of the problem, so that the solver does not know these constraints when `isSatisifi...Currently, the way the `MaxHSLike` solver is instantiated and initialized in the MaxSAT launcher does not allow the solver to be fed with the constraints of the problem, so that the solver does not know these constraints when `isSatisifiable()` is invoked.https://gitlab.ow2.org/sat4j/sat4j/-/issues/162Provide access to decisions taken during the search in the API2021-02-22T21:14:58ZDaniel Le BerreProvide access to decisions taken during the search in the APIThere are several use cases in which it can be useful to know which decisions have been taken
to obtain a given model.
That information is currently available inside the Solver class, but not available in the API.
It is used to "block" ...There are several use cases in which it can be useful to know which decisions have been taken
to obtain a given model.
That information is currently available inside the Solver class, but not available in the API.
It is used to "block" a given model by adding a clause made of the negation of the decision literals.
Providing access to those decisions may allow the user to perform e.g. projected enumeration.
Providing public access to those decisions may require:
- [x] provide a new method in the API to access those decisions
- [ ] to move the current code of `Solver.createBlockingClauseForCurrentModel` to another place (`ModelIterator`?)
- [ ] optionally extend the `ModelIterator` class to support projected model enumerationDaniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/moco/-/issues/2Reference set crash2020-06-23T23:54:50ZMiguel TavaresReference set crashLoss of precision with doubles creates a bug when creating the reference setLoss of precision with doubles creates a bug when creating the reference sethttps://gitlab.ow2.org/sat4j/moco/-/issues/1Division by 02020-06-23T23:48:03ZMiguel TavaresDivision by 0The "evaluate" function in the "DivObj" file does not deal with division by 0.The "evaluate" function in the "DivObj" file does not deal with division by 0.https://gitlab.ow2.org/sat4j/sat4j/-/issues/160Refactor LearnedConstraintDeletionStrategy management2020-03-11T14:33:06ZDaniel Le BerreRefactor LearnedConstraintDeletionStrategy managementThe way LearnedConstraintDeletionStrategy strategy design pattern is implemented currently is not satisfactory: each strategy is created once in each solver. Only one should be instantiated.
We need to find a better way to handle both t...The way LearnedConstraintDeletionStrategy strategy design pattern is implemented currently is not satisfactory: each strategy is created once in each solver. Only one should be instantiated.
We need to find a better way to handle both the timers required for LCDS and the strategies themselves.https://gitlab.ow2.org/sat4j/sat4j/-/issues/159Update continuous integration settings to build correctly for contributors2020-01-03T15:12:34ZDaniel Le BerreUpdate continuous integration settings to build correctly for contributorsWhen the project is forked, the CI build does not work due to credentials issue.
The build should work off-the-shelves when forking.When the project is forked, the CI build does not work due to credentials issue.
The build should work off-the-shelves when forking.https://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/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 Berre