sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-05-11T12:15:13Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/8Allow iterating over optimal solutions2018-05-11T12:15:13ZDaniel Le BerreAllow iterating over optimal solutionsThe solver is not properly cleaned up once an optimal solution is found.
Literals propagated at decision level 0 by pseudo boolean constraints used during the optimization are not properly removed.
While this does not affect our major t...The solver is not properly cleaned up once an optimal solution is found.
Literals propagated at decision level 0 by pseudo boolean constraints used during the optimization are not properly removed.
While this does not affect our major tools (PB or MAXSAT solvers) since they aim only at finding one optimal solution, it is an issue when one wants to find several optimal solutions. See TestLonca to see the problem in action.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/9Trivial inconsistency in cardinality constraints not properly handled2018-05-11T12:15:13ZDaniel Le BerreTrivial inconsistency in cardinality constraints not properly handledWhen doing optimization with cardinality constraints (at least), at some point the degree of the constraint is strictly bigger than the number of literals in the constraints. In that case, the constraint cannot be satisfied:
x& + x2 + x3...When doing optimization with cardinality constraints (at least), at some point the degree of the constraint is strictly bigger than the number of literals in the constraints. In that case, the constraint cannot be satisfied:
x& + x2 + x3 >= 4 cannot be satisfied.
As such, sat4j should throw a ContradictionException when that constraint is created.
While it is the case in the AtLeast implementation of the card constraint, it is not the case for MaxWatchPb and MinWatchPb. 2.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/10allow ability to clone a solver2018-05-11T12:15:13ZEmmanuel 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/12Use List instead of IVec in DependencyHelper.getSolution()2018-05-11T12:15:13ZDaniel Le BerreUse List instead of IVec in DependencyHelper.getSolution()Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to...Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to interact with that class.
We could use for instance a java.util.List object instead of an IVec.
The main issue here is that it would break the API: the DependencyHelper class exists since Sat4j 2.1.
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 ...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/15Allow to reset the DependencyHelper2018-05-11T12:15:13ZDaniel Le BerreAllow to reset the DependencyHelperThere is currently no way to reset a DependencyHelper. In some cases, it might be useful to reset it, i.e. to clear its mapping, objective function and solver.There is currently no way to reset a DependencyHelper. In some cases, it might be useful to reset it, i.e. to clear its mapping, objective function and solver.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/16Order of added constraints affects the results of RemiUtils2018-05-11T12:15:13ZSebastian HennebergOrder of added constraints affects the results of RemiUtilsThe order in which the pseudo boolean constraints are added to the solver affects the result of RemiUtils which should not be the case in my opinion. I found out that the constraint that will be added at first causes the problem. If this...The order in which the pseudo boolean constraints are added to the solver affects the result of RemiUtils which should not be the case in my opinion. I found out that the constraint that will be added at first causes the problem. If this constraint is added later, the expected result will be returned ("4,5,6"). Otherwise RemiUtils.backbone() returns "4,5" which is obviously wrong because the constraint "+1 x6 >= 1" requires literal 6 to be true in all satisfying assignments.
- Sebastian2.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/20Allow creation of soft constraints in a specific GateTranslator2018-05-11T12:15:13ZDaniel Le BerreAllow creation of soft constraints in a specific GateTranslatorSat4j provides a utility class GateTranslator to translate logical gate to CNF.
Some people would like to be able to use a similar class to produce weighted CNF, to be solved with a MAXSAT solver.
It should not be difficult to create a...Sat4j provides a utility class GateTranslator to translate logical gate to CNF.
Some people would like to be able to use a similar class to produce weighted CNF, to be solved with a MAXSAT solver.
It should not be difficult to create a subclass of GateTranslator to provide that functionality in the maxsat package.https://gitlab.ow2.org/sat4j/sat4j/-/issues/21Error in method toString() of OPBStringSolver for negative literals2018-05-11T12:15:13ZStéphanie ROUSSELError in method toString() of OPBStringSolver for negative literalsWhen adding a constraint with negative literals to an OPBStringSolver , its method toString() generates a opb file with unexpected indices for these negative literals.
More precisely, instead of generating -1 x1 +1 x2 as it could be expe...When adding a constraint with negative literals to an OPBStringSolver , its method toString() generates a opb file with unexpected indices for these negative literals.
More precisely, instead of generating -1 x1 +1 x2 as it could be expected in the attached example, it generates +1 x-1 +1 x2.2.3.1https://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 exc...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 soluti...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 ...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/27PMaxSAT Solving2018-05-11T12:15:13ZFatih TurkmenPMaxSAT SolvingWhen solving PMaxSAT problems, if there is no soft clause, the method isSatisfiable() works fine, i.e. it returns true, but the method model() throws a IllegalStateException even if there is a solution. I thought that the MaxSAT solver w...When solving PMaxSAT problems, if there is no soft clause, the method isSatisfiable() works fine, i.e. it returns true, but the method model() throws a IllegalStateException even if there is a solution. I thought that the MaxSAT solver would behave exactly like MiniSATSolver when there is no soft clause but seems not.
Moreover, the ModelIterator is used to iterate over models obtained from any SAT (e.g. MiniSAT or MaxSAT) solver. I think this requires a special attention in the case of MaxSAT solving...
I attached an automatically generated CNF file for testing purposes although it seems easy to regenerate the problem.2.3.1