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/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/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/91MSS that are computed by AllMUSes class are not always maximal in the group case2018-04-13T11:56:15ZStéphanie ROUSSELMSS that are computed by AllMUSes class are not always maximal in the group caseLet us consider the base {b & c, b & d, a & c, -a | -b}, -a | -b being a constraint.
MSS should be {b & c , b & d} and {a & c} i.e. {g1,g2} and {g3} but the solver returns {g3}, {g2}, {g1,g2} i.e. {a & c}, {b & d} and {b & d, b & c}. Th...Let us consider the base {b & c, b & d, a & c, -a | -b}, -a | -b being a constraint.
MSS should be {b & c , b & d} and {a & c} i.e. {g1,g2} and {g3} but the solver returns {g3}, {g2}, {g1,g2} i.e. {a & c}, {b & d} and {b & d, b & c}. The second set is clearly not a MUS.
This problem might be linked to the use of unitary clauses.
2.3.4https://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/89wrong model?2018-04-13T11:56:13ZMihai Barbuceanuwrong model?Hi,
I am using the GateTransalator to input a problem and I do something like that:
assuming gate is the GateTranslator used, I set gate.gateTrue(...) for:
(and (or v1 v2 v3)
(atmost 1 v1 v2 v3)
(or v4))
Then I do gate.gate...Hi,
I am using the GateTransalator to input a problem and I do something like that:
assuming gate is the GateTranslator used, I set gate.gateTrue(...) for:
(and (or v1 v2 v3)
(atmost 1 v1 v2 v3)
(or v4))
Then I do gate.gateTrue for:
(atleast 1 v4 v5)
Then I run the solver and collect all models. The issue is I get solutions containing v5 = true, (e.g. v1=true, v5=true) which I think it's wrong if both of the above are true. Am I misinterpreting something?
(The problem looks like that because is generated in a rather complex way from a business interface)
Thanks a lot
Mihaihttps://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/87exploding runtime in case of repeated calls for satisfiability2018-04-13T11:56:12ZSebastian Grafexploding runtime in case of repeated calls for satisfiabilityIf the same VariableOrder is set in the solver (or a new instance of an VariableOrder, that is identically configured) and again run solver.isSatisfiable() the required runtime for the single call increases by about the factor of 1.5 eac...If the same VariableOrder is set in the solver (or a new instance of an VariableOrder, that is identically configured) and again run solver.isSatisfiable() the required runtime for the single call increases by about the factor of 1.5 each time this is done.
e.g. the following code-snipped will increase the runtime of a single isSatisfiable()-call by approximately the factor of 3000 (1.5^20)
for(int i=0; i<20, i++) {
solver.setOrder(o);
solver.isSatisfiable();
}
The problem is not existing in case of using Sat4j up to revision 1176, but is visible in each newer revision - I have tested multiple revisions.
Moreover, in case of revisions between 1177 and 1206 the behavior is even worse (I was even not able to get the same variable order evaluated multiple times, e.g. i get a timeout). Thus, it could be seen with revision 1207 and is still existing in the lates revision. (checked up to revision 1732)
What I also could find out and what confused me a bit (and what seems to cause the runtime-explosion) is, that with the same variable order and variable settings, each "multiple call of setOrder() and isSatisfiable()" causes immensly increase in the number of found conflics and, thus, required thousands or millons of search() calls within the solver.
Regards,
Sebastian2.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/84Maxsat fails with java.lang.ArrayIndexOutOfBoundsException2018-04-13T11:56:17ZMichael TautschnigMaxsat fails with java.lang.ArrayIndexOutOfBoundsExceptionOn the following trivial problem
p wcnf 401432 1 729
729 -378671 59559 0
sat4j 2.3.2 fails with the following error (this works fine in 2.3.1 built on the same machine):
c declared #vars 401432
c #constraints 1
c constraints ...On the following trivial problem
p wcnf 401432 1 729
729 -378671 59559 0
sat4j 2.3.2 fails with the following error (this works fine in 2.3.1 built on the same machine):
c declared #vars 401432
c #constraints 1
c constraints type
c org.sat4j.minisat.constraints.cnf.OriginalBinaryClause => 1
c 1 constraints processed.
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 378671
at org.sat4j.minisat.core.Solver.primeImplicant(Unknown Source)
at org.sat4j.tools.SolverDecorator.primeImplicant(Unknown Source)
at org.sat4j.pb.ObjectiveFunction.calculateDegreeImplicant(Unknown Source)
at org.sat4j.pb.PseudoOptDecorator.calculateObjective(Unknown Source)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(Unknown Source)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(Unknown Source)
at org.sat4j.AbstractOptimizationLauncher.solve(Unknown Source)
at org.sat4j.AbstractLauncher.run(Unknown Source)
at org.sat4j.maxsat.GenericOptLauncher.main(Unknown Source)
Best,
Michael2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/83Allow JSON I/O for embedded applications2018-04-13T11:56:17ZDaniel Le BerreAllow JSON I/O for embedded applicationsIn order to lower the cost of using Sat4j in a mobile device, it would be nice to allow interacting with the solver using the JSON format.
It is not a problem to read Dimacs formatted input that way: the CNF would be a list of list of n...In order to lower the cost of using Sat4j in a mobile device, it would be nice to allow interacting with the solver using the JSON format.
It is not a problem to read Dimacs formatted input that way: the CNF would be a list of list of non null integers.
The answer would be either "true" associated with a model (list of satisfied literals) or "false" associated with the empty list.
We probably also need to consider the case in which the solver cannot answer ("unknown").
It is not clear if offering a Dimacs interface in JSON really makes sense for the end user, or if the input should be a string based propositional variables and that the mapping should be managed by the solver.
Another issue is the represent cardinality constraints and pseudo boolean constraints.
Would {"literals": {1,-2,3,-4,5}, "op"="=", "degree":3} be ok to represent for instance x1 + \lnot x2 + x3 + \lnot x4 + x5 = 3 cardinality constraint?
2.3.3https://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/81ISolver.findModel(VecInt) is affected by previous call2018-04-13T11:56:12ZIngo ReimundISolver.findModel(VecInt) is affected by previous callIn my project i use sat4-sat to check satisfiable of different literals agains one set of constraints. So i found a situation, in which one call of solver.findModel(IVecInt) have an affect to the next one.
In the attachted file, you fin...In my project i use sat4-sat to check satisfiable of different literals agains one set of constraints. So i found a situation, in which one call of solver.findModel(IVecInt) have an affect to the next one.
In the attachted file, you find my junit test which fails, but if you comment out "bound5" with the corresponding solver call everything will be fine.
The importend part of this test, are the last three lines. This lines check if literal 1, 2 and 4 are part of the solution. 1 have to be part of the solution, because this literal is part of a clause which have no other lierals. 2 should be true, because 1 is it.
This part of the test fails if and only if i search for a solution with 4 and -3.2.3.2https://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/79Solver leaks timer threads accross reuse2018-04-13T11:56:16ZDaniel Le BerreSolver leaks timer threads accross reuseThe SAT solver uses the java.util.Timer class to stop the solver after a given timeout.
```
boolean firstTimeGlobal = false;
if (this.timeBasedTimeout) {
if (!global || this.timer == null) {
if (thi...The SAT solver uses the java.util.Timer class to stop the solver after a given timeout.
```
boolean firstTimeGlobal = false;
if (this.timeBasedTimeout) {
if (!global || this.timer == null) {
if (this.timer != null) {
this.timer.cancel();
}
firstTimeGlobal = true;
this.undertimeout = true;
TimerTask stopMe = new TimerTask() {
@Override
public void run() {
Solver.this.undertimeout = false;
}
};
this.timer = new Timer(true);
this.timer.schedule(stopMe, this.timeout);
}
}
```
When calling several time the method isSatisfiable on a solver, the solver creates for each call a new timer thread, due to the Timer.schedule() method.
This is a big issue because a thread stack is created for each thread, thus quickly the solver is running out of memory in those conditions.
https://gitlab.ow2.org/sat4j/sat4j/-/issues/78Not able to run the pseudo boolean solver at all2018-04-13T11:56:17ZJayalakshmi BalasubramaniamNot able to run the pseudo boolean solver at allI have downloaded the sat solver and pseudo boolean solvers' respective jar files. I am able to run the sat solver on command line and I get the expected output. But, when I give an input parameter(.opb file) to the pseudo boolean solver...I have downloaded the sat solver and pseudo boolean solvers' respective jar files. I am able to run the sat solver on command line and I get the expected output. But, when I give an input parameter(.opb file) to the pseudo boolean solver and try to run the respective jar with the parameter from command line it always gives a parseInstance error. I dont know how to resolve this issue. All help appreciated.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/76Intermediate results not displayed during optimization2018-04-13T11:56:16ZDaniel Le BerreIntermediate results not displayed during optimizationIn 2.3.2, the verbose mode in OptToPBSatAdapter.model() is using a printwriter
to display the messages. The default printwriter using stdout is not autoflushing by default, so the content is not displayed on the console.
The fix is easy:...In 2.3.2, the verbose mode in OptToPBSatAdapter.model() is using a printwriter
to display the messages. The default printwriter using stdout is not autoflushing by default, so the content is not displayed on the console.
The fix is easy: just enable autoflush.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/75create a toString method for negated objects within Dependency Helper2018-04-13T11:56:15ZDaniel Le Berrecreate a toString method for negated objects within Dependency HelperWhen an object is negated using the DependencyHelper class, the negated object does not have a nice toString() method.
Should use the classical "-" prefix in front of the object name to show that it is negated.When an object is negated using the DependencyHelper class, the negated object does not have a nice toString() method.
Should use the classical "-" prefix in front of the object name to show that it is negated.2.3.3