sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-04-13T11:56:17Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/110Remove propagated literals when removing a PB constraint2018-04-13T11:56:17ZDaniel Le BerreRemove propagated literals when removing a PB constraintIt may happen in some cases that a PB constraint propagates literals at decision zero.
In case of clauses or cardinality constraints, a unit clause of a set of unit clauses are returned, so when those constraints are removed, they are removed from the trail.
In the case of PB constraints, the propagated literals are not associated to unit clauses. As such, the remove method in PB constraint should take care to remove from the trail the implied literals (the ones pushed at decision level 0).
The issue was discovered by Yacoub in the context of maxsat solving using lower bounding.It may happen in some cases that a PB constraint propagates literals at decision zero.
In case of clauses or cardinality constraints, a unit clause of a set of unit clauses are returned, so when those constraints are removed, they are removed from the trail.
In the case of PB constraints, the propagated literals are not associated to unit clauses. As such, the remove method in PB constraint should take care to remove from the trail the implied literals (the ones pushed at decision level 0).
The issue was discovered by Yacoub in the context of maxsat solving using lower bounding.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/106release jars do not include debug information2018-04-13T11:56:16ZDaniel Le Berrerelease jars do not include debug informationThe jar currently produced by our ant script does not provide jars with debug information included. As such, if an error occurs, there is not reference to the line number in the stack trace.The jar currently produced by our ant script does not provide jars with debug information included. As such, if an error occurs, there is not reference to the line number in the stack trace.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/130Support unused variables in the objective function when the optimization prob...2018-04-13T11:56:16ZDaniel Le BerreSupport unused variables in the objective function when the optimization problem is trivialDuring the PB15, an issue was discovered when variables not used in the CNF appear in the objective function and that the optimal solution is found directly.
Here is a simple test case:
[code]
* #variable= 3 #constraint= 1
min: +1 x1 +1 x2 +1 x3 ;
+1 x3 +1 x2 = 1;
[/code]
The solver will find a first model x2 -x3 for instance which satisfes the constraint.
The solver adds a constraint x1 + x2 +x3 < 1 which makes the formula UNSAT.
As such, the previous model, without mention of x1 is returned.
We need to detect that case, and to complete the model by falsifying the literals found in the objective function.
Detecting that situation is easy. Fixing properly the model requires a bit of work.During the PB15, an issue was discovered when variables not used in the CNF appear in the objective function and that the optimal solution is found directly.
Here is a simple test case:
[code]
* #variable= 3 #constraint= 1
min: +1 x1 +1 x2 +1 x3 ;
+1 x3 +1 x2 = 1;
[/code]
The solver will find a first model x2 -x3 for instance which satisfes the constraint.
The solver adds a constraint x1 + x2 +x3 < 1 which makes the formula UNSAT.
As such, the previous model, without mention of x1 is returned.
We need to detect that case, and to complete the model by falsifying the literals found in the objective function.
Detecting that situation is easy. Fixing properly the model requires a bit of work.2.3.6https://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/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)
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\]).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/135Sat4j not terminating2015-11-09T16:03:01ZAnithaSat4j not terminatingI am using pseudo boolean solver to find minimize an objective function. sat4j worked fine for small examples. However, with the attached testcase, it runs indefinitely. Moreover, whats confusing is: After 1hr or so, it gives segmentation fault 11 in my terminal but the process still runs in background. I am confused.
23230 ttys001 67:08.18 /usr/bin/java -jar /Users/.../sat4j/sat4j-pb.jar min.opb
Attaching testcase in opb format. It consists of non-linear constraints. I am not sure if something is wrong with the testcase. It looks fine to me.
Appreciate reply as soon as possible.
I am using pseudo boolean solver to find minimize an objective function. sat4j worked fine for small examples. However, with the attached testcase, it runs indefinitely. Moreover, whats confusing is: After 1hr or so, it gives segmentation fault 11 in my terminal but the process still runs in background. I am confused.
23230 ttys001 67:08.18 /usr/bin/java -jar /Users/.../sat4j/sat4j-pb.jar min.opb
Attaching testcase in opb format. It consists of non-linear constraints. I am not sure if something is wrong with the testcase. It looks fine to me.
Appreciate reply as soon as possible.
2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/124Lexico-Optimization does not work with ManyCore (parallel) solvers.2015-01-15T09:23:22ZDaniel Le BerreLexico-Optimization does not work with ManyCore (parallel) solvers.During the LION 9 challenge, two versions of Sat4j was used.
That challenge is about solving multi-objective boolean functions, in that case lexicographic one.
The pure resolution based one worked fine while the one using the parallel solver Both answered sub-optimal solutions.
The parallel solver has been used successfully for years on PB benchmarks.
The main issue with lexicographic optimization is that an UNSAT answer is not final contrariwise to the mono-objective optimization.
Initial investigation of the problem shows that the parallel solvers always answer UNSAT after a while.During the LION 9 challenge, two versions of Sat4j was used.
That challenge is about solving multi-objective boolean functions, in that case lexicographic one.
The pure resolution based one worked fine while the one using the parallel solver Both answered sub-optimal solutions.
The parallel solver has been used successfully for years on PB benchmarks.
The main issue with lexicographic optimization is that an UNSAT answer is not final contrariwise to the mono-objective optimization.
Initial investigation of the problem shows that the parallel solvers always answer UNSAT after a while.2.3.6