sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-07-07T05:11:52Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/32Tautological PB constraints with no literals incorrectly considered asempty c...2018-07-07T05:11:52ZDaniel Le BerreTautological PB constraints with no literals incorrectly considered asempty clausesWhen creating PB constraints with no literal and a degree of 0 or -1 for instance, the solver launches a contradiction exception while it should just ignore those constraints.
This is particularly annoying when doing optimization.When creating PB constraints with no literal and a degree of 0 or -1 for instance, the solver launches a contradiction exception while it should just ignore those constraints.
This is particularly annoying when doing optimization.2.3.1https://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/35LexicoHelper constructors are incorrect when explain option is set to true2018-07-07T05:11:53ZDaniel Le BerreLexicoHelper constructors are incorrect when explain option is set to trueThe LexicoHelper class keeps track of the PBSolverDecorator used in the LexicoDecorator object.
The object gathered when setting the xplain flag to true is not a PBSolverDecorator but an XplainPB.
As such, an exception is launched when t...The LexicoHelper class keeps track of the PBSolverDecorator used in the LexicoDecorator object.
The object gathered when setting the xplain flag to true is not a PBSolverDecorator but an XplainPB.
As such, an exception is launched when the explanation is enabled.
See here a trace of the error shown in p2cudf:
org.sat4j.pb.tools.XplainPB cannot be cast to org.sat4j.pb.PBSolverDecorator
Exception in thread "Thread-0" java.lang.NullPointerException
at org.eclipse.equinox.p2.cudf.solver.Projector.stopSolver(Projector.java:490)
at org.eclipse.equinox.p2.cudf.solver.SimplePlanner.stopSolver(SimplePlanner.java:61)
at org.eclipse.equinox.p2.cudf.Main$1.run(Main.java:55)2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/37Unit clauses not propagated again when doing multiple calls to the SAT solver2018-07-07T05:11:53ZDaniel Le BerreUnit clauses not propagated again when doing multiple calls to the SAT solverThe issue was described by Axel on SAT4J forum:
http://forge.ow2.org/forum/message.php?msg_id=118089
The short story is that unit clauses, after being propagated once, are no longer propagated on successive calls to the SAT solver becau...The issue was described by Axel on SAT4J forum:
http://forge.ow2.org/forum/message.php?msg_id=118089
The short story is that unit clauses, after being propagated once, are no longer propagated on successive calls to the SAT solver because qhead was not reset to 0 but to trail.last().
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/40Random Walk Decorator disable Objective Function based heuristics2018-07-07T05:11:53ZDaniel Le BerreRandom Walk Decorator disable Objective Function based heuristicsIt is possible to add random walks in the solver using the RandomWalkDecorator class, by using e.g.
mysolver.setOrder(new RandomWalkDecorator(new VarOrderHeap(),0.005);
It works fine for SAT solvers, however, there is an issue when wor...It is possible to add random walks in the solver using the RandomWalkDecorator class, by using e.g.
mysolver.setOrder(new RandomWalkDecorator(new VarOrderHeap(),0.005);
It works fine for SAT solvers, however, there is an issue when working with PB solvers, which use a heuristics taking into account the objective function.
The current implementation of PBSolver breaks the Liskov Substitution Principle because there is an instanceof statement in the PBSolver.setObjectiveFunction() method referring to a concrete class.
As such, using a decorator, the objective function is not passed to the VarOrderObjective object.
The solution is to fix properly the LSP issue by:
- creating an IOrderObjective interface to catch the capability to manage the objective function in a heuristics.
- use that interface in PBSolver in the instanceof statement.
- make the VarOrderObjective implement that interface.
- create a subclass of RandomWaldDecorator that implement that interface. 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/44add lower bound optimization strategy2018-07-07T05:11:53ZEmmanuel Loncaadd lower bound optimization strategyAll the optimization strategies are using upper bound search. Initial experiments on the software dependency problems showed that lower bounding could provide good results. Moving a dedicated code for lower bounding optimization into sat...All the optimization strategies are using upper bound search. Initial experiments on the software dependency problems showed that lower bounding could provide good results. Moving a dedicated code for lower bounding optimization into sat4j library.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/38Investigate usage of plain CNF rather than custom cardinality of PB constraints2018-07-07T05:11:53ZDaniel Le BerreInvestigate usage of plain CNF rather than custom cardinality of PB constraintsSat4j uses by default a custom constraint for cardinality and PB constraints.
The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure.
Many solvers fo...Sat4j uses by default a custom constraint for cardinality and PB constraints.
The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure.
Many solvers for solving MaxSat problems rely on cardinality of PB translation into SAT.
It would be nice to be able to easily try in sat4j the effect of pure clausal encodings against current solution.2.3.2https://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/55Fix memory leak in case of repeated use of Sat4j in an application2021-10-07T05:52:49ZDaniel Le BerreFix memory leak in case of repeated use of Sat4j in an applicationIn an application creating new solvers on user's action, the consumption of memory is growing.
It looks like there is a memory leak somewhere.In an application creating new solvers on user's action, the consumption of memory is growing.
It looks like there is a memory leak somewhere.2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/56Allow the end user to visualize the search of the solvers2019-01-03T09:55:37ZDaniel Le BerreAllow the end user to visualize the search of the solversIt is possible to hook SearchListener s to the solver in order to see what's going on inside the solver.
However, this need to be done using the API. There is currently no easy way to allow the command line user to trace the behavior of ...It is possible to hook SearchListener s to the solver in order to see what's going on inside the solver.
However, this need to be done using the API. There is currently no easy way to allow the command line user to trace the behavior of the solver.
It would be nice to provide a default tracing scheme to monitor the solver's behavior.2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/59Use package-info.java instead of package.html for package JavaDoc2019-01-03T09:55:37ZDaniel Le BerreUse package-info.java instead of package.html for package JavaDocThere are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move t...There are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move the current package documentation inside package-info.java files.
See http://docs.oracle.com/javase/6/docs/technotes/tools/solaris/javadoc.html#packagecomment for details.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/60ClassCastException when a class implements Propagatable but not Constr watche...2019-01-03T09:55:37ZPablo AbadClassCastException when a class implements Propagatable but not Constr watches a conflicting literalWhile experimenting with some new constraint types I've run into the situation where a constraint looks at several gruop of literals.
For that, each group has it's own class that watches for propagation and undo of their literals.
Since...While experimenting with some new constraint types I've run into the situation where a constraint looks at several gruop of literals.
For that, each group has it's own class that watches for propagation and undo of their literals.
Since watches require that a class implements interface Propagatable, everything looks fine, but I'm havng problems when one of the watched literals is identidfied as part of a conflict.
The offending lines are located in Solver.java around line 1025:
{noformat}
public Constr propagate() {
...
qhead = ltrail.size(); // propQ.clear();
// FIXME enlever le transtypage
return (Constr) lwatched.get(i);
...
}
{noformat}
There, a Propagatable from the watch list is cast to Constr to return the conflicting clause.
As a workaround, I've added a new method to Propagatable:
{noformat}
/**
* Returns the associated constraint with this object. Used for conflict analisys
*/
Constr associatedConstraint();
{noformat}
then I modified all the existing clauses to define this method as returning this:
{noformat}
public Constr associatedConstraint() {
return this;
}
{noformat}
and finally modified Solver to use the new method.
{noformat}
public Constr propagate() {
...
qhead = ltrail.size(); // propQ.clear();
return lwatched.get(i).associatedConstraint();
...
}
{noformat}
This works fine for the ocnstraints I'm defining, but it will be great if SAT4J can support this case by default, as the API implies.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/63Make Java 1.5 binaries instead of 1.42019-01-03T09:55:38ZDaniel Le BerreMake Java 1.5 binaries instead of 1.4Eclipse 4.2 will stop support for 1.4 VM as such it now requires 1.5 bycote instead of 1.4 one:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=369145
Sat4j is written in Java 5 but is downcompiled to Java 1.4 bytecode using JSR 14 target...Eclipse 4.2 will stop support for 1.4 VM as such it now requires 1.5 bycote instead of 1.4 one:
https://bugs.eclipse.org/bugs/show_bug.cgi?id=369145
Sat4j is written in Java 5 but is downcompiled to Java 1.4 bytecode using JSR 14 target.
Starting with Sat4j 2.3.2, Sat4j will be compiled with target 1.5 instead of jsr14.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/67Concurrent calls to isSatisfiable2019-01-03T09:55:38ZAlexey VoronovConcurrent calls to isSatisfiableIt would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under th...It would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under the hood, which resulted in very misleading exceptions until I realised that there was a concurrency problem.
An easy solution would be to simply add Synchronized to isSatisfiable() functions. The drawback of this will be that the call to model() after isSatisfiable() might give the model for the assumptions of another thread.
Another solution is to add ConcurrentModificationException if isSatisfiable is called while another call to isSatisfiable is in progress. This will not solve problems with model() after isSatisfiable(), but at least might hint early on that there is a concurrency problem.
A great solution would be to allow multiple calls to isSatisfiable (with different sets of assumptions) to be executed in parallel. I’m not sure that this is achievable by any simple code modification, but my thoughts are as following. Whatever is kept in the solver between consecutive calls can be readily shared between two parallel calls. And whatever is removed between consecutive calls should be private to each call of isSatisfiable. API would change, since models would be different for each call to isSatisfiable, but isSatisfiable itself could return the model if there exist one (using some java variant of Haskell’s Maybe or Scala’s Option class).
Parallel calls would create all sorts of problems, for example, what happens if a clause is added to the solver while a call to isSatisfiable() is in progress in another thread. But maybe such issues can be separated somehow.
I don’t yet know what would be the simplest---yet user-friendly--- solution. All ideas welcome :)2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/71Add statistics in ManyCore solvers on the solvers that answers 2018-04-13T11:56:14ZDaniel Le BerreAdd statistics in ManyCore solvers on the solvers that answers When using a manycore solver, it would be nice to have some statistics concerning the solvers that have been used to compute the solutions.When using a manycore solver, it would be nice to have some statistics concerning the solvers that have been used to compute the solutions.2.3.2