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/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/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/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/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/47Fix NPE when solver is killed by the competition framework while the solver c...2018-05-11T12:15:13ZDaniel Le BerreFix NPE when solver is killed by the competition framework while the solver cleans up the learned clausesWhen the competition framework stops the solver, a new thread is created, which displays some stats about learned clauses.
If the solver is cleaning up the set of learned clauses at that moment, the solver will throw an NPE, because the...When the competition framework stops the solver, a new thread is created, which displays some stats about learned clauses.
If the solver is cleaning up the set of learned clauses at that moment, the solver will throw an NPE, because the iterator on the learned clauses will try to access a constraint that has been removed.
We need to find a nice fix for that problem that will not slows down the solver during the search.
The issue mainly appears in the MAXSAT evaluation, in which the size of the benchmarks is small, thus the cleaning of the learned constraints very frequent because of the "wall" feature.https://gitlab.ow2.org/sat4j/sat4j/-/issues/48Memory requirement checking in ManyCore ends up in a counter intuitive behavior2018-07-07T05:11:53ZDaniel Le BerreMemory requirement checking in ManyCore ends up in a counter intuitive behaviorCurrently, if the available memory is less than 500MB, we only use one solver in ManyCore (thus ManyCorePB).
That behavior is quite counter intuitive because there are some use cases (e.g. debugging in p2) where it is nice to use a norm...Currently, if the available memory is less than 500MB, we only use one solver in ManyCore (thus ManyCorePB).
That behavior is quite counter intuitive because there are some use cases (e.g. debugging in p2) where it is nice to use a normal solver in one "thread" and a StringSolver on the other "thread". This is even worst since we now allow to provide a list of solvers directly on the constructor.
It is better to remove that check, at to let the user decide exactly how many solvers to use.https://gitlab.ow2.org/sat4j/sat4j/-/issues/49Allow the creation of a new variable with a hint for preferred branching pola...2018-05-11T12:15:13ZDaniel Le BerreAllow the creation of a new variable with a hint for preferred branching polarityCurrently, the user can ask for the creation of a new variable in the solver using nextFreeVarId().
In some cases, depending of what the variable represents, it might help to give a hint to the solver of the truth value to branch first o...Currently, the user can ask for the creation of a new variable in the solver using nextFreeVarId().
In some cases, depending of what the variable represents, it might help to give a hint to the solver of the truth value to branch first on.
overloading the nextFreeVarId() method to provide such feature would be nice.https://gitlab.ow2.org/sat4j/sat4j/-/issues/50Allow the solver to decide on a subset of the variables2018-07-07T05:11:53ZDaniel Le BerreAllow the solver to decide on a subset of the variablesIn some cases, it is necessary to force the solver to decide on a subset of the variables.
This can be done for checking that a set of variables constitutes a backdoor set for instance.
Adding that feature in Sat4j should not be a probl...In some cases, it is necessary to force the solver to decide on a subset of the variables.
This can be done for checking that a set of variables constitutes a backdoor set for instance.
Adding that feature in Sat4j should not be a problem if the restriction is applied to the heuristics (IOrder subclass).
The main changes required for that are:
- Add a new IOrder subclass that allows the end user to specific a subset of the variables to choose from
- Ask the solver to return UNKNOWN when no variables can be selected for branching.
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/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/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/58Allow easy control and information retrieval while the solver is running2018-05-11T12:15:13ZDaniel Le BerreAllow easy control and information retrieval while the solver is runningThere are many cases in which the user would like to control the SAT solver using the API.
While many things are currently possible, it is required to understand the internals of Sat4j.
Here the idea would be to allow the user to communi...There are many cases in which the user would like to control the SAT solver using the API.
While many things are currently possible, it is required to understand the internals of Sat4j.
Here the idea would be to allow the user to communicate using usual Dimacs format with the solver.https://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/62Expose solver stats and info programatically2018-05-11T12:15:13ZPablo AbadExpose solver stats and info programaticallyCurrently, the Solver class exposes several methods that can be used to get insight into different solver metrics:
void printStat(PrintWriter out, String prefix)
void printStat(PrintStream out, String prefix)
int nVars()
void printLearnt...Currently, the Solver class exposes several methods that can be used to get insight into different solver metrics:
void printStat(PrintWriter out, String prefix)
void printStat(PrintStream out, String prefix)
int nVars()
void printLearntClausesInfos(PrintWriter out, String prefix)
void printInfos(PrintWriter out, String prefix)
Map<String, Number> getStat()
long getTimeoutMs()
int realNumberOfVariables()
int nConstraints()
While some of these methods may be used while building constraints, most of them return information about the problem being represented and status of the solving process.
Furthermore, some of this information can't be accessed programatically, but printed to a Stream or Writer.
The proposal would be to create an interface that provides methods for retrieving all these information and add a method in Solver that returns an implementation of this interface. Ideally, all the printXXX methods could be moved from Solver into another class that would receive this interface.
Here is a possible draft of this interface:
public interface SolverStats {
int numberOfVars();
int realNumberOfVars();
int nContraints();
void observeStats(StatObserver observer);
void observeConstraintTypes(ConstraintTypeObserver observer);
void observeLearnedConstraintTypes(ConstraintTypeObserver observer);
}
public interface StatObserver {
public void observe(String stat, Number value);
// or a method per value type
}
public interface ConstraintTypeObserver {
public void observe(String type, int count);
}