sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-04-13T11:56:14Zhttps://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/118Crashes with NPE after call to unsatExplanation()2018-04-13T11:56:17ZRobert StelzmannCrashes with NPE after call to unsatExplanation()- created a solver with SolverFactory.newLight() respectively SolverFactory.newDefault()
- ran it via isSatisfiable()
-> call to unsatExplanation() leads to a NPE, since unsatExplanationInTermsOfAssumptions is null.- created a solver with SolverFactory.newLight() respectively SolverFactory.newDefault()
- ran it via isSatisfiable()
-> call to unsatExplanation() leads to a NPE, since unsatExplanationInTermsOfAssumptions is null.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/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/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/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 ...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.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/129Timeout should be in ms, not s2018-11-12T16:04:57ZDaniel Le BerreTimeout should be in ms, not sReceived from Arnaud Malapert:
Je crois qu'il y a une erreur dans le message de la TimeoutException.
Dans la classe Solver :
```
if (!undertimeout) {
String message = " Timeout (" + timeout
+ (timeBase...Received from Arnaud Malapert:
Je crois qu'il y a une erreur dans le message de la TimeoutException.
Dans la classe Solver :
```
if (!undertimeout) {
String message = " Timeout (" + timeout
+ (timeBasedTimeout ? "s" : " conflicts") + ") exceeded";
throw new TimeoutException(message); //$NON-NLS-1$//$NON-NLS-2$
}
```
Il me semble que timeout est en millisecondes plutôt qu'en secondes.https://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 +...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/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/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 segmentatio...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/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/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/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!".