Commit 167e15b8 authored by lonca's avatar lonca
Browse files

SAT solvers used for CSP computations are know able to tell if they are real...

SAT solvers used for CSP computations are know able to tell if they are real solvers or DIMACS/PB output solvers.
This behavior is needed since output solvers must specify the literals mappings, which might be hidden in a computation point of view due to its (possibly) huge size.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2540 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent d06ebaa2
......@@ -23,6 +23,7 @@ import java.util.Map;
import org.sat4j.AbstractLauncher;
import org.sat4j.ILauncherMode;
import org.sat4j.pb.tools.PBAdapter;
import org.sat4j.reader.ECSPFormat;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
......@@ -37,6 +38,8 @@ public class CSPLauncher extends AbstractLauncher {
*/
private static final long serialVersionUID = 1L;
private boolean shouldOnlyDisplayEncoding = false;
public CSPLauncher() {
bufferizeLog();
}
......@@ -48,13 +51,14 @@ public class CSPLauncher extends AbstractLauncher {
*/
@Override
protected ISolver configureSolver(String[] args) {
ISolver asolver;
ICspPBSatSolver asolver;
if (args.length == 2) {
asolver = SolverFactory.instance().createSolverByName(args[0]);
} else {
asolver = SolverFactory.newDefault();
asolver = new CspSatSolverDecorator(new PBAdapter(SolverFactory.newDefault()));
}
log(asolver.toString(COMMENT_PREFIX));
this.shouldOnlyDisplayEncoding = asolver.shouldOnlyDisplayEncoding();
return asolver;
}
......@@ -69,7 +73,7 @@ public class CSPLauncher extends AbstractLauncher {
protected Reader createReader(final ISolver aSolver,
final String problemname) {
ECSPFormat cspFormat = ECSPFormat.inferInstanceType(problemname);
this.out = cspFormat.decoratePrintWriter(this.out);
this.out = cspFormat.decoratePrintWriter(this.shouldOnlyDisplayEncoding, this.out);
flushLog();
Reader aReader = cspFormat.getReader(this, aSolver);
setLauncherMode(cspFormat.isOptimizationModeRequired() ? ILauncherMode.OPTIMIZATION : ILauncherMode.DECISION);
......@@ -88,6 +92,13 @@ public class CSPLauncher extends AbstractLauncher {
throws ParseFormatException, IOException, ContradictionException {
this.silent = true;
IProblem problem = super.readProblem(problemname);
if(this.shouldOnlyDisplayEncoding) {
displayEncoding();
}
return problem;
}
private void displayEncoding() {
if(this.reader.hasAMapping()) {
this.out.write("c CSP to SAT var mapping:");
Map<Integer, String> mapping = this.reader.getMapping();
......@@ -103,7 +114,6 @@ public class CSPLauncher extends AbstractLauncher {
}
this.out.write("\n");
}
return problem;
}
public static void main(String[] args) {
......
package org.sat4j.csp;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.math.BigInteger;
import java.util.Map;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.ISolverService;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.SearchListener;
import org.sat4j.specs.TimeoutException;
import org.sat4j.specs.UnitClauseProvider;
public class CspSatSolverDecorator implements ICspPBSatSolver {
private static final long serialVersionUID = 1L;
private IPBSolver solver;
private boolean shouldDisplayEncoding = false;
public CspSatSolverDecorator(IPBSolver solver) {
this.solver = solver;
}
public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
throws ContradictionException {
return solver.addPseudoBoolean(lits, coeffs, moreThan, d);
}
public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException {
return solver.addAtMost(literals, coeffs, degree);
}
public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
throws ContradictionException {
return solver.addAtMost(literals, coeffs, degree);
}
public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException {
return solver.addAtLeast(literals, coeffs, degree);
}
public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
throws ContradictionException {
return solver.addAtLeast(literals, coeffs, degree);
}
public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight) throws ContradictionException {
return solver.addExactly(literals, coeffs, weight);
}
public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
throws ContradictionException {
return solver.addExactly(literals, coeffs, weight);
}
public void setObjectiveFunction(ObjectiveFunction obj) {
solver.setObjectiveFunction(obj);
}
public ObjectiveFunction getObjectiveFunction() {
return solver.getObjectiveFunction();
}
public boolean model(int var) {
return solver.model(var);
}
public int[] model() {
return solver.model();
}
@SuppressWarnings("deprecation")
public int newVar() {
return solver.newVar();
}
public int[] primeImplicant() {
return solver.primeImplicant();
}
public int nextFreeVarId(boolean reserve) {
return solver.nextFreeVarId(reserve);
}
public boolean primeImplicant(int p) {
return solver.primeImplicant(p);
}
public boolean isSatisfiable() throws TimeoutException {
return solver.isSatisfiable();
}
public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout) throws TimeoutException {
return solver.isSatisfiable(assumps, globalTimeout);
}
public void registerLiteral(int p) {
solver.registerLiteral(p);
}
public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
return solver.isSatisfiable(globalTimeout);
}
public void setExpectedNumberOfClauses(int nb) {
solver.setExpectedNumberOfClauses(nb);
}
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
return solver.isSatisfiable(assumps);
}
public IConstr addClause(IVecInt literals) throws ContradictionException {
return solver.addClause(literals);
}
public int[] findModel() throws TimeoutException {
return solver.findModel();
}
public IConstr addBlockingClause(IVecInt literals) throws ContradictionException {
return solver.addBlockingClause(literals);
}
public int[] findModel(IVecInt assumps) throws TimeoutException {
return solver.findModel(assumps);
}
public IConstr discardCurrentModel() throws ContradictionException {
return solver.discardCurrentModel();
}
public IVecInt createBlockingClauseForCurrentModel() {
return solver.createBlockingClauseForCurrentModel();
}
public boolean removeConstr(IConstr c) {
return solver.removeConstr(c);
}
public int nConstraints() {
return solver.nConstraints();
}
public int newVar(int howmany) {
return solver.newVar(howmany);
}
public boolean removeSubsumedConstr(IConstr c) {
return solver.removeSubsumedConstr(c);
}
public int nVars() {
return solver.nVars();
}
@SuppressWarnings("deprecation")
public void printInfos(PrintWriter out, String prefix) {
solver.printInfos(out, prefix);
}
public void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException {
solver.addAllClauses(clauses);
}
public void printInfos(PrintWriter out) {
solver.printInfos(out);
}
public IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException {
return solver.addAtMost(literals, degree);
}
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException {
return solver.addAtLeast(literals, degree);
}
public IConstr addExactly(IVecInt literals, int n) throws ContradictionException {
return solver.addExactly(literals, n);
}
public IConstr addParity(IVecInt literals, boolean even) {
return solver.addParity(literals, even);
}
public IConstr addConstr(Constr constr) {
return solver.addConstr(constr);
}
public void setTimeout(int t) {
solver.setTimeout(t);
}
public void setTimeoutOnConflicts(int count) {
solver.setTimeoutOnConflicts(count);
}
public void setTimeoutMs(long t) {
solver.setTimeoutMs(t);
}
public int getTimeout() {
return solver.getTimeout();
}
public long getTimeoutMs() {
return solver.getTimeoutMs();
}
public void expireTimeout() {
solver.expireTimeout();
}
public void reset() {
solver.reset();
}
@SuppressWarnings("deprecation")
public void printStat(PrintStream out, String prefix) {
solver.printStat(out, prefix);
}
@SuppressWarnings("deprecation")
public void printStat(PrintWriter out, String prefix) {
solver.printStat(out, prefix);
}
public void printStat(PrintWriter out) {
solver.printStat(out);
}
public Map<String, Number> getStat() {
return solver.getStat();
}
public String toString(String prefix) {
return solver.toString(prefix);
}
public void clearLearntClauses() {
solver.clearLearntClauses();
}
public void setDBSimplificationAllowed(boolean status) {
solver.setDBSimplificationAllowed(status);
}
public boolean isDBSimplificationAllowed() {
return solver.isDBSimplificationAllowed();
}
public <S extends ISolverService> void setSearchListener(SearchListener<S> sl) {
solver.setSearchListener(sl);
}
public void setUnitClauseProvider(UnitClauseProvider ucp) {
solver.setUnitClauseProvider(ucp);
}
public <S extends ISolverService> SearchListener<S> getSearchListener() {
return solver.getSearchListener();
}
public boolean isVerbose() {
return solver.isVerbose();
}
public void setVerbose(boolean value) {
solver.setVerbose(value);
}
public void setLogPrefix(String prefix) {
solver.setLogPrefix(prefix);
}
public String getLogPrefix() {
return solver.getLogPrefix();
}
public IVecInt unsatExplanation() {
return solver.unsatExplanation();
}
public int[] modelWithInternalVariables() {
return solver.modelWithInternalVariables();
}
public int realNumberOfVariables() {
return solver.realNumberOfVariables();
}
public boolean isSolverKeptHot() {
return solver.isSolverKeptHot();
}
public void setKeepSolverHot(boolean keepHot) {
solver.setKeepSolverHot(keepHot);
}
public ISolver getSolvingEngine() {
return solver.getSolvingEngine();
}
@Override
public boolean shouldOnlyDisplayEncoding() {
return this.shouldDisplayEncoding;
}
@Override
public void setShouldOnlyDisplayEncoding(boolean b) {
this.shouldDisplayEncoding = b;
}
}
package org.sat4j.csp;
import org.sat4j.pb.IPBSolver;
public interface ICspPBSatSolver extends IPBSolver {
boolean shouldOnlyDisplayEncoding();
void setShouldOnlyDisplayEncoding(boolean b);
}
......@@ -18,6 +18,9 @@
*******************************************************************************/
package org.sat4j.csp;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.constraints.MixedDataStructureDanielWL;
import org.sat4j.minisat.core.DataStructureFactory;
......@@ -26,10 +29,8 @@ import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.tools.PBAdapter;
import org.sat4j.specs.ISolver;
import org.sat4j.tools.DimacsOutputSolver;
import org.sat4j.tools.DimacsStringSolver;
/**
......@@ -74,7 +75,19 @@ public class SolverFactory extends ASolverFactory<ISolver> {
return instance;
}
/**
public ICspPBSatSolver createSolverByName(String solvername) {
try {
Class<?>[] paramtypes = {};
Method m = this.getClass()
.getMethod("new" + solvername, paramtypes); //$NON-NLS-1$
return (ICspPBSatSolver) m.invoke(null, (Object[]) null);
} catch (SecurityException | NoSuchMethodException | IllegalAccessException | IllegalArgumentException | InvocationTargetException e) {
System.err.println(e.getLocalizedMessage());
}
return null;
}
/**
* @param dsf
* the data structure used for representing clauses and lits
* @return MiniSAT the data structure dsf.
......@@ -106,16 +119,16 @@ public class SolverFactory extends ASolverFactory<ISolver> {
return newSAT();
}
public static ISolver newSAT() {
return org.sat4j.pb.SolverFactory.newSAT();
public static ICspPBSatSolver newSAT() {
return new CspSatSolverDecorator(org.sat4j.pb.SolverFactory.newSAT());
}
public static ISolver newUNSAT() {
return org.sat4j.pb.SolverFactory.newUNSAT();
public static ICspPBSatSolver newUNSAT() {
return new CspSatSolverDecorator(org.sat4j.pb.SolverFactory.newUNSAT());
}
public static ISolver newCuttingPlanes() {
return org.sat4j.pb.SolverFactory.newCuttingPlanes();
public static ICspPBSatSolver newCuttingPlanes() {
return new CspSatSolverDecorator(org.sat4j.pb.SolverFactory.newCuttingPlanes());
}
@Override
......@@ -130,21 +143,19 @@ public class SolverFactory extends ASolverFactory<ISolver> {
* @see #lightSolver() the same method, polymorphic, to be called from an
* instance of ASolverFactory.
*/
public static ISolver newLight() {
return newMiniSAT(new MixedDataStructureDanielWL());
public static ICspPBSatSolver newLight() {
return new CspSatSolverDecorator(new PBAdapter(newMiniSAT(new MixedDataStructureDanielWL())));
}
@Override
public ISolver lightSolver() {
public ICspPBSatSolver lightSolver() {
return newLight();
}
public static ISolver newDimacsOutput() {
return new DimacsOutputSolver();
}
public static IPBSolver newDimacsOutputPB() {
return new PBAdapter(new DimacsStringSolver());
public static ICspPBSatSolver newDimacsOutputPB() {
final CspSatSolverDecorator solver = new CspSatSolverDecorator(new PBAdapter(new DimacsStringSolver()));
solver.setShouldOnlyDisplayEncoding(true);
return solver;
}
}
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