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.0