sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2022-03-09T14:39:30Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/142Java 9 modularization?2022-03-09T14:39:30ZMark RaynsfordJava 9 modularization?Hello.
Are there any plans to modularize `sat4j` as Java 9 modules?Hello.
Are there any plans to modularize `sat4j` as Java 9 modules?3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/1Use a specific data structure for binary clauses compatible with reason simpl...2018-05-11T12:15:13ZDaniel Le BerreUse a specific data structure for binary clauses compatible with reason simplificationThe support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because th...The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.https://gitlab.ow2.org/sat4j/sat4j/-/issues/6Allow iterating over all prime impliquants2018-05-11T12:15:13ZDaniel Le BerreAllow iterating over all prime impliquantsissue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover...issue #3 ask for computing one primeImplicant. In some situations, computing all prime implicants is important.
Using the ModelIterator class with the primeImplicant() method instead of the model() method does compute an implicant cover, not all prime implicants.
something specific need to be implemented for that task.https://gitlab.ow2.org/sat4j/sat4j/-/issues/19Allow creation of clauses, cardinality and pseudo boolean constraints using a...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of clauses, cardinality and pseudo boolean constraints using arrays of primitive typeWhen creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.When creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.https://gitlab.ow2.org/sat4j/sat4j/-/issues/20Allow creation of soft constraints in a specific GateTranslator2018-05-11T12:15:13ZDaniel Le BerreAllow creation of soft constraints in a specific GateTranslatorSat4j provides a utility class GateTranslator to translate logical gate to CNF.
Some people would like to be able to use a similar class to produce weighted CNF, to be solved with a MAXSAT solver.
It should not be difficult to create a...Sat4j provides a utility class GateTranslator to translate logical gate to CNF.
Some people would like to be able to use a similar class to produce weighted CNF, to be solved with a MAXSAT solver.
It should not be difficult to create a subclass of GateTranslator to provide that functionality in the maxsat package.https://gitlab.ow2.org/sat4j/sat4j/-/issues/22DependencyHelper (the solvers in general) behave differently when units are s...2018-05-11T12:15:13ZDaniel Le BerreDependencyHelper (the solvers in general) behave differently when units are set first or set lastThe DependencyHelper behavior can look strange to newcomer since its behavior depends of the order of the constraints.
SAT power users use that order to let the solver perform as much simplification as possible.
Here, we receive an exc...The DependencyHelper behavior can look strange to newcomer since its behavior depends of the order of the constraints.
SAT power users use that order to let the solver perform as much simplification as possible.
Here, we receive an exception when the constraints are simplified.
Several options are available:
- do not fix, its a feature, not a bug
- fix be ignoring simplified constraints => no more control of what's going on in the helper, might be error prone
- fix by delegating unit to be the last thing added to the solver: the helper acts as a proxy here. => no more power user control of the helper.
Need to think about it.https://gitlab.ow2.org/sat4j/sat4j/-/issues/24Add statistics about SAT/UNSAT calls2018-05-11T12:15:13ZDaniel Le BerreAdd statistics about SAT/UNSAT callsWhen doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.When doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.https://gitlab.ow2.org/sat4j/sat4j/-/issues/25Allow input string to be read properly using InputStream or Reader2018-05-11T12:15:13ZDaniel Le BerreAllow input string to be read properly using InputStream or ReaderFor the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is ...For the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is not supported in some readers.
Not a big deal to fix, but need to be done properly.https://gitlab.ow2.org/sat4j/sat4j/-/issues/28Allow easy explanation for OPB file2022-04-09T17:42:39ZDaniel Le BerreAllow easy explanation for OPB fileCurrently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to...Currently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to easily display the unsat core in terms of constraints number (might not be that good because an equality constraint is splitted into 2 constraints).https://gitlab.ow2.org/sat4j/sat4j/-/issues/46Add an API to reduce the value of the objective function in case of optimization2018-05-11T12:15:13ZDaniel Le BerreAdd an API to reduce the value of the objective function in case of optimizationWhen we do optimization using strengthening, we decrease the value of an atMostK constraint, corresponding to the best upper bound of the objective function.
When using CNF translation of AtMostK, this is done only by setting some boole...When we do optimization using strengthening, we decrease the value of an atMostK constraint, corresponding to the best upper bound of the objective function.
When using CNF translation of AtMostK, this is done only by setting some boolean variables.
It is currently not easy to know when that value is reduced, thus it is not possible to take advantage of the CNF translation.
https://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/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/52Add usage of Lower bounding to MaxSat2018-05-11T12:15:13ZDaniel Le BerreAdd usage of Lower bounding to MaxSatA lower bounding procedure is available in Sat4j API since release 2.3.1.
It would be nice to have the ability to use it on the command line of the maxsat solver.A lower bounding procedure is available in Sat4j API since release 2.3.1.
It would be nice to have the ability to use it on the command line of the maxsat solver.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/54Dispatch lower bounding to all parts of Sat4j2018-05-11T12:15:13ZDaniel Le BerreDispatch lower bounding to all parts of Sat4jLower bounding is available in the API of Sat4j 2.3.1.
The next step is now to provide that feature on the command line of all optimization tools.Lower bounding is available in the API of Sat4j 2.3.1.
The next step is now to provide that feature on the command line of all optimization tools.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/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/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/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/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/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/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/93Find a way to factorize the various settings for the solvers2018-07-07T05:11:52ZDaniel Le BerreFind a way to factorize the various settings for the solversThe PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not...The PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not have any dependency to commons CLI, so is a bit different from the two others.
However, we need to find a central class to perform the configuration of solvers: note that in sat package, the configuration of the solvers is done twice, one in DetailedCommandPanel and one in Launcher.
https://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/102API for using an OPB string spec2018-07-07T05:11:52ZMihai BarbuceanuAPI for using an OPB string specHi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going throug...Hi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going through the command line.
Many Thanks,
Mihaihttps://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/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/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/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/123Does Sat4j provide model counting capability?2018-07-07T05:11:53ZMouhammad SakrDoes Sat4j provide model counting capability?https://gitlab.ow2.org/sat4j/sat4j/-/issues/125CP solver provides incorrect results when performing Lexico-optimization2018-07-07T05:11:53ZDaniel Le BerreCP solver provides incorrect results when performing Lexico-optimizationOnce issue #124 has been fixed, the parallel solver res+cp solver still provides a wrong solution (ignore unit clauses in 3 cases) or wrong optimum (in 10 cases) out of the 2688 benchmarks.
It is likely that such issue is related to for...Once issue #124 has been fixed, the parallel solver res+cp solver still provides a wrong solution (ignore unit clauses in 3 cases) or wrong optimum (in 10 cases) out of the 2688 benchmarks.
It is likely that such issue is related to former #113 issue, i.e. incorrect handling of unit clause removal in case of unsatisfiability.https://gitlab.ow2.org/sat4j/sat4j/-/issues/126How do I do an industry standard export for Partial Weighted MaxSat problems?2018-07-07T05:11:53ZGhost UserHow do I do an industry standard export for Partial Weighted MaxSat problems?I have filed this as question, but it might result in a change request:
I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constrai...I have filed this as question, but it might result in a change request:
I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constraints. If I do not want to convert them to CNF constraints, I cannot export a wcnf file but must export something other.
I think the .opb format is suitable for that case. Am I right?
I tried to create .opb output using the OPBStringSolver or the LPStringSolver. Both have the same problem:
The WeightedMaxSatDecorator calls the method "registerLiteral(int p)" on the decorated solver. Since both the OPBStringSolver and the LPStringSolver extend the DimacsStringSolver, the method DimacsStringSolver.registerLiteral(int p) is called, which throws an UnsupportedOperationException.
So, if one of these StringSolvers is suitable for my problem: Would it be a solution to override the method in that suitable solver so that it does not do anything?
An, if none of these StringSolvers is suitable: Is there another way of exporting all input that the WeightedMaxSatDecorator got into a standard file format?https://gitlab.ow2.org/sat4j/sat4j/-/issues/127OPBSolver exports files with empty objectives2018-11-12T16:07:10ZGhost UserOPBSolver exports files with empty objectivesI tried the OPBSolverDecorator for exporting .opb files. In some cases, my objective function is empty because I am solving a pure SAT instance (using the PB solver because of "at most 1"-constraints).
In these cases, the OPBSolverDecor...I tried the OPBSolverDecorator for exporting .opb files. In some cases, my objective function is empty because I am solving a pure SAT instance (using the PB solver because of "at most 1"-constraints).
In these cases, the OPBSolverDecorator outputs a .opb format that the command line sat4j-pb.jar does not understand. The text opb file then contains the following line:
min: ;
This is because the "toString()" method does a null-check on the objective function, but it does no empty-check on it. I think my fix for it is suboptimal:
```
if (this.obj != null) {
String objStr = obj.toString();
if (objStr.trim().length() > 0) {
tmp.append("\n");
tmp.append("min: ");
tmp.append(this.obj);
tmp.append(";");
}
}
```https://gitlab.ow2.org/sat4j/sat4j/-/issues/128PB solver finds wrong optimal solution when a unit clause appears in the inpu...2018-07-07T05:11:53ZDaniel Le BerrePB solver finds wrong optimal solution when a unit clause appears in the input fileWhen running the functional tests on PB12 benchmarks, the solvers return incorrectly on a few benchmarks, e.g. normalized-PB06/OPT-SMALLINT/submitted-PB06/manquiho/bounded_golomb_rulers/normalized-bogr_7.opb.
Those benchmarks contain un...When running the functional tests on PB12 benchmarks, the solvers return incorrectly on a few benchmarks, e.g. normalized-PB06/OPT-SMALLINT/submitted-PB06/manquiho/bounded_golomb_rulers/normalized-bogr_7.opb.
Those benchmarks contain unit clauses.
It might be the case that a propagation by one learned constraint is removed incorrectly (e.g. a PB constraint propagates x which is also a unit clause).
We may need to check in the PB constraint when we remove it if the literals are not propagated by a unit clause, or simply to remove that literal from the PB constraint.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/133Support XCSP 3 format2018-07-07T05:11:53ZDaniel Le BerreSupport XCSP 3 formatA new version of XCSP has just been released.
http://xcsp.org/
The most important part of the new format is available in available in a subset of the spec, XCSP 3.0 core:
http://xcsp.org/core/menuCore.html
Sat4j CSP should implement it...A new version of XCSP has just been released.
http://xcsp.org/
The most important part of the new format is available in available in a subset of the spec, XCSP 3.0 core:
http://xcsp.org/core/menuCore.html
Sat4j CSP should implement it to be used in the classroom with master students.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/136Incorrect answer with PB Solver2018-07-07T05:11:54ZAnithaIncorrect answer with PB SolverI am seeing a strange issue with solving a PBO problem using SAT4J: version NIGHTLY.v20151101
Attached are 2 opb files: min-nonbuggy.opb and min.opb
Differences between the files: Both files differ from line 18 onwards. "min.opb" is an...I am seeing a strange issue with solving a PBO problem using SAT4J: version NIGHTLY.v20151101
Attached are 2 opb files: min-nonbuggy.opb and min.opb
Differences between the files: Both files differ from line 18 onwards. "min.opb" is an extension of min-nonbuggy.opb. Note that both files have same objective function that needs to be minimized.
The first file ("min-nonbuggy.opb") returns correct answer with optimum value as "4" with x12=0, x14 = 0 and x17=0. I agree with this answer. I also verified this by manually solving the constraints and objective function.
The second file ("min.opb") returns answer with optimum value as "5" with x12=1, x14=0 and x17=0. I think this is wrong.
(I am interested in values that appear in objective function only)
This is quite surprising given that - no additional constraint involving "x12" appears in "min.opb". So x12 should be 0 regardless of value of x17. Isn't it? Why is the answer returned as x12=1?
https://gitlab.ow2.org/sat4j/sat4j/-/issues/138Fix WBO issue found during PB 20162018-07-07T05:11:54ZDaniel Le BerreFix WBO issue found during PB 2016A problem with WBO has been discovered during PB16. It seems that the top costs are ignored.A problem with WBO has been discovered during PB16. It seems that the top costs are ignored.2.3.6https://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/146ModelIteratorTest.testGlobalTimeoutCounter makes build instable2018-09-16T14:55:52ZDaniel Le BerreModelIteratorTest.testGlobalTimeoutCounter makes build instableThe test case ModelIteratorTest.testGlobalTimeoutCounter uses a timeout, which makes the test fail if it is reached.
The issue is that such timeout may be reached depending of the load of the computer running the tests.
So the same cod...The test case ModelIteratorTest.testGlobalTimeoutCounter uses a timeout, which makes the test fail if it is reached.
The issue is that such timeout may be reached depending of the load of the computer running the tests.
So the same code may pass or not pass the tests depending of the load of the runner ...https://gitlab.ow2.org/sat4j/sat4j/-/issues/148ArrayIndexOutOfBound exception on non normalized WBO opb file2018-10-29T16:44:23ZDaniel Le BerreArrayIndexOutOfBound exception on non normalized WBO opb fileIn WBO, non normalized constraints cause an ArrayIndexOutOfBoundsException:
```
java -jar dist/CUSTOM/sat4j-pb.jar CuttingPlanes ~/Downloads/bugpourevocrash2.opb
```
```
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsExcepti...In WBO, non normalized constraints cause an ArrayIndexOutOfBoundsException:
```
java -jar dist/CUSTOM/sat4j-pb.jar CuttingPlanes ~/Downloads/bugpourevocrash2.opb
```
```
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 6
at org.sat4j.core.Vec.get(Vec.java:239)
at org.sat4j.pb.constraints.pb.InternalMapPBStructure.get(InternalMapPBStructure.java:102)
at org.sat4j.pb.constraints.pb.ConflictMap.isImplyingLiteral(ConflictMap.java:621)
at org.sat4j.pb.constraints.pb.ConflictMap.isAssertive(ConflictMap.java:583)
at org.sat4j.pb.core.PBSolverCP.analyzeCP(PBSolverCP.java:141)
at org.sat4j.pb.core.PBSolverCP.analyze(PBSolverCP.java:129)
at org.sat4j.minisat.core.Solver.search(Solver.java:1320)
at org.sat4j.minisat.core.Solver.isSatisfiable(Solver.java:1824)
at org.sat4j.tools.SolverDecorator.isSatisfiable(SolverDecorator.java:115)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:179)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:172)
at org.sat4j.OptimizationMode.solve(OptimizationMode.java:121)
at org.sat4j.AbstractLauncher.solve(AbstractLauncher.java:318)
at org.sat4j.AbstractLauncher.run(AbstractLauncher.java:257)
at org.sat4j.pb.LanceurPseudo2007.main(LanceurPseudo2007.java:97)
```
[bugpourevocrash.opb](/uploads/3a9ca6ffde44f1a136d337ba86ded8c5/bugpourevocrash.opb)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/150Update code base to Java 72018-11-13T06:56:33ZDaniel Le BerreUpdate code base to Java 7The original source code of Sat4j was Java 1.5 down compiled to 1.4.
The 2.3.6 release will be compatible with Java 7.
As such, new syntactic structures are available (try with resources, multiple exceptions).
We need to take care pro...The original source code of Sat4j was Java 1.5 down compiled to 1.4.
The 2.3.6 release will be compatible with Java 7.
As such, new syntactic structures are available (try with resources, multiple exceptions).
We need to take care properly of that.
SonarQube can help us for that.2.3.6Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/153Bug when mixing constraint removal and constraints satisfied by unit propagation2019-01-27T15:32:36ZMiguel NevesBug when mixing constraint removal and constraints satisfied by unit propagationHi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation.
In particular, the bug is triggered by the following sequence of operations:
- add constra...Hi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation.
In particular, the bug is triggered by the following sequence of operations:
- add constraints (x1 + x2 + x3 <= 2), (x1 + x2 >= 2) and (not(x2) v not(x3))
- check satisfiability: formula is SAT, as expected
- remove (x1 + x2 >= 2)
- add (x2 + x3 >= 2): this should contradict (not(x2) v not(x3)), but no exception is thrown
- check satisfiability: formula should be UNSAT, but SAT is returned instead
I have attached a small Java program that follows this sequence of operations, triggering the bug.
Best regards,
Miguel Neves
[SatByUnitBug.java](/uploads/f36125668baadf4011b0cf998bac3a42/SatByUnitBug.java)https://gitlab.ow2.org/sat4j/sat4j/-/issues/155Provide a way to serialize constraints in files2023-03-11T18:46:20ZDaniel Le BerreProvide a way to serialize constraints in filesThe current `toString()` method is mainly used for debugging purpose. We need currently a way to dump constraints in a textual format which can be used to recover the constraint later on.
The proposal is to add a new method `dump()` in ...The current `toString()` method is mainly used for debugging purpose. We need currently a way to dump constraints in a textual format which can be used to recover the constraint later on.
The proposal is to add a new method `dump()` in `IConstr` and in `IProblem` to allow dumping an object to either a Dimacs of OPB file.
There are a lot of corner cases, especially regarding unit clauses.
It will require a lot of testing before being released.https://gitlab.ow2.org/sat4j/sat4j/-/issues/156some small problems in fileName-handling2019-06-23T16:22:04ZDieter von Holtensome small problems in fileName-handlinga recent message in Twitter '... the upcoming new release of Sat4J ... ' activated me to throw in a fix from my codebase:
in method `parseInstance()` there are two small problems - see comments in lines 107 - 117.
[InstanceReader.java]...a recent message in Twitter '... the upcoming new release of Sat4J ... ' activated me to throw in a fix from my codebase:
in method `parseInstance()` there are two small problems - see comments in lines 107 - 117.
[InstanceReader.java](/uploads/1247974b5e53b73bc9b132f0e5329890/InstanceReader.java)https://gitlab.ow2.org/sat4j/sat4j/-/issues/158Fix new violation considered as a bug in SonarQube2019-08-20T08:36:34ZDaniel Le BerreFix new violation considered as a bug in SonarQubeA recent update of SonarQube has introduced a new violation considered as a bug:
https://sonarqube.ow2.org/project/issues?id=org.ow2.sat4j%3Aorg.ow2.sat4j.pom&resolved=false&types=BUG
Refactor this code so that the Iterator supports mul...A recent update of SonarQube has introduced a new violation considered as a bug:
https://sonarqube.ow2.org/project/issues?id=org.ow2.sat4j%3Aorg.ow2.sat4j.pom&resolved=false&types=BUG
Refactor this code so that the Iterator supports multiple traversal, aka iterator() method should not return this.
There are three cases in which it happens, related to multi-criteria optimization. It would be nice to fix this before 2.3.6 release.Emmanuel LoncaEmmanuel Loncahttps://gitlab.ow2.org/sat4j/sat4j/-/issues/159Update continuous integration settings to build correctly for contributors2020-01-03T15:12:34ZDaniel Le BerreUpdate continuous integration settings to build correctly for contributorsWhen the project is forked, the CI build does not work due to credentials issue.
The build should work off-the-shelves when forking.When the project is forked, the CI build does not work due to credentials issue.
The build should work off-the-shelves when forking.https://gitlab.ow2.org/sat4j/sat4j/-/issues/160Refactor LearnedConstraintDeletionStrategy management2020-03-11T14:33:06ZDaniel Le BerreRefactor LearnedConstraintDeletionStrategy managementThe way LearnedConstraintDeletionStrategy strategy design pattern is implemented currently is not satisfactory: each strategy is created once in each solver. Only one should be instantiated.
We need to find a better way to handle both t...The way LearnedConstraintDeletionStrategy strategy design pattern is implemented currently is not satisfactory: each strategy is created once in each solver. Only one should be instantiated.
We need to find a better way to handle both the timers required for LCDS and the strategies themselves.https://gitlab.ow2.org/sat4j/sat4j/-/issues/162Provide access to decisions taken during the search in the API2021-02-22T21:14:58ZDaniel Le BerreProvide access to decisions taken during the search in the APIThere are several use cases in which it can be useful to know which decisions have been taken
to obtain a given model.
That information is currently available inside the Solver class, but not available in the API.
It is used to "block" ...There are several use cases in which it can be useful to know which decisions have been taken
to obtain a given model.
That information is currently available inside the Solver class, but not available in the API.
It is used to "block" a given model by adding a clause made of the negation of the decision literals.
Providing access to those decisions may allow the user to perform e.g. projected enumeration.
Providing public access to those decisions may require:
- [x] provide a new method in the API to access those decisions
- [ ] to move the current code of `Solver.createBlockingClauseForCurrentModel` to another place (`ModelIterator`?)
- [ ] optionally extend the `ModelIterator` class to support projected model enumerationDaniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/163MaxHSLike solver won't launch from command line2021-02-19T21:06:16ZRomain WALLONMaxHSLike solver won't launch from command lineCurrently, the way the `MaxHSLike` solver is instantiated and initialized in the MaxSAT launcher does not allow the solver to be fed with the constraints of the problem, so that the solver does not know these constraints when `isSatisifi...Currently, the way the `MaxHSLike` solver is instantiated and initialized in the MaxSAT launcher does not allow the solver to be fed with the constraints of the problem, so that the solver does not know these constraints when `isSatisifiable()` is invoked.https://gitlab.ow2.org/sat4j/sat4j/-/issues/165Missing negated literals in dedicated watch structure for computing prime imp...2021-03-03T06:53:03ZDaniel Le BerreMissing negated literals in dedicated watch structure for computing prime implicantsIn the enclosed CNF file, the default prime implicant computation strategy displays as prime implicant
v 2 3 4 5 6 0
while the two others display
v 2 3 4 5 6 -21 -22 -24 -25 -26 -27 0
All output should always be the same.
[Q3inK08.c...In the enclosed CNF file, the default prime implicant computation strategy displays as prime implicant
v 2 3 4 5 6 0
while the two others display
v 2 3 4 5 6 -21 -22 -24 -25 -26 -27 0
All output should always be the same.
[Q3inK08.cnf](/uploads/2a9c1cb835ee96b61f66655dbe116ef2/Q3inK08.cnf)Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/166Add a way to reveal the cardinality constraints found by DetectCards2021-03-30T08:35:51ZDaniel Le BerreAdd a way to reveal the cardinality constraints found by DetectCardsThe only way current to display those constraints is to use a specific launcher:
```
java -Dprintcards=true -cp sat4j-pb.jar org.sat4j.pb.CardConstrLearningSolverLauncher file.cnf
```
It would be nice to have that information displayed...The only way current to display those constraints is to use a specific launcher:
```
java -Dprintcards=true -cp sat4j-pb.jar org.sat4j.pb.CardConstrLearningSolverLauncher file.cnf
```
It would be nice to have that information displayed using the more classical
```
java -jar sat4j-pb.jar DetectCards file.cnf
```https://gitlab.ow2.org/sat4j/sat4j/-/issues/167Fix displayed information when revealing cardinality constraints2021-03-30T08:38:34ZDaniel Le BerreFix displayed information when revealing cardinality constraintsWhen revealing cardinality constraints, the information displayed is not accurate.
See e.g. for a pigeon hole 3-4 problem:
```
c solving ph3-4.cnf
c reading problem ...
c ... done. Wall clock time 0.01s.
c declared #vars 12
c #con...When revealing cardinality constraints, the information displayed is not accurate.
See e.g. for a pigeon hole 3-4 problem:
```
c solving ph3-4.cnf
c reading problem ...
c ... done. Wall clock time 0.01s.
c declared #vars 12
c #constraints 0
c constraints type
c 0 constraints processed.
c launching cardinality constraint revelation process
c remaining constraints: 4/22
c cardinality constraints found (preprocessing): 3
c cardinality search time (preprocessing): 11ms
c found 3 at-most cardinality constraint of degree 1 and size 4
c solver contains 7 constraints
```
The `#constraints` and `constraints processed` are not accurate.https://gitlab.ow2.org/sat4j/sat4j/-/issues/169Global time-based timer are not canceled2021-10-07T05:52:49ZDaniel Le BerreGlobal time-based timer are not canceledin #55 @puzzler reported memory out when creating many Sat4j solvers with a model iterator.
After investigation, the issue is that the model iterator enforces a global timeout in the solver. In that case, the internal Timer object is ne...in #55 @puzzler reported memory out when creating many Sat4j solvers with a model iterator.
After investigation, the issue is that the model iterator enforces a global timeout in the solver. In that case, the internal Timer object is never canceled, which prevents Sat4j objects to be garbage collected.
The workaround is to use a conflict based timeout in that case.
To prevent similar issue in the future, we could:
- use a conflict-based timer by default
- do not force global timeout for model iterator
- ...
The issue requires further investigation.Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/171Make Sat4j 3.0 a set of Java modules2023-04-29T18:01:55ZDaniel Le BerreMake Sat4j 3.0 a set of Java modulesWith release 3.0, we want to deliver Sat4j as separate Java modules.
The main issue is to be able to build executable jars for the end users of SAT, PB or MAXSAT solvers.
#142 has initiated the discussion 3 years ago.
This work will b...With release 3.0, we want to deliver Sat4j as separate Java modules.
The main issue is to be able to build executable jars for the end users of SAT, PB or MAXSAT solvers.
#142 has initiated the discussion 3 years ago.
This work will be performed on a separate branch by @romain_wallon and @lonca until we find a reasonable solution (i.e. easy to use jar files from the command line for the end user).https://gitlab.ow2.org/sat4j/sat4j/-/issues/172Fix manifest metadata to contain only the one applicable2022-07-31T06:31:36ZDaniel Le BerreFix manifest metadata to contain only the one applicableThe current jars files of Sat4j used as osgi bundles or as executable jar files are currently sharing the same static manifest files.
The osgi bundles are generated using maven.
The executable jar files using ant.
The latter requires ...The current jars files of Sat4j used as osgi bundles or as executable jar files are currently sharing the same static manifest files.
The osgi bundles are generated using maven.
The executable jar files using ant.
The latter requires a classpath entry which currently generates warnings in eclipse build (see [issue 146](https://github.com/eclipse-platform/eclipse.platform.releng.aggregator/issues/416)).
To avoid this, the manifest files should be adapted to the target usage of the jar files.Daniel Le BerreDaniel Le Berrehttps://gitlab.ow2.org/sat4j/sat4j/-/issues/173Unnecessary code to remove in the DAC_meanLearnedDegree branch2023-01-30T10:38:35ZAlain KemgueUnnecessary code to remove in the DAC_meanLearnedDegree branchUnnecessary [code](https://gitlab.ow2.org/sat4j/sat4j/-/blob/DAC_meanLearnedDegree/train_dqn.py#L643-L659) to remove in the next push.Unnecessary [code](https://gitlab.ow2.org/sat4j/sat4j/-/blob/DAC_meanLearnedDegree/train_dqn.py#L643-L659) to remove in the next push.https://gitlab.ow2.org/sat4j/sat4j/-/issues/174Cardinality detector statistics are incorrect2023-10-12T10:23:39ZDaniel Le BerreCardinality detector statistics are incorrectWhen launching DetectCards on a PHP 200 instance, the solve provides the following output:
```
c declared #vars 40200
c #constraints 201
c constraints type
c org.sat4j.pb.constraints.pb.OriginalHTClausePB => 201
c 201 constraints ...When launching DetectCards on a PHP 200 instance, the solve provides the following output:
```
c declared #vars 40200
c #constraints 201
c constraints type
c org.sat4j.pb.constraints.pb.OriginalHTClausePB => 201
c 201 constraints processed.
c launching cardinality constraint revelation process
c remaining constraints: 0/4020000
c cardinality constraints found (preprocessing): 200
c cardinality search time (preprocessing): 14648ms
c found 200 at-most cardinality constraint of degree 200 and size 201
c solver contains 401 constraints
```
The main issue is that the at-most cardinality constraint should be of degree 1, not 200. Internally, the constraint is an AtLeastCard, so the degree should be size-degree to fix that. However, changing the computation of the degree in PreprocCardConstrLearningSolver line 348 does not seem to fix the problem.
Another (small) issue is that the number of constraints is not correct. According to the logs, there was 4020000 clauses originally. This is the number with would have expected instead of 201.Emmanuel LoncaEmmanuel Loncahttps://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 Berre