Commit 4c0ef9f3 authored by Daniel Le Berre's avatar Daniel Le Berre

Improved the backbone algorithm by reducing the number of SAT calls by one...

Improved the backbone algorithm by reducing the number of SAT calls by one order to magnitude on BR4CP renault benchmarks.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2214 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent d4b4498a
......@@ -79,7 +79,8 @@ final class DecisionMode implements ILauncherMode {
long beginpi = System.currentTimeMillis();
model = solver.primeImplicant();
try {
IVecInt backbone = Backbone.compute(solver, model);
IVecInt backbone = Backbone.instance().compute(solver,
model);
long endpi = System.currentTimeMillis();
out.print(solver.getLogPrefix());
reader.decode(backbone.toArray(), out);
......
......@@ -78,6 +78,12 @@ public class MinWatchCard implements Propagatable, Constr, Undoable,
*/
private final ILits voc;
/**
* Maximum number of falsified literal in the constraint.
*
*/
private final int maxUnsatisfied;
/**
* Constructs and normalizes a cardinality constraint. used by
* minWatchCardNew in the non-normalized case.
......@@ -131,7 +137,7 @@ public class MinWatchCard implements Propagatable, Constr, Undoable,
// On normalise la contrainte au sens de Barth
normalize();
this.maxUnsatisfied = lits.length - this.degree;
}
/**
......@@ -157,7 +163,7 @@ public class MinWatchCard implements Propagatable, Constr, Undoable,
// On copie les litt?raux de la contrainte
this.lits = new int[ps.size()];
ps.moveTo(this.lits);
this.maxUnsatisfied = lits.length - this.degree;
}
/**
......@@ -170,9 +176,13 @@ public class MinWatchCard implements Propagatable, Constr, Undoable,
* @see Constr#calcReason(int p, IVecInt outReason)
*/
public void calcReason(int p, IVecInt outReason) {
for (int lit : this.lits) {
if (this.voc.isFalsified(lit)) {
outReason.push(lit ^ 1);
int c = p == ILits.UNDEFINED ? -1 : 0;
for (int q : this.lits) {
if (this.voc.isFalsified(q)) {
outReason.push(q ^ 1);
if (++c >= this.maxUnsatisfied) {
return;
}
}
}
}
......@@ -241,8 +251,6 @@ public class MinWatchCard implements Propagatable, Constr, Undoable,
}
}
// DLB: inutile?
// ps.shrinkTo(nbElement);
assert modif <= 0;
return modif;
......
......@@ -33,6 +33,8 @@ import java.util.HashSet;
import java.util.Set;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
......@@ -47,22 +49,159 @@ import org.sat4j.specs.TimeoutException;
* @author leberre
*
*/
public class Backbone {
private Backbone() {
public final class Backbone {
interface Backboner {
IVecInt compute(ISolver solver, int[] implicant, IVecInt assumptions)
throws TimeoutException;
}
private static final Backboner BB = new Backboner() {
/**
* Computes the backbone of a formula following the iterative algorithm
* described in João Marques-Silva, Mikolás Janota, Inês Lynce: On
* Computing Backbones of Propositional Theories. ECAI 2010: 15-20 and
* using Sat4j specific prime implicant computation.
*
* @param solver
* @return
* @throws TimeoutException
*/
public IVecInt compute(ISolver solver, int[] implicant,
IVecInt assumptions) throws TimeoutException {
int nbSatTests = 0;
long timePI = 0L;
long begin;
Set<Integer> assumptionsSet = new HashSet<Integer>();
for (IteratorInt it = assumptions.iterator(); it.hasNext();) {
assumptionsSet.add(it.next());
}
IVecInt litsToTest = new VecInt();
for (int p : implicant) {
if (!assumptionsSet.contains(p)) {
litsToTest.push(-p);
}
}
int worstCase = litsToTest.size();
IVecInt candidates = new VecInt();
assumptions.copyTo(candidates);
int p;
IConstr constr;
while (!litsToTest.isEmpty()) {
p = litsToTest.last();
candidates.push(p);
litsToTest.pop();
if (solver.isSatisfiable(candidates)) {
candidates.pop();
begin = System.currentTimeMillis();
implicant = solver.primeImplicant();
timePI += (System.currentTimeMillis() - begin);
int oldsize = litsToTest.size();
removeVarNotPresentAndSatisfiedLits(implicant, litsToTest,
solver.nVars());
// System.err.println(litsToTest.size() - oldsize);
} else {
candidates.pop().push(-p);
}
nbSatTests++;
}
System.err.printf(
"vars %d constrs %d tests : %d/%d temps PI %d %n",
solver.nVars(), solver.nConstraints(), nbSatTests,
worstCase, timePI);
return candidates;
}
};
/**
* Computes the backbone of a formula following the algorithm described in
* João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of
* Propositional Theories. ECAI 2010: 15-20
* Computes the backbone of a formula using the iterative approach found in
* BB but testing a set of literals at once instead of only one. This
* approach outperforms BB in terms of SAT calls. Both approach are made
* available for testing purposes.
*
* @param solver
* @return
* @throws TimeoutException
*/
public static IVecInt compute(ISolver solver) throws TimeoutException {
private static final Backboner IBB = new Backboner() {
public IVecInt compute(ISolver solver, int[] implicant,
IVecInt assumptions) throws TimeoutException {
int nbSatTests = 0;
long timePI = 0L;
long begin;
Set<Integer> assumptionsSet = new HashSet<Integer>();
for (IteratorInt it = assumptions.iterator(); it.hasNext();) {
assumptionsSet.add(it.next());
}
IVecInt litsToTest = new VecInt();
for (int p : implicant) {
if (!assumptionsSet.contains(p)) {
litsToTest.push(-p);
}
}
int worstCase = litsToTest.size();
IVecInt candidates = new VecInt();
assumptions.copyTo(candidates);
int p;
IConstr constr;
while (!litsToTest.isEmpty()) {
try {
constr = solver.addClause(litsToTest);
if (solver.isSatisfiable(candidates)) {
begin = System.currentTimeMillis();
implicant = solver.primeImplicant();
timePI += (System.currentTimeMillis() - begin);
// int oldsize = litsToTest.size();
removeVarNotPresentAndSatisfiedLits(implicant,
litsToTest, solver.nVars());
// System.err.println(litsToTest.size() - oldsize);
solver.removeSubsumedConstr(constr);
} else {
for (IteratorInt it = litsToTest.iterator(); it
.hasNext();) {
candidates.push(-it.next());
}
solver.removeConstr(constr);
litsToTest.clear();
}
} catch (ContradictionException e) {
for (IteratorInt it = litsToTest.iterator(); it.hasNext();) {
candidates.push(-it.next());
}
litsToTest.clear();
}
nbSatTests++;
}
System.err.printf(
"vars %d constrs %d tests : %d/%d temps PI %d %n",
solver.nVars(), solver.nConstraints(), nbSatTests,
worstCase, timePI);
return candidates;
}
};
private final Backboner bb;
private final static Backbone instance = ibb();
private Backbone(Backboner bb) {
this.bb = bb;
}
public static Backbone instance() {
return instance;
}
public static Backbone bb() {
return new Backbone(BB);
}
public static Backbone ibb() {
return new Backbone(IBB);
}
public IVecInt compute(ISolver solver) throws TimeoutException {
return compute(solver, VecInt.EMPTY);
}
......@@ -77,7 +216,7 @@ public class Backbone {
* @return
* @throws TimeoutException
*/
public static IVecInt compute(ISolver solver, IVecInt assumptions)
public IVecInt compute(ISolver solver, IVecInt assumptions)
throws TimeoutException {
boolean result = solver.isSatisfiable(assumptions);
if (!result) {
......@@ -87,40 +226,14 @@ public class Backbone {
}
public static IVecInt compute(ISolver solver, int[] implicant)
public IVecInt compute(ISolver solver, int[] implicant)
throws TimeoutException {
return compute(solver, implicant, VecInt.EMPTY);
}
public static IVecInt compute(ISolver solver, int[] implicant,
IVecInt assumptions) throws TimeoutException {
Set<Integer> assumptionsSet = new HashSet<Integer>();
for (IteratorInt it = assumptions.iterator(); it.hasNext();) {
assumptionsSet.add(it.next());
}
IVecInt litsToTest = new VecInt();
for (int p : implicant) {
if (!assumptionsSet.contains(p)) {
litsToTest.push(-p);
}
}
IVecInt candidates = new VecInt();
assumptions.copyTo(candidates);
int p;
while (!litsToTest.isEmpty()) {
p = litsToTest.last();
candidates.push(p);
litsToTest.pop();
if (solver.isSatisfiable(candidates)) {
candidates.pop();
implicant = solver.primeImplicant();
removeVarNotPresentAndSatisfiedLits(implicant, litsToTest,
solver.nVars());
} else {
candidates.pop().push(-p);
}
}
return candidates;
public IVecInt compute(ISolver solver, int[] implicant, IVecInt assumptions)
throws TimeoutException {
return bb.compute(solver, implicant, assumptions);
}
private static void removeVarNotPresentAndSatisfiedLits(int[] implicant,
......
......@@ -59,7 +59,7 @@ public class BackboneTest {
clause.push(1);
solver.addClause(clause);
clause.clear();
IVecInt backbone = Backbone.compute(solver);
IVecInt backbone = Backbone.instance().compute(solver);
assertTrue(backbone.contains(1));
assertTrue(backbone.contains(-2));
assertTrue(backbone.contains(-3));
......@@ -79,7 +79,7 @@ public class BackboneTest {
clause.push(-1).push(-3);
solver.addClause(clause);
clause.clear();
IVecInt backbone = Backbone.compute(solver);
IVecInt backbone = Backbone.instance().compute(solver);
assertEquals(0, backbone.size());
}
......@@ -100,7 +100,7 @@ public class BackboneTest {
clause.push(-1).push(-2);
solver.addClause(clause);
clause.clear();
IVecInt backbone = Backbone.compute(solver);
IVecInt backbone = Backbone.instance().compute(solver);
assertEquals(0, backbone.size());
}
......@@ -142,17 +142,17 @@ public class BackboneTest {
solver3.addClause(new VecInt(is));
}
IVecInt vecInt1 = Backbone.compute(solver1);
IVecInt vecInt1 = Backbone.instance().compute(solver1);
assertEquals(vecInt1.size(), 2);
assertTrue(vecInt1.contains(1));
assertTrue(vecInt1.contains(2));
IVecInt vecInt2 = Backbone.compute(solver2);
IVecInt vecInt2 = Backbone.instance().compute(solver2);
assertEquals(vecInt2.size(), 2);
assertTrue(vecInt2.contains(1));
assertTrue(vecInt2.contains(2));
IVecInt vecInt3 = Backbone.compute(solver3);
IVecInt vecInt3 = Backbone.instance().compute(solver3);
assertEquals(vecInt3.size(), 2);
assertTrue(vecInt3.contains(1));
assertTrue(vecInt3.contains(3));
......
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