sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-04-13T11:56:15Zhttps://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/99Added unsat proof capability to Sat4j2018-04-13T11:56:15ZDaniel Le BerreAdded unsat proof capability to Sat4jMore and more applications require a certified unsat answer. The SAT competition 2013 has a certified unsat track. A simple proof format for SAT solver developers is the Reverse Unit Propagation format (RUP).
Such proof format can easil...More and more applications require a certified unsat answer. The SAT competition 2013 has a certified unsat track. A simple proof format for SAT solver developers is the Reverse Unit Propagation format (RUP).
Such proof format can easily be added to the library as a specific SearchListener.2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/101CSReader doesn't throws a ContradictionException when adding conflicting clau...2018-04-13T11:56:15ZHector M chavezCSReader doesn't throws a ContradictionException when adding conflicting clauses.When parsing a CSP instance using XMLCSPReader, it doesn't throw a ContradictionException for conflicting clauses. It only prints a message to the console.
Ex:
...
XMLCSPReader reader = new XMLCSPReader(solver, true);
try {
reader....When parsing a CSP instance using XMLCSPReader, it doesn't throw a ContradictionException for conflicting clauses. It only prints a message to the console.
Ex:
...
XMLCSPReader reader = new XMLCSPReader(solver, true);
try {
reader.parseInstance(file); // Console output: c INSTANCE TRIVIALLY UNSAT
if(problem.isSatisfiable()){ // Returns true
//
}
} catch (ContradictionException e) {
System.out.println("Contradiction"); // Should be thrown by parseInstance
}
The ContradictionException is catched by method endConstraint() in org.sat4j.CSPReader.java and it prints the message. After that happens there is no way of knowing it was TRIVIALLY UNSAY.
2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/103Computing MUSes Silently2018-04-13T11:56:15ZFatih TurkmenComputing MUSes SilentlyI have been checking the implementation of AllMUSes class. I would like to get the time necessary to find (I know that different solvers can be used here for different purpoes..)
1. One (subset)
2. Cardinality minimal
3. All MUSes (all s...I have been checking the implementation of AllMUSes class. I would like to get the time necessary to find (I know that different solvers can be used here for different purpoes..)
1. One (subset)
2. Cardinality minimal
3. All MUSes (all subset minimals, computeAllMUSes() method)
However, I have the following issue regarding the MUS solver. It outputs to console all MUSes and MSSes even if I set verbosity to false. Is it possible to disable this? I think there is a problem in managing the output streams... I am checking the code here with no success yet:
http://websvn.ow2.org/filedetails.php?repname=sat4j&path=%2Fmaven%2Ftrunk%2Forg.sat4j.core%2Fsrc%2Fmain%2Fjava%2Forg%2Fsat4j%2Ftools%2FAllMUSes.javahttps://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/108Lack of 2.3.5 tag for sat4j2018-04-13T11:56:15ZKrzysztof DanielLack of 2.3.5 tag for sat4jThere is no tag in the repo for 2.3.5 release. This is a big problem for me as I can't rebuild sat4j in Fedora, and therefore can't build Eclipse.There is no tag in the repo for 2.3.5 release. This is a big problem for me as I can't rebuild sat4j in Fedora, and therefore can't build Eclipse.https://gitlab.ow2.org/sat4j/sat4j/-/issues/111Iteration through all possible solutions didn't find all possible solutions2018-04-13T11:56:15ZSascha El-sharkawyIteration through all possible solutions didn't find all possible solutionsHello,
I downloaded a dimacs translation of the Linux kernel 2.6.33 (http://formulas.linux-variability-analysis-tools.googlecode.com/hg/2.6.33.3-2var.dimacs, I removed the 2 blank lines at the end of the file). And tried it to reason it ...Hello,
I downloaded a dimacs translation of the Linux kernel 2.6.33 (http://formulas.linux-variability-analysis-tools.googlecode.com/hg/2.6.33.3-2var.dimacs, I removed the 2 blank lines at the end of the file). And tried it to reason it with Sat4j 2.3.4 (http://forge.ow2.org/project/download.php?group_id=228&file_id=19075). I tried 2 different possibilities to iterate through all possible solutions:
1. With a loop over problem.isSatisfiable() (c.f. http://www.sat4j.org/howto.php#models).
2. With the ModelIterator (c.f http://www.sat4j.org/maven21/org.sat4j.core/apidocs/org/sat4j/tools/ModelIterator.html).
I saved all found solutions to my hard disk and compared each other with a diff tool. Only the first 6 solutions are different, all other models are equal to the 6st solution.
I tried also another possibility; iterating through all variables and adding a constraint to the complete model, that this variable must be true. Excerpt from my code:
```
Reader reader = new DimacsReader(solver);
for (int i = 1; i <= problem.nVars(); i++) {
int[] varAssignment = {i};
int configNo = 0;
List<int[]> foundSolutions = new ArrayList<int[]>();
try {
solver.addClause(new VecInt(varAssignment));
if(solver.isSatisfiable()) {
System.out.println("Created Configuration No. " + configNo);
int[] newModel = problem.model();
if (!compareSolutions(foundSolutions, newModel)) {
saveModel(folder, configNo);
foundSolutions.add(newModel);
configNo++;
}
}
} catch (ContradictionException e) {
System.out.println("Empty clause added. This model will be skipped.");
}
reader.parseInstance(filename); // Reset model
}
```
The third options find more than 6 different solutions. Can anybody explain my why the documented iterators only find 6 solutions? I guess this is a bug, or did I used sat4J wrong?
Best regards,
Sascha El-Sharkawy
https://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/139Invalid multiple solutions with call to isSatisfiable(true) in ModelIterator2018-04-13T11:56:15ZMark EngelbergInvalid multiple solutions with call to isSatisfiable(true) in ModelIteratorI am generating multiple solutions for a sat problem in the following way:
Create the default solver.
Call the newVar method with exactly the number of variables in my problem.
Call the setExpectedNumberOfClauses method with exactly the...I am generating multiple solutions for a sat problem in the following way:
Create the default solver.
Call the newVar method with exactly the number of variables in my problem.
Call the setExpectedNumberOfClauses method with exactly the number of clauses (not including the added "exactly" constraint).
Call addClause multiple times to add all the clauses.
Call addExactly to add one "exactly" constraint.
Call isSatisfiable(true) and when this returns true, call model() to get one of the solutions to my problem.
Then, I use addBlockingClause to add the exact opposite of the solution (i.e., negating all the numbers in the solution) to the solver.
I continue by again calling isSatisfiable(true) and if this returns true, call model() to get the next solution to my problem.
I repeat this process until isSatisfiable(true) returns false.
What I am finding is that subsequent calls to isSatisfiable after the first solution is found and I call addBlockingClause to block that solution *do not* respect the "exactly" constraint I have imposed on the solver.
Is this a known problem? Is my strategy for getting multiple solutions sound? Is there a workaround, for example, should I re-assert the exact constraints each time I add a blocking clause?2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/71Add statistics in ManyCore solvers on the solvers that answers 2018-04-13T11:56:14ZDaniel Le BerreAdd statistics in ManyCore solvers on the solvers that answers When using a manycore solver, it would be nice to have some statistics concerning the solvers that have been used to compute the solutions.When using a manycore solver, it would be nice to have some statistics concerning the solvers that have been used to compute the solutions.2.3.2https://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/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/117Timers are not correctly released when performing optimization2018-04-13T11:56:14ZDaniel Le BerreTimers are not correctly released when performing optimizationIan Bull reported that using Sat4j 2.3.5 with eclipse, when calling thousands of time Sat4j, most timers were not released.
Ian Bull reported that using Sat4j 2.3.5 with eclipse, when calling thousands of time Sat4j, most timers were not released.
2.3.6https://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/131Sat4j maxsat does not pick the right reader with an arbitrary extension2018-04-13T11:56:14ZDaniel Le BerreSat4j maxsat does not pick the right reader with an arbitrary extensionWhen a new user of sat4j tries to solve a partial weighted maxsat problem, it is likely that the extension used may not be the expected wcnf.
In that case, the default solver is the cnf one, which will wrongly interpret the content of t...When a new user of sat4j tries to solve a partial weighted maxsat problem, it is likely that the extension used may not be the expected wcnf.
In that case, the default solver is the cnf one, which will wrongly interpret the content of the file, i.e. will treat the first number, the weight, as a literal.
There are several ways to solve this:
- do not use the extension to decide of the reader
- display an error message if the wncf extension is seen by the classical Dimacs reader.
The latter is probably the best option.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/137DependencyHelper corrupts existing constraints2018-04-13T11:56:14ZRobert GiegerichDependencyHelper corrupts existing constraintsOriginally I added constraints directly with methods of the solver object. As I want to add implications with more comfort, I tried to switch to DependencyHelper.
```
FOREACH ASSIGNMENT:
solver.addExactly(new VecInt(zap.toArray), 1)
FO...Originally I added constraints directly with methods of the solver object. As I want to add implications with more comfort, I tried to switch to DependencyHelper.
```
FOREACH ASSIGNMENT:
solver.addExactly(new VecInt(zap.toArray), 1)
FOREACH TEACHER:
solver.addAtLeast(new VecInt(vars.toArray), new VecInt(weights.toArray), number)
solver.addAtLeast(new VecInt(vars.toArray), new VecInt(weights.toArray), number)
{code}
becomes
{code:title=Solution invalid}
FOREACH ASSIGNMENT:
depHelper.atLeast("Require at least one teacher for " + key, 1, zap.toArray:_*)
depHelper.atMost("Require at most one teacher for " + key, 1, zap.toArray:_*)
FOREACH TEACHER:
depHelper.atLeast("Hours at least " + number + " of " + variables, number, weightedVariables:_*)
depHelper.atMost("Hours at most " + number+ " of " + variables, number, weightedVariables:_*)
```
Now the solver presents an invalid solution, breaking some "Exactly one assignment"-constraints in both ways: Sometimes no teacher is assigned, sometimes several teachers are. When I leave out the constraints limiting the teacher's work hours, the solution is valid.
The DependencyHelper is of type \[Int,String\], but i also found this result when using my own type as "T" (\[DecisionVar,String\]).2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/141"OW2 Forge"-link dead on www.sat4j.org2018-04-13T11:56:14ZGhost User"OW2 Forge"-link dead on www.sat4j.orgThe link "OW2 Forge" (to http://sat4j.ow2.org/) on the website www.sat4j.org is broken. The URL "http://sat4j.ow2.org/" points to a page which only says "It works!".The link "OW2 Forge" (to http://sat4j.ow2.org/) on the website www.sat4j.org is broken. The URL "http://sat4j.ow2.org/" points to a page which only says "It works!".https://gitlab.ow2.org/sat4j/sat4j/-/issues/77Allow dependencyHelper to return the truth value of a negated object2018-04-13T11:56:13ZDaniel Le BerreAllow dependencyHelper to return the truth value of a negated objectCurrently, the dependencyHelper does not allow to retrieve the truth value of a negated object. This can be a problem in practice (we actually need it for MISC 2012).Currently, the dependencyHelper does not allow to retrieve the truth value of a negated object. This can be a problem in practice (we actually need it for MISC 2012).2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/80Allow lexicographic optimization from OPB files2018-04-13T11:56:13ZDaniel Le BerreAllow lexicographic optimization from OPB filesSat4j supports currently lexicographic optimization for several linear optimization functions using the API.
It would be nice to allow the end user to define those optimizations functions directly in an OPB file, using several min: lines.Sat4j supports currently lexicographic optimization for several linear optimization functions using the API.
It would be nice to allow the end user to define those optimizations functions directly in an OPB file, using several min: lines.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.3