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 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/108Lack of 2.3.5 tag for sat4j2018-04-13T11:56:15ZKrzysztof DanielLack of 2.3.5 tag for sat4jThere is no tag in the repo for 2.3.5 release. This is a big problem for me as I can't rebuild sat4j in Fedora, and therefore can't build Eclipse.There is no tag in the repo for 2.3.5 release. This is a big problem for me as I can't rebuild sat4j in Fedora, and therefore can't build Eclipse.https://gitlab.ow2.org/sat4j/sat4j/-/issues/18ISolver.isSatisfiable(VecInt) is affected by previous call2018-05-11T12:15:13ZFabian BenduhnISolver.isSatisfiable(VecInt) is affected by previous callThe method ISolver.isSatisfiable(VecInt) is affected by previous calls which leads to unexpected results.The method ISolver.isSatisfiable(VecInt) is affected by previous calls which leads to unexpected results.2.3.1