sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-07-07T05:11:52Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/34Make sure that all solvers return a unit clause in addClause2018-07-07T05:11:52ZDaniel Le BerreMake sure that all solvers return a unit clause in addClauseIn many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.
However, especially in the simple SAT case, that behavior i...In many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.
However, especially in the simple SAT case, that behavior is not enforced for all DataStructureFactory.
We thus need to make sure that all DSF do return a UnitClause object instead of null when a unit clause is detected.
2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/39Add the possibility to create a constraint k among n in IProblem2018-07-07T05:11:53ZDaniel Le BerreAdd the possibility to create a constraint k among n in IProblemIn the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.
The current way to proceed in Sat4j is to create both a <= and a >= constraints.
T...In the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.
The current way to proceed in Sat4j is to create both a <= and a >= constraints.
That's fine. However, there are possibilities to encode directly such kind of constraints in the solver.
As such, it would be great to provide a new method for that in the API, even if the current implementation remains unchanged.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/41Use a specific data structure to locate efficiently the weight associated to ...2018-07-07T05:11:53ZDaniel Le BerreUse a specific data structure to locate efficiently the weight associated to a literal in a counter based constraintAfter checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals
int indiceP = 0;
while ((lits[ind...After checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals
int indiceP = 0;
while ((lits[indiceP] ^ 1) != p)
indiceP++;
Using an auxiliary array or map to store the location of the literals instead of going through that loop will probably make the propagation and undo much faster.
(hint: use an array when the size of the constraint contains at least half of the variables, else use a map).2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/42Allow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others)...2018-07-07T05:11:53ZDaniel Le BerreAllow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others) compressed filesBenchmarks take more and more space, so they are usually stored in a compressed form.
Java has a built in support for zip file, but not for bz2 files.
One pragmatic way to add support for bz2 (and maybe 7z compressed files), is to use p...Benchmarks take more and more space, so they are usually stored in a compressed form.
Java has a built in support for zip file, but not for bz2 files.
One pragmatic way to add support for bz2 (and maybe 7z compressed files), is to use platform specific decoders, e.g. bunzip2 on unix platform.
This is how abscon is managing bz2 files, and it works fine for both Linux and Mac Os X.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/43Allow the solver to be aware of the user defined max var id2018-07-07T05:11:53ZDaniel Le BerreAllow the solver to be aware of the user defined max var idWhen using SAT encodings, it is often necessary to create new variables on the fly.
This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.
In that context, it is important to make a difference between th...When using SAT encodings, it is often necessary to create new variables on the fly.
This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.
In that context, it is important to make a difference between the original max var id
and the maxvarid after adding the new variables.
It is assumed in most cases in Sat4j that the user defined maxvarid is defined using the method
ISolver.newVar(int maxvarid)
Then new variables can be retrieved using nextFreeVarId().
We could for instance fix the value set using newVar() and add a method to retrieve it.
That way, the model iterator for instance could use that value instead of the current nVar().2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/45Separate MS and PWMS decorator from the optimization method2018-07-07T05:11:53ZDaniel Le BerreSeparate MS and PWMS decorator from the optimization methodSince we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the probl...Since we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the problem, it should delegate that to a PseudoOptDecorator or a ConstraintRelaxingPseudoOptDecorator.
Since we use here new variables, it means updating the current pseudo-opt decorators to deal with additional variables.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/4Provide a representation of pseudo boolean constraints with primitive type lo...2018-05-11T12:15:13ZDaniel Le BerreProvide a representation of pseudo boolean constraints with primitive type long instead of BigIntegerPseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those const...Pseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those constraints, to efficiently propagate truth values.
One could choose either int or long for that.
long is probably a good tradeoff between the space required to store the information and the number of cases in which it will apply. Since we are going to 64 bits arch, long should be handled natively by the JVMs at some point.2.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/36Allow pretty printing of solutions2018-07-07T05:11:53ZDaniel Le BerreAllow pretty printing of solutionsWe currently generate very long lines with the solution of the problem (SAT, PB or MAXSAT).
We have OutOfMemory problems when displaying a solution after a OOM exception has ben launched.
It would probably not happen is the output stre...We currently generate very long lines with the solution of the problem (SAT, PB or MAXSAT).
We have OutOfMemory problems when displaying a solution after a OOM exception has ben launched.
It would probably not happen is the output stream is flushed regularly, i.e. after a limited amount of literals in the solution line.
It would therefore be nice to have a way to pretty print the solution line.
The only issue is that it may break scripts that simply do a grep to retrieve the solution.https://gitlab.ow2.org/sat4j/sat4j/-/issues/72Print the statistics of all solvers in manycore2018-04-13T11:56:15ZDaniel Le BerrePrint the statistics of all solvers in manycoreCurrently, only the statistics of the winner are displayed. We should display the statistics of all solvers.Currently, only the statistics of the winner are displayed. We should display the statistics of all solvers.https://gitlab.ow2.org/sat4j/sat4j/-/issues/90Better management of forgotten variables for undo-based constraints2018-04-13T11:56:17ZDaniel Le BerreBetter management of forgotten variables for undo-based constraintsSat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
...Sat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
However, there is an issue for constraints requiring a call to undo when backtracking.
The constraints to be considered when undoing an assignment is stored for a variable, not a literal. As such, when forgetting a variable, both the constraints where the positive and negative literal appears are part of that constraint. So a call to undo() on a constraint that does contains the literal will occur.
Worst, it is necessary to perform the undo both on the literal and its oppositve in that case, to properly undo all constraints.
In our testcases, the PB constraints are encoding the objective function and are deleted after each PI computation, so the current fix is simply to avoid a NPE that occurs when the undo() method is applied on a constraint not associated by such literal.
We are currently working on a new PI computation scheme, so that code with forget will eventually be removed. The current fix allows the solver to be correct, and prevents NPE to occur.