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/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/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/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/123Does Sat4j provide model counting capability?2018-07-07T05:11:53ZMouhammad SakrDoes Sat4j provide model counting capability?https://gitlab.ow2.org/sat4j/sat4j/-/issues/122Allow the definitions of levels of the heuristic2018-07-07T05:11:53ZDaniel Le BerreAllow the definitions of levels of the heuristicIn some cases, domain knowledge allow the user of the solver to rank the variables to guide the solver.
It would be nice to provide a way to provide such information to Sat4j users.In some cases, domain knowledge allow the user of the solver to rank the variables to guide the solver.
It would be nice to provide a way to provide such information to Sat4j users.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/116Implement decision conflict replacement proposed by Knuth2018-07-07T05:11:53ZDaniel Le BerreImplement decision conflict replacement proposed by KnuthDonald Knuth proposes in SAT13 to swap a regular conflict by a conflict clause containing only decision variables under certain conditions. It is not clear if such proposal works in practice.
All details available here:
http://www-cs-fac...Donald Knuth proposes in SAT13 to swap a regular conflict by a conflict clause containing only decision variables under certain conditions. It is not clear if such proposal works in practice.
All details available here:
http://www-cs-faculty.stanford.edu/~uno/programs/sat13.whttps://gitlab.ow2.org/sat4j/sat4j/-/issues/115Fix issue in Minisat Expensive Simplification2018-07-07T05:11:53ZDaniel Le BerreFix issue in Minisat Expensive SimplificationThe minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?).
The code...The minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?).
The code of minisat available in github contains the fix. We might want to implement our own.
It might be the case that such issue arrises when using cardinality constraints. Need to investigate further.https://gitlab.ow2.org/sat4j/sat4j/-/issues/114Implement reusable trail2018-07-07T05:11:52ZDaniel Le BerreImplement reusable trailReusable trail is proven to be efficient (used in Lingeling and Knuth SAT13 CDCL solver).
In order to implement future improvements in Sat4j, implementing such feature becomes mandatory.
All details are available here:
http://jsat.ewi.tu...Reusable trail is proven to be efficient (used in Lingeling and Knuth SAT13 CDCL solver).
In order to implement future improvements in Sat4j, implementing such feature becomes mandatory.
All details are available here:
http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_11_vanderTak.pdfhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/97Allow Sat4j statistics to be visible using JMX2018-07-07T05:11:52ZDaniel Le BerreAllow Sat4j statistics to be visible using JMXJava allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we c...Java allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we could at least use it for providing an access to the solver statistics while the solver is running.https://gitlab.ow2.org/sat4j/sat4j/-/issues/92Add documents on Sat4j web site to conform with OW2 mature project requirements2018-07-07T05:11:52ZDaniel Le BerreAdd documents on Sat4j web site to conform with OW2 mature project requirementsA few documents are mandatory according to the Ow2 mature project requirements:
- code convention guidelines
- SVN guidelines
- Ow2 dashboardA few documents are mandatory according to the Ow2 mature project requirements:
- code convention guidelines
- SVN guidelines
- Ow2 dashboardhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/82Allow to restrict the enumeration to a subset of variables2018-07-07T05:11:52ZDaniel Le BerreAllow to restrict the enumeration to a subset of variablesIn some cases, the user might want to reduce the enumeration to a subset only of the variables (when new variables have been added for the encoding for instance).In some cases, the user might want to reduce the enumeration to a subset only of the variables (when new variables have been added for the encoding for instance).https://gitlab.ow2.org/sat4j/sat4j/-/issues/74Make Sat4j easily usable in Scala2018-05-11T12:15:13ZDaniel Le BerreMake Sat4j easily usable in ScalaScala has some conventions for methods and fields that are different from usual Java ones.
It might be a good idea to complete the current API to make the integration of Sat4j inside scala programs seemingless.
Scala has some conventions for methods and fields that are different from usual Java ones.
It might be a good idea to complete the current API to make the integration of Sat4j inside scala programs seemingless.
3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/73Make Sat4j easily embeddable with JVM language2018-05-11T12:15:13ZDaniel Le BerreMake Sat4j easily embeddable with JVM languageWe use the Java code conventions in Sat4j.
Those conventions are not necessarily used in other JVM languages (such as Scala and Groovy for instance).
We would like to make Sat4j the library of choice for all JVM languages.
Such it might ...We use the Java code conventions in Sat4j.
Those conventions are not necessarily used in other JVM languages (such as Scala and Groovy for instance).
We would like to make Sat4j the library of choice for all JVM languages.
Such it might be needed to add/rename some methods of the api to make them easily usably in those languages.3.0https://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);
}
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/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/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/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.