sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2024-03-19T21:13:55Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/175Internal model enumeration provides incorrect results on this specific input ...2024-03-19T21:13:55ZDaniel Le BerreInternal model enumeration provides incorrect results on this specific input fileThe internal model enumeration does not provide the correct 2 models for the enclosed cnf file:
```
p cnf 10 23
1 3 6 0
2 5 0
4 5 0
5 0
-7 3 6 0
-3 7 0
-6 7 0
-1 -7 0
-2 -5 0
-8 1 6 0
-1 8 0
-6 8 0
-3 -8 0
-4 -5 0
-9 0
-5 -2 -4 -9 0
-10...The internal model enumeration does not provide the correct 2 models for the enclosed cnf file:
```
p cnf 10 23
1 3 6 0
2 5 0
4 5 0
5 0
-7 3 6 0
-3 7 0
-6 7 0
-1 -7 0
-2 -5 0
-8 1 6 0
-1 8 0
-6 8 0
-3 -8 0
-4 -5 0
-9 0
-5 -2 -4 -9 0
-10 1 3 0
-1 10 0
-3 10 0
-6 -10 0
-1 -2 0
-3 -4 0
-5 -6 0
```
It returns 11 models, which is incorrect (only the first two are corrects) :
```
c Found solution #1 (0,01)s
v -1 -2 3 -4 5 -6 7 -8 -9 10 0
c Found solution #2 (0,02)s
v 1 -2 -3 -4 5 -6 -7 8 -9 10 0
c Found solution #3 (0,02)s
v 1 2 -3 -4 5 -6 -7 8 -9 10 0
c Found solution #4 (0,02)s
v 1 -2 -3 4 5 -6 -7 8 -9 10 0
c Found solution #5 (0,02)s
v 1 2 -3 4 5 -6 -7 8 -9 10 0
c Found solution #6 (0,02)s
v 1 2 -3 4 -5 -6 -7 8 -9 10 0
c Found solution #7 (0,02)s
v 1 2 -3 4 5 -6 -7 8 9 10 0
c Found solution #8 (0,02)s
v 1 -2 -3 4 5 -6 -7 8 9 10 0
c Found solution #9 (0,02)s
v 1 2 -3 -4 5 -6 -7 8 9 10 0
c Found solution #10 (0,02)s
v 1 -2 -3 -4 5 -6 -7 8 9 10 0
c Found solution #11 (0,02)s
v 1 2 -3 4 -5 -6 -7 8 9 10 0
```
The external model enumeration provides the expected result.Daniel Le BerreDaniel Le Berrehttps://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/70Allow the possibility to compute counter models (negate a formula)2019-01-03T09:55:38ZDaniel Le BerreAllow the possibility to compute counter models (negate a formula)In some cases, it is necessary to compute counter examples of a formula (i;e. models of the negation of the formula).
It is easy to do that using the Plaisted-Greenbaum transformation, i.e. by adding a new fresh variable zi per constrai...In some cases, it is necessary to compute counter examples of a formula (i;e. models of the negation of the formula).
It is easy to do that using the Plaisted-Greenbaum transformation, i.e. by adding a new fresh variable zi per constraint, creating binary clauses -zi \lor -lj for each clause, and adding a new clause containing all zi.
This could be performed easily in a decorator.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/68Allow computing all MUSes using two calls to the SAT solver2019-01-03T09:55:38ZDaniel Le BerreAllow computing all MUSes using two calls to the SAT solverSat4j can currently compute one MUS.
It is possible to compute all MUSes using two calls to a SAT solver: the first one to detect all P-prime M-implicant of the formula (see my ECAI 96 paper or my PhD - in french- for details), the secon...Sat4j can currently compute one MUS.
It is possible to compute all MUSes using two calls to a SAT solver: the first one to detect all P-prime M-implicant of the formula (see my ECAI 96 paper or my PhD - in french- for details), the second one to compute a minimal hitting set (here it is mandatory to compute prime implicants).
The main issue will be to perform the second step: the first one can be performed by applying MAXSAT SAT several times, and preventing the same solutions to appear by adding blocking clauses.
2.3.3https://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/64Allow the solver to keep hot between successive calls2019-01-03T09:55:38ZDaniel Le BerreAllow the solver to keep hot between successive callsIn some cases, it may be interesting to keep the SAT solver in a state where the heuristics is not reset at each call.
As such, there is basically no difference between a restart and stopping the solver and starting it again (phase savin...In some cases, it may be interesting to keep the SAT solver in a state where the heuristics is not reset at each call.
As such, there is basically no difference between a restart and stopping the solver and starting it again (phase saving would be kept too).
Note that is does not look to pay off for optimization but might be useful for other uses.https://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/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/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/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/129Timeout should be in ms, not s2018-11-12T16:04:57ZDaniel Le BerreTimeout should be in ms, not sReceived from Arnaud Malapert:
Je crois qu'il y a une erreur dans le message de la TimeoutException.
Dans la classe Solver :
```
if (!undertimeout) {
String message = " Timeout (" + timeout
+ (timeBase...Received from Arnaud Malapert:
Je crois qu'il y a une erreur dans le message de la TimeoutException.
Dans la classe Solver :
```
if (!undertimeout) {
String message = " Timeout (" + timeout
+ (timeBasedTimeout ? "s" : " conflicts") + ") exceeded";
throw new TimeoutException(message); //$NON-NLS-1$//$NON-NLS-2$
}
```
Il me semble que timeout est en millisecondes plutôt qu'en secondes.https://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...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/140Add support for parity constraints2018-09-16T15:09:50ZDaniel Le BerreAdd support for parity constraintsSome applications require Boolean exploration of spaces defined using clauses, pseudo-Boolean constraints but also parity constraints.
Sat4j supports already clauses, cardinality and pseudo-Boolean constraints. Parity constraints suppor...Some applications require Boolean exploration of spaces defined using clauses, pseudo-Boolean constraints but also parity constraints.
Sat4j supports already clauses, cardinality and pseudo-Boolean constraints. Parity constraints support could be added to Sat4j core the same way as the cardinality constraints: by providing a concise representation of those constraints but still using the resolution proof system.
2.3.6https://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/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/134Throw IllegalStateException when calling unsatExplanation to avoid NPE.2018-07-07T05:11:53ZDaniel Le BerreThrow IllegalStateException when calling unsatExplanation to avoid NPE.If a user calls unsatExplanation() on a SAT problem, or before the solver has run, he will get an NPE.
One should throw an IllegalStateException with an appropriate message instead.If a user calls unsatExplanation() on a SAT problem, or before the solver has run, he will get an NPE.
One should throw an IllegalStateException with an appropriate message instead.https://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/132nesting atmost/atleast constraints into other constrains when using the gate ...2018-07-07T05:11:53ZMihai Barbuceanunesting atmost/atleast constraints into other constrains when using the gate translatorHi Daniel,
I've noticed that when using the GateTranslator, atleat/atmost constraints can only be specified globally for the gate. E.g. I can not say something like
if x then (atmost 1 y z w)
The atmost would apply globally to the ga...Hi Daniel,
I've noticed that when using the GateTranslator, atleat/atmost constraints can only be specified globally for the gate. E.g. I can not say something like
if x then (atmost 1 y z w)
The atmost would apply globally to the gate, not conditionally on x being true.
Is there a way to achieve this with the current GT, or is this a feature than can be introduced?
Many thanks,
Mihai
https://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/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.1