Commit 85553c0e authored by Daniel Le Berre's avatar Daniel Le Berre

Added some statistics regarding the number of positive additional variables removed.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2134 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 5e9044d8
......@@ -94,6 +94,7 @@ public class CounterBasedPrimeImplicantStrategy implements
this.prime[Math.abs(d)] = d;
}
int removed = 0;
int posremoved = 0;
int propagated = 0;
top: for (int i = 0; i < solver.decisions.size(); i++) {
d = solver.decisions.get(i);
......@@ -106,6 +107,9 @@ public class CounterBasedPrimeImplicantStrategy implements
}
}
removed++;
if (d > 0 && d > solver.nVars()) {
posremoved++;
}
for (IteratorInt it = watched[toInternal(d)].iterator(); it
.hasNext();) {
count[it.next()]--;
......@@ -124,10 +128,10 @@ public class CounterBasedPrimeImplicantStrategy implements
"%s prime implicant computation statistics ALGO2%n",
solver.getLogPrefix());
System.out
.printf("%s implied: %d, decision: %d (removed %d, propagated %d), time(ms):%d %n",
.printf("%s implied: %d, decision: %d, removed %d (+%d), propagated %d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, propagated, end
- begin);
solver.decisions.size(), removed, posremoved,
propagated, end - begin);
}
return implicant;
}
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import static org.sat4j.core.LiteralsUtils.neg;
import static org.sat4j.core.LiteralsUtils.toInternal;
import org.sat4j.specs.IConstr;
......@@ -47,6 +48,22 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
private int[] prime;
/**
* Assume literal p and perform unit propagation
*
* @param p
* a literal
* @return true if no conflict is reached, false if a conflict is found.
*/
boolean setAndPropagate(Solver<? extends DataStructureFactory> solver, int p) {
if (solver.voc.isUnassigned(p)) {
assert !solver.trail.contains(p);
assert !solver.trail.contains(neg(p));
return solver.assume(p) && solver.propagate() == null;
}
return solver.voc.isSatisfied(p);
}
public int[] compute(Solver<? extends DataStructureFactory> solver) {
assert solver.qhead == solver.trail.size()
+ solver.learnedLiterals.size();
......@@ -69,12 +86,13 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
d = it.next();
p = toInternal(d);
prime[Math.abs(d)] = d;
noproblem = solver.setAndPropagate(p);
noproblem = setAndPropagate(solver, p);
assert noproblem;
}
boolean canBeRemoved;
int rightlevel;
int removed = 0;
int posremoved = 0;
int propagated = 0;
int tested = 0;
int l2propagation = 0;
......@@ -86,14 +104,14 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
// d has been propagated
prime[Math.abs(d)] = d;
propagated++;
} else if (solver.setAndPropagate(toInternal(-d))) {
} else if (setAndPropagate(solver, toInternal(-d))) {
canBeRemoved = true;
tested++;
rightlevel = solver.currentDecisionLevel();
for (int j = i + 1; j < solver.decisions.size(); j++) {
l2propagation++;
if (!solver.setAndPropagate(toInternal(solver.decisions
.get(j)))) {
if (!setAndPropagate(solver,
toInternal(solver.decisions.get(j)))) {
canBeRemoved = false;
break;
}
......@@ -105,18 +123,21 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
IConstr confl = solver.propagate();
assert confl == null;
removed++;
if (d > 0 && d > solver.nVars()) {
posremoved++;
}
} else {
prime[Math.abs(d)] = d;
solver.cancel();
assert solver.voc.isUnassigned(toInternal(d));
noproblem = solver.setAndPropagate(toInternal(d));
noproblem = setAndPropagate(solver, toInternal(d));
assert noproblem;
}
} else {
// conflict, literal is necessary
prime[Math.abs(d)] = d;
solver.cancel();
noproblem = solver.setAndPropagate(toInternal(d));
noproblem = setAndPropagate(solver, toInternal(d));
assert noproblem;
}
}
......@@ -134,10 +155,10 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
"%s prime implicant computation statistics ORIG%n",
solver.getLogPrefix());
System.out
.printf("%s implied: %d, decision: %d (removed %d, tested %d, propagated %d), l2 propagation:%d, time(ms):%d %n",
.printf("%s implied: %d, decision: %d, removed %d (+%d), tested %d, propagated %d), l2 propagation:%d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, tested,
propagated, l2propagation, end - begin);
solver.decisions.size(), removed, posremoved,
tested, propagated, l2propagation, end - begin);
}
return implicant;
......
......@@ -29,7 +29,6 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import static org.sat4j.core.LiteralsUtils.neg;
import static org.sat4j.core.LiteralsUtils.toDimacs;
import static org.sat4j.core.LiteralsUtils.toInternal;
import static org.sat4j.core.LiteralsUtils.var;
......@@ -1363,22 +1362,6 @@ public class Solver<D extends DataStructureFactory> implements ISolverService,
return confl;
}
/**
* Assume literal p and perform unit propagation
*
* @param p
* a literal
* @return true if no conflict is reached, false if a conflict is found.
*/
boolean setAndPropagate(int p) {
if (voc.isUnassigned(p)) {
assert !trail.contains(p);
assert !trail.contains(neg(p));
return assume(p) && propagate() == null;
}
return voc.isSatisfied(p);
}
private int[] prime;
public int[] primeImplicant() {
......
......@@ -72,13 +72,17 @@ public class WatcherBasedPrimeImplicantStrategy implements
isMandatory(solver.trail.get(i));
}
for (int d : solver.fullmodel) {
solver.assume(toInternal(d));
p = toInternal(d);
if (solver.voc.isUnassigned(p)) {
solver.assume(p);
}
}
for (int d : solver.fullmodel) {
reduceClausesContainingTheNegationOfPI(solver, toInternal(d));
}
int removed = 0;
int posremoved = 0;
int propagated = 0;
for (int d : solver.fullmodel) {
if (this.prime[Math.abs(d)] != 0) {
......@@ -89,6 +93,9 @@ public class WatcherBasedPrimeImplicantStrategy implements
solver.forget(Math.abs(d));
reduceClausesContainingTheNegationOfPI(solver, toInternal(-d));
removed++;
if (d > 0 && d > solver.nVars()) {
posremoved++;
}
}
}
solver.cancelUntil(0);
......@@ -105,10 +112,10 @@ public class WatcherBasedPrimeImplicantStrategy implements
"%s prime implicant computation statistics BRESIL%n",
solver.getLogPrefix());
System.out
.printf("%s implied: %d, decision: %d (removed %d, propagated %d), time(ms):%d %n",
.printf("%s implied: %d, decision: %d, removed %d (+%d), propagated %d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, propagated, end
- begin);
solver.decisions.size(), removed, posremoved,
propagated, end - begin);
}
return implicant;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment