Commit db543e5a authored by leberre's avatar leberre
Browse files

It is now possible to compute min4cardinality MUSes using AllMUSes class. Need some testing.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1683 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent f6426f27
package org.sat4j.tools;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
public class AbstractMinimalModel extends SolverDecorator<ISolver> {
/**
*
*/
private static final long serialVersionUID = 1L;
protected final IVecInt pLiterals;
protected final SolutionFoundListener modelListener;
public static IVecInt positiveLiterals(ISolver solver) {
IVecInt literals = new VecInt(solver.nVars());
for (int i = 1; i <= solver.nVars(); i++) {
literals.push(i);
}
return literals;
}
public static IVecInt negativeLiterals(ISolver solver) {
IVecInt literals = new VecInt(solver.nVars());
for (int i = 1; i <= solver.nVars(); i++) {
literals.push(-i);
}
return literals;
}
public AbstractMinimalModel(ISolver solver) {
this(solver, SolutionFoundListener.VOID);
}
public AbstractMinimalModel(ISolver solver, IVecInt p) {
this(solver, p, SolutionFoundListener.VOID);
}
public AbstractMinimalModel(ISolver solver,
SolutionFoundListener modelListener) {
this(solver, negativeLiterals(solver), modelListener);
}
public AbstractMinimalModel(ISolver solver, IVecInt p,
SolutionFoundListener modelListener) {
super(solver);
this.pLiterals = new VecInt(p.size());
p.copyTo(this.pLiterals);
this.modelListener = modelListener;
}
}
......@@ -95,23 +95,48 @@ public class AllMUSes {
if (secondPhaseClauses.isEmpty()) {
computeAllMSS();
}
ISolver solver = SolverFactory.newDefault();
for (IVecInt v : secondPhaseClauses) {
try {
solver.addClause(v);
} catch (ContradictionException e) {
return musList;
}
}
AbstractMinimalModel minSolver = new Minimal4InclusionModel(solver,
Minimal4InclusionModel.positiveLiterals(solver));
return computeAllMUSes(listener, minSolver);
}
public List<IVecInt> computeAllMUSesOrdered(SolutionFoundListener listener) {
if (secondPhaseClauses.isEmpty()) {
computeAllMSS();
}
ISolver solver = SolverFactory.newDefault();
for (IVecInt v : secondPhaseClauses) {
try {
solver.addClause(v);
} catch (ContradictionException e) {
return musList;
}
}
AbstractMinimalModel minSolver = new Minimal4CardinalityModel(solver,
Minimal4InclusionModel.positiveLiterals(solver));
return computeAllMUSes(listener, minSolver);
}
private List<IVecInt> computeAllMUSes(SolutionFoundListener listener,
ISolver minSolver) {
if (css.isVerbose()) {
System.out.println(css.getLogPrefix() + "Computing all MUSes ...");
}
css.internalState();
ISolver solver = SolverFactory.newDefault();
IVecInt mus;
IVecInt blockingClause;
try {
for (IVecInt v : secondPhaseClauses) {
solver.addClause(v);
}
Minimal4InclusionModel minSolver = new Minimal4InclusionModel(
solver, Minimal4InclusionModel.positiveLiterals(solver));
while (minSolver.isSatisfiable()) {
blockingClause = new VecInt();
......@@ -148,8 +173,16 @@ public class AllMUSes {
}
public List<IVecInt> computeAllMSS(SolutionFoundListener listener) {
css.internalState();
int nVar = css.nVars();
IVecInt pLits = new VecInt();
for (Integer i : css.getAddedVars()) {
pLits.push(i);
}
AbstractMinimalModel min4Inc = new Minimal4InclusionModel(css, pLits);
return computeAllMSS(listener, min4Inc, pLits);
}
public List<IVecInt> computeAllMSSOrdered(SolutionFoundListener listener) {
if (css.isVerbose()) {
System.out.println(css.getLogPrefix() + "Computing all MSSes ...");
}
......@@ -158,7 +191,14 @@ public class AllMUSes {
pLits.push(i);
}
Minimal4InclusionModel min4Inc = new Minimal4InclusionModel(css, pLits);
AbstractMinimalModel min4Inc = new Minimal4CardinalityModel(css, pLits);
return computeAllMSS(listener, min4Inc, pLits);
}
private List<IVecInt> computeAllMSS(SolutionFoundListener listener,
ISolver min4Inc, IVecInt pLits) {
css.internalState();
int nVar = css.nVars();
IVecInt blockingClause;
......
......@@ -31,6 +31,7 @@ package org.sat4j.tools;
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.TimeoutException;
......@@ -44,10 +45,12 @@ import org.sat4j.specs.TimeoutException;
* @author leberre
* @see org.sat4j.specs.ISolver#addAtMost(IVecInt, int)
*/
public class Minimal4CardinalityModel extends SolverDecorator<ISolver> {
public class Minimal4CardinalityModel extends AbstractMinimalModel {
private static final long serialVersionUID = 1L;
private int[] prevfullmodel;
/**
* @param solver
*/
......@@ -55,6 +58,20 @@ public class Minimal4CardinalityModel extends SolverDecorator<ISolver> {
super(solver);
}
public Minimal4CardinalityModel(ISolver solver, IVecInt p,
SolutionFoundListener modelListener) {
super(solver, p, modelListener);
}
public Minimal4CardinalityModel(ISolver solver, IVecInt p) {
super(solver, p);
}
public Minimal4CardinalityModel(ISolver solver,
SolutionFoundListener modelListener) {
super(solver, modelListener);
}
/*
* (non-Javadoc)
*
......@@ -64,27 +81,33 @@ public class Minimal4CardinalityModel extends SolverDecorator<ISolver> {
public int[] model() {
int[] prevmodel = null;
IVecInt vec = new VecInt();
IConstr lastOne = null;
try {
do {
prevfullmodel = super.modelWithInternalVariables();
prevmodel = super.model();
vec.clear();
for (int i = 1; i <= nVars(); i++) {
vec.push(-i);
}
int counter = 0;
for (int q : prevmodel) {
if (q < 0) {
for (int q : prevfullmodel) {
if (pLiterals.contains(q)) {
counter++;
}
}
addAtMost(vec, counter - 1);
lastOne = addAtMost(pLiterals, counter - 1);
} while (isSatisfiable());
} catch (TimeoutException e) {
throw new IllegalStateException("Solver timed out"); //$NON-NLS-1$
} catch (ContradictionException e) {
// added trivial unsat clauses
}
// restore();
if (lastOne != null) {
removeConstr(lastOne);
}
return prevmodel;
}
@Override
public int[] modelWithInternalVariables() {
model();
return prevfullmodel;
}
}
......@@ -49,16 +49,12 @@ import org.sat4j.specs.TimeoutException;
*
* @see org.sat4j.specs.ISolver#addClause(IVecInt)
*/
public class Minimal4InclusionModel extends SolverDecorator<ISolver> {
public class Minimal4InclusionModel extends AbstractMinimalModel {
private static final long serialVersionUID = 1L;
private final IVecInt pLiterals;
private int[] prevfullmodel;
private final SolutionFoundListener modelListener;
/**
*
* @param solver
......@@ -70,10 +66,7 @@ public class Minimal4InclusionModel extends SolverDecorator<ISolver> {
*/
public Minimal4InclusionModel(ISolver solver, IVecInt p,
SolutionFoundListener modelListener) {
super(solver);
this.pLiterals = new VecInt(p.size());
p.copyTo(this.pLiterals);
this.modelListener = modelListener;
super(solver,p,modelListener);
}
/**
......@@ -94,22 +87,6 @@ public class Minimal4InclusionModel extends SolverDecorator<ISolver> {
this(solver, negativeLiterals(solver), SolutionFoundListener.VOID);
}
public static IVecInt positiveLiterals(ISolver solver) {
IVecInt literals = new VecInt(solver.nVars());
for (int i = 1; i <= solver.nVars(); i++) {
literals.push(i);
}
return literals;
}
public static IVecInt negativeLiterals(ISolver solver) {
IVecInt literals = new VecInt(solver.nVars());
for (int i = 1; i <= solver.nVars(); i++) {
literals.push(-i);
}
return literals;
}
/*
* (non-Javadoc)
*
......
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