sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-04-13T11:56:14Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/121Initialization of org.sat4j.minisat.core.Solver calls Runtime.getRuntime().fr...2018-04-13T11:56:14ZGhost UserInitialization of org.sat4j.minisat.core.Solver calls Runtime.getRuntime().freeMemory()The class Solver in the sat4j core package initializes a variable called "memoryTimer" with an anonymous inner class of type ConflictTimerAdapter.
This inner class statically initializes a variable called "memorybound":
final long memor...The class Solver in the sat4j core package initializes a variable called "memoryTimer" with an anonymous inner class of type ConflictTimerAdapter.
This inner class statically initializes a variable called "memorybound":
final long memorybound = Runtime.getRuntime().freeMemory() / 10;
This is an expensive operation which seems to slow down the entire system for counting the available memory. In a multi-threaded scenary with many small partial weighted maxsat instances, it can lead to the machine being occupied with calculating the free memory again and again.
And: The initial class is not necessarily needed at all, e.g. when running a WeightedMaxSatDecorator with the default solver:
maxSatSolver = new WeightedMaxSatDecorator(SolverFactory.newDefault());
I propose to implement another kind of initialization that is only computing the amount of available memory when it is really needed. There are some usages of the variable "solver.memory_based" insat4j-core and sat4j-pb, and I think this could be replaced by a getter method that does the initialization when it is needed.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/120Remove call to System.gc in solver2018-04-13T11:56:12ZGhost UserRemove call to System.gc in solverI did some performance tests with the partial weighted maxsat solver called in many (up to 150) threads. After a while, tens of threads stuck in the call to "System.gc" in the class "org.sat4j.minisat.core.Solver", method "reduceDB()". T...I did some performance tests with the partial weighted maxsat solver called in many (up to 150) threads. After a while, tens of threads stuck in the call to "System.gc" in the class "org.sat4j.minisat.core.Solver", method "reduceDB()". This was a major performance bottleneck.
I downloaded the source, removed the call to "System.gc", compiled the sat4j-core and started the performance test again. The bottleneck was gone.
I think this call to System.gc should be removed. If there is really a need for this call, it could be made configurable (via an API call), so that it can be switched off if sat4j is used in multithreaded applications.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/119Iterators can be created at each conflict2018-04-13T11:56:15ZBenoît HoessenIterators can be created at each conflictWhenever the ConflictTimerContainer is used, an iterator on Vec is created.
```
public void newConflict() {
Iterator<ConflictTimer> it = this.timers.iterator();
while (it.hasNext()) {
it.next().newConfli...Whenever the ConflictTimerContainer is used, an iterator on Vec is created.
```
public void newConflict() {
Iterator<ConflictTimer> it = this.timers.iterator();
while (it.hasNext()) {
it.next().newConflict();
}
}
{code}
This could be easily changed to a version using no iterator to avoid object creation/destruction
{code:title=ConflictTimerContainer.java|borderStyle=solid}
public void newConflict() {
for(int i =0; i<this.timers.size(); i++){
this.timers.get(i).newConflict();
}
}
```
This, applied to a small instance like velev-engi-uns-1.0-4nd.cnf can reduce the number of created object by 92594 (= 311936 B)2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/112Integrate faster prime implicant computation2018-04-13T11:56:11ZDaniel Le BerreIntegrate faster prime implicant computationWe propose in a paper to be presented in FMCAD 2013 a new algorithm for computing prime implicants in a CDCL solver. The code of that paper is available on a specific branch (BRESIL). We need to move that code to the main branch now, and...We propose in a paper to be presented in FMCAD 2013 a new algorithm for computing prime implicants in a CDCL solver. The code of that paper is available on a specific branch (BRESIL). We need to move that code to the main branch now, and to make a release of Sat4j including that new feature before presenting that work at FMCAD.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/109Allow iterating on a part of a model (subset of its variables)2018-04-13T11:56:13ZDaniel Le BerreAllow iterating on a part of a model (subset of its variables)In some cases, it may be useful to iterate over a subset of the variables
(over decisions variables for instance).
The idea is to simply restrict the use of the model iterator (using blocking clauses) to a subset of the variables only.
...In some cases, it may be useful to iterate over a subset of the variables
(over decisions variables for instance).
The idea is to simply restrict the use of the model iterator (using blocking clauses) to a subset of the variables only.
We require for this a new class, for efficiency reason, instead of generalizing the code of the actual ModelIterator class.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/104Improve error report when xsd missing2018-04-13T11:56:15ZBenoît HoessenImprove error report when xsd missingWhen using the csp solver within sat4J, a null pointer exception is launched if instance_2_0.xsd is missing from org.sat4j.csp.xml.CspXmlParser:50
A possible fix would be to make sure that url is not null:
if(url == null){
throw new ...When using the csp solver within sat4J, a null pointer exception is launched if instance_2_0.xsd is missing from org.sat4j.csp.xml.CspXmlParser:50
A possible fix would be to make sure that url is not null:
if(url == null){
throw new IOException("Unable to locate instance_2_0.xsd");
}2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/100Create a specific event when learning unit clauses2018-04-13T11:56:14ZDaniel Le BerreCreate a specific event when learning unit clausesWhen the solver learns unit clauses (a literal), it needs to got back to decision level zero, and such clause is managed specifically in the solver.
In the context of parallel SAT solving, a solver like plingeling is sharing unit clauses...When the solver learns unit clauses (a literal), it needs to got back to decision level zero, and such clause is managed specifically in the solver.
In the context of parallel SAT solving, a solver like plingeling is sharing unit clauses among parallel solvers. Having a specific unit clause event would allow to implement more easily such feature in Sat4j.2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/98Allow hybrid lexico optimization2018-04-13T11:56:12ZDaniel Le BerreAllow hybrid lexico optimizationIn some cases, it would be nice to be able to perform a lexico optimization without waiting to prove the optimality of each criteria.
It means that the first criteria is optimized during a given timeout, then the first and second are op...In some cases, it would be nice to be able to perform a lexico optimization without waiting to prove the optimality of each criteria.
It means that the first criteria is optimized during a given timeout, then the first and second are optimized during a given timeout, and so on until all the criteria are considered.
We would use a classical transformation of lexico into a linear objective function for all but the first optimization.2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/96Allow Sat4j to provide unsat proofs in RUP format2018-04-13T11:56:17ZDaniel Le BerreAllow Sat4j to provide unsat proofs in RUP formatThere is a new track for certifying unsat proofs. It should not be difficult to allow sat4j to participate by implementing an unsat proof search listener.There is a new track for certifying unsat proofs. It should not be difficult to allow sat4j to participate by implementing an unsat proof search listener.2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/94if-then constraint2018-04-13T11:56:15ZMihai Barbuceanuif-then constraintWhat would be the best way to have if-then constraints (without the else part, which the ite forces on the user) in the GateTranslator? The GateTranslator does not have a default constructor hence can't be simply extended.
Thanks
MihaiWhat would be the best way to have if-then constraints (without the else part, which the ite forces on the user) in the GateTranslator? The GateTranslator does not have a default constructor hence can't be simply extended.
Thanks
Mihai2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/90Better management of forgotten variables for undo-based constraints2018-04-13T11:56:17ZDaniel Le BerreBetter management of forgotten variables for undo-based constraintsSat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
...Sat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
However, there is an issue for constraints requiring a call to undo when backtracking.
The constraints to be considered when undoing an assignment is stored for a variable, not a literal. As such, when forgetting a variable, both the constraints where the positive and negative literal appears are part of that constraint. So a call to undo() on a constraint that does contains the literal will occur.
Worst, it is necessary to perform the undo both on the literal and its oppositve in that case, to properly undo all constraints.
In our testcases, the PB constraints are encoding the objective function and are deleted after each PI computation, so the current fix is simply to avoid a NPE that occurs when the undo() method is applied on a constraint not associated by such literal.
We are currently working on a new PI computation scheme, so that code with forget will eventually be removed. The current fix allows the solver to be correct, and prevents NPE to occur.https://gitlab.ow2.org/sat4j/sat4j/-/issues/88Avoid calling visualization code when no visualization is needed2018-04-13T11:56:17ZDaniel Le BerreAvoid calling visualization code when no visualization is neededWhen using the sat4j-sat.jar package without option (to discover them) on a machine without X server (a cluster), the app throws an exception because it tries to access X related features.
Exception in thread "main" java.lang.ExceptionI...When using the sat4j-sat.jar package without option (to discover them) on a machine without X server (a cluster), the app throws an exception because it tries to access X related features.
Exception in thread "main" java.lang.ExceptionInInitializerError
at java.lang.Class.forName0(Native Method)
at java.lang.Class.forName(Class.java:169)
at org.sat4j.sat.RTSI.findnames(Unknown Source)
at org.sat4j.sat.RTSI.find(Unknown Source)
at org.sat4j.sat.RTSI.find(Unknown Source)
at org.sat4j.sat.RTSI.find(Unknown Source)
at org.sat4j.sat.Solvers.showAvailableRestarts(Unknown Source)
at org.sat4j.sat.Solvers.usage(Unknown Source)
at org.sat4j.sat.Launcher.usage(Unknown Source)
at org.sat4j.sat.Launcher.run(Unknown Source)
at org.sat4j.sat.Launcher.main(Unknown Source)
Caused by: java.awt.HeadlessException:
No X11 DISPLAY variable was set, but this program performed an operation which requires it.
at sun.awt.HeadlessToolkit.getScreenSize(HeadlessToolkit.java:261)
at org.sat4j.sat.RemoteControlFrame.<clinit>(Unknown Source)
... 11 more
Such code should only be launched when the visualization option is set.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/86Add Glucose 21 dynamic restart strategy and enable it by default2018-04-13T11:56:13ZDaniel Le BerreAdd Glucose 21 dynamic restart strategy and enable it by defaultThe new Dynamic restart strategy of Glucose 2.1 has been presented in "Refining restarts strategies for SAT and UNSAT formulae. Gilles Audemard and Laurent Simon, in proceedings of CP'2012".
That dynamic restart strategy is going to be ...The new Dynamic restart strategy of Glucose 2.1 has been presented in "Refining restarts strategies for SAT and UNSAT formulae. Gilles Audemard and Laurent Simon, in proceedings of CP'2012".
That dynamic restart strategy is going to be Sat4j default instead of Armin Biere's In/Out rapid Restart strategy.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/85Allow easy access to a pseudo boolean optimizer2018-04-13T11:56:14ZDaniel Le BerreAllow easy access to a pseudo boolean optimizerWhen a newcomer to Sat4j wants to solve a pseudo boolean optimization problems, it usually takes the PB solver available in SolverFactory.newDefault(), which looks ok from a user point of view.
However, by default, a PB solver does not ...When a newcomer to Sat4j wants to solve a pseudo boolean optimization problems, it usually takes the PB solver available in SolverFactory.newDefault(), which looks ok from a user point of view.
However, by default, a PB solver does not perform any optimization. The optimization is performed by a generic procedure on IOptimizationProblem.
The PseudoOptDecorator provides the IOptimizationProblem capability to IPBSolver.
The optimization can then be performed using an OptToPBSATAdapter object.
That process allows the power user to build custom PB optimizers but makes difficult the usage of the library for most users that really just pick the default settings.
The idea is to add a new method in the SolverFactory, newDefaultOptimizer, to provide a ready to use optimizer.
2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/72Print the statistics of all solvers in manycore2018-04-13T11:56:15ZDaniel Le BerrePrint the statistics of all solvers in manycoreCurrently, only the statistics of the winner are displayed. We should display the statistics of all solvers.Currently, only the statistics of the winner are displayed. We should display the statistics of all solvers.https://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/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/45Separate MS and PWMS decorator from the optimization method2018-07-07T05:11:53ZDaniel Le BerreSeparate MS and PWMS decorator from the optimization methodSince we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the probl...Since we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the problem, it should delegate that to a PseudoOptDecorator or a ConstraintRelaxingPseudoOptDecorator.
Since we use here new variables, it means updating the current pseudo-opt decorators to deal with additional variables.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/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/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.1