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