sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-05-11T12:15:13Zhttps://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/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.
https://gitlab.ow2.org/sat4j/sat4j/-/issues/57Add a way to ask the solver to stop searching after a given decision level is...2018-05-11T12:15:13ZDaniel Le BerreAdd a way to ask the solver to stop searching after a given decision level is reachedIn some cases it might be might to tell the solver to abort the search when a given decision level is reached.
There are several possibilities to implement that:
- restart when a decision level limit is found, i.e. stop the current expl...In some cases it might be might to tell the solver to abort the search when a given decision level is reached.
There are several possibilities to implement that:
- restart when a decision level limit is found, i.e. stop the current exploration
- stop the search, i.e. abort completely the process (would throws a TimeoutException).
https://gitlab.ow2.org/sat4j/sat4j/-/issues/74Make Sat4j easily usable in Scala2018-05-11T12:15:13ZDaniel Le BerreMake Sat4j easily usable in ScalaScala has some conventions for methods and fields that are different from usual Java ones.
It might be a good idea to complete the current API to make the integration of Sat4j inside scala programs seemingless.
Scala has some conventions for methods and fields that are different from usual Java ones.
It might be a good idea to complete the current API to make the integration of Sat4j inside scala programs seemingless.
3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/51Allow usage of Lower Bounding on Sat4j PB command line2018-07-07T05:11:53ZDaniel Le BerreAllow usage of Lower Bounding on Sat4j PB command lineIn Sat4J 2.3.1, a lower bounding procedure was made available in the API.
That feature is not available in the PB command line.
It would be nice to add it to the PB command line.In Sat4J 2.3.1, a lower bounding procedure was made available in the API.
That feature is not available in the PB command line.
It would be nice to add it to the PB command line.2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/113Lower bounding optimization does not work for maxsat2018-04-13T11:56:13ZDaniel Le BerreLower bounding optimization does not work for maxsatWhen using the lower bounding technique on a maxsat problem, the solver does not stop when the formula becomes satisfiable.
The enclosed wcnf has an optimal solution of 400, found using upper bounding, but not found using lower bounding.When using the lower bounding technique on a maxsat problem, the solver does not stop when the formula becomes satisfiable.
The enclosed wcnf has an optimal solution of 400, found using upper bounding, but not found using lower bounding.2.3.6