sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/issues2018-11-10T11:03:13Zhttps://gitlab.ow2.org/sat4j/sat4j/issues/149Instability of timeout based tests2018-11-10T11:03:13ZDaniel Le BerreInstability of timeout based testsIt is painful to have timeout based tests failing from time to time, breaking builds while there is no problem.
Just occurred today in https://gitlab.ow2.org/sat4j/sat4j/-/jobs/8082
We need to either find out why those tests do not take consistently the same time or get rid off the timeout!It is painful to have timeout based tests failing from time to time, breaking builds while there is no problem.
Just occurred today in https://gitlab.ow2.org/sat4j/sat4j/-/jobs/8082
We need to either find out why those tests do not take consistently the same time or get rid off the timeout!https://gitlab.ow2.org/sat4j/sat4j/issues/1Use a specific data structure for binary clauses compatible with reason simpl...2018-05-11T12:15:13ZDaniel Le BerreUse a specific data structure for binary clauses compatible with reason simplificationThe support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.https://gitlab.ow2.org/sat4j/sat4j/issues/2Allow iteration on MUS2018-05-11T12:15:13ZDaniel Le BerreAllow iteration on MUSOne new feature of release 2.3.0 is to compute minimal unsatisfiable subformulas. It is currently possible to compute on MUS. In some cases, it would make sense to compute all of them.
One specific iterator is needed for that purpose. One new feature of release 2.3.0 is to compute minimal unsatisfiable subformulas. It is currently possible to compute on MUS. In some cases, it would make sense to compute all of them.
One specific iterator is needed for that purpose. https://gitlab.ow2.org/sat4j/sat4j/issues/3Allow computation of prime implicants instead of models2018-05-11T12:15:13ZDaniel Le BerreAllow computation of prime implicants instead of modelsThe solver currently returns a model, i.e. a complete assignment of the boolean variables of the problem, that satisfies the constraints.
In some cases, a partial assignment that satisfies those constraints is needed (i.e. a prime implicant).
Providing a utility class that computes a prime implicant from a model could be a good way to provide that new feature to end users.The solver currently returns a model, i.e. a complete assignment of the boolean variables of the problem, that satisfies the constraints.
In some cases, a partial assignment that satisfies those constraints is needed (i.e. a prime implicant).
Providing a utility class that computes a prime implicant from a model could be a good way to provide that new feature to end users.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/5Global timeout not properly taken into account when optimizing solutions2018-05-11T12:15:13ZDaniel Le BerreGlobal timeout not properly taken into account when optimizing solutionsWhen optimizing a solution, the timeout should be global, not for each call to the issatisfiable() method.
This is taken into account thanks to the boolean parameter global in isSatisfiable(). If it is true, the timeout will not be reset at each time.
It looks like a problem appears when optimizing Eclipse solutions:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=336967
When optimizing a solution, the timeout should be global, not for each call to the issatisfiable() method.
This is taken into account thanks to the boolean parameter global in isSatisfiable(). If it is true, the timeout will not be reset at each time.
It looks like a problem appears when optimizing Eclipse solutions:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=336967
2.3.0https://gitlab.ow2.org/sat4j/sat4j/issues/6Allow iterating over all prime impliquants2018-05-11T12:15:13ZDaniel Le BerreAllow iterating over all prime impliquantsissue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover, not all prime implicants.
something specific need to be implemented for that task.issue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover, not all prime implicants.
something specific need to be implemented for that task.https://gitlab.ow2.org/sat4j/sat4j/issues/10allow ability to clone a solver2018-05-11T12:15:13Zemmanuel lonca emmanuel loncaallow ability to clone a solverneed to clone a solver to launch multiple instances of a solver to compute best utility on some optimization function for a single optimization problemneed to clone a solver to launch multiple instances of a solver to compute best utility on some optimization function for a single optimization problem2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/11Allow creation of ManyCore solver from a list/array of existing solvers inste...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of ManyCore solver from a list/array of existing solvers instead of their name in a factoryIt is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.It is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/13Compute minimal size unsat core2018-05-11T12:15:13ZDaniel Le BerreCompute minimal size unsat coreIt is currently possible to compute subset minimal unsat cores.
Some users would like to compute a size minimal unsat core.
It should not be too difficult to implement: just another strategy for the Xplain class.It is currently possible to compute subset minimal unsat cores.
Some users would like to compute a size minimal unsat core.
It should not be too difficult to implement: just another strategy for the Xplain class.2.3.3https://gitlab.ow2.org/sat4j/sat4j/issues/14After a call to expireTimeout(), a solver cannot be relaunched2018-05-11T12:15:13ZDaniel Le BerreAfter a call to expireTimeout(), a solver cannot be relaunchedOnce an expireTimeout() is performed, the solver state is in the "should stop" mode and a TimeoutException is launched whenever a call to isSatisfiable is performed.
The fix is simple: the expireTimeout should properly reset the solver state in such a way that subsequent calls to the solver (isSatisfiable() methods) are properly handled.
That issue as a nasty side effect on the MultiCore solver: it will prevent the various systems to be used after the first call to expireTimeout.Once an expireTimeout() is performed, the solver state is in the "should stop" mode and a TimeoutException is launched whenever a call to isSatisfiable is performed.
The fix is simple: the expireTimeout should properly reset the solver state in such a way that subsequent calls to the solver (isSatisfiable() methods) are properly handled.
That issue as a nasty side effect on the MultiCore solver: it will prevent the various systems to be used after the first call to expireTimeout.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/17Problem with isSatisfiable(VecInt)2018-05-11T12:15:13ZFabian BenduhnProblem with isSatisfiable(VecInt)ISolver.issatisfiable(VecInt) shows unexpected behavior.
ISolver.issatisfiable(VecInt) shows unexpected behavior.
2.3.1https://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.1https://gitlab.ow2.org/sat4j/sat4j/issues/19Allow creation of clauses, cardinality and pseudo boolean constraints using a...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of clauses, cardinality and pseudo boolean constraints using arrays of primitive typeWhen creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.When creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.https://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 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.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/23Optimization timeout2018-05-11T12:15:13ZDaniel Le BerreOptimization timeoutIn some cases, it is important to be able to limit the amount of time dedicated to the optimization, i.e. it is important to let the solver find a solution, but we would like to limit to a few seconds only the time to optimize the solution found.
In some cases, it is important to be able to limit the amount of time dedicated to the optimization, i.e. it is important to let the solver find a solution, but we would like to limit to a few seconds only the time to optimize the solution found.
2.3.3https://gitlab.ow2.org/sat4j/sat4j/issues/24Add statistics about SAT/UNSAT calls2018-05-11T12:15:13ZDaniel Le BerreAdd statistics about SAT/UNSAT callsWhen doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.When doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.https://gitlab.ow2.org/sat4j/sat4j/issues/25Allow input string to be read properly using InputStream or Reader2018-05-11T12:15:13ZDaniel Le BerreAllow input string to be read properly using InputStream or ReaderFor the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is not supported in some readers.
Not a big deal to fix, but need to be done properly.For the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is not supported in some readers.
Not a big deal to fix, but need to be done properly.https://gitlab.ow2.org/sat4j/sat4j/issues/26After adding and removing a clause in Xplain, subsequent addition of the clau...2018-05-11T12:15:13ZDaniel Le BerreAfter adding and removing a clause in Xplain, subsequent addition of the clause are ignoredIf someone tries to add several times a constraint that has just been added to the solver, Xplain will just ignore it.
This is problematic if the clause has been removed in the meanwhile.
A check need to be performed on clause removal.If someone tries to add several times a constraint that has just been added to the solver, Xplain will just ignore it.
This is problematic if the clause has been removed in the meanwhile.
A check need to be performed on clause removal.2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/29Mus computation does not work when input file contains duplicated contiguous ...2018-07-07T05:11:52ZDaniel Le BerreMus computation does not work when input file contains duplicated contiguous clauses (aka MUS competition bug)During the SAT 2011 competition MUS track, Sat4j MUS was found incorrect (i.e. the solution found was not an UNSAT core).
Those instances do contain unit clauses, so it is probably the case that Sat4j MUS does not output the unit clauses in the solution line because unit clauses are handled specifically in the solver.
That issue should not be difficult to handle.
Incorrect answers were found on the following benchmarks:
mus/marques-silva/product-configuration/C168_FW_UT_851.cnf
mus/marques-silva/design-debugging/c5315-bug-gate-0.dimacs.seq.filtered.cnf
mus/marques-silva/design-debugging/c7552-bug-gate-0.dimacs.seq.filtered.cnf
mus/marques-silva/equivalence-checking/c2670.cnf
During the SAT 2011 competition MUS track, Sat4j MUS was found incorrect (i.e. the solution found was not an UNSAT core).
Those instances do contain unit clauses, so it is probably the case that Sat4j MUS does not output the unit clauses in the solution line because unit clauses are handled specifically in the solver.
That issue should not be difficult to handle.
Incorrect answers were found on the following benchmarks:
mus/marques-silva/product-configuration/C168_FW_UT_851.cnf
mus/marques-silva/design-debugging/c5315-bug-gate-0.dimacs.seq.filtered.cnf
mus/marques-silva/design-debugging/c7552-bug-gate-0.dimacs.seq.filtered.cnf
mus/marques-silva/equivalence-checking/c2670.cnf
2.3.1https://gitlab.ow2.org/sat4j/sat4j/issues/30reset() method2018-07-07T05:11:52ZFatih Turkmenreset() methodThe reset() method in the context of MiniSAT and MaxSAT is not working properly. It is supposed to reset all settings (variables, clauses) but it does not so. For instance, after reset() call, calling nVar() returns the number of variables previously set.
Ps: For the MaxSAT, the problem seems to be fixed and it would appear in the new version but for MiniSAT, I am not aware of any attempt... The reset() method in the context of MiniSAT and MaxSAT is not working properly. It is supposed to reset all settings (variables, clauses) but it does not so. For instance, after reset() call, calling nVar() returns the number of variables previously set.
Ps: For the MaxSAT, the problem seems to be fixed and it would appear in the new version but for MiniSAT, I am not aware of any attempt...