sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-07-07T05:11:54Zhttps://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/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/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/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/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/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/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?