Commit f0d0fa44 authored by leberre's avatar leberre

Fixed several issues due to the decision base model enumeration.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2325 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 584b77cf
......@@ -668,7 +668,7 @@ public class MinWatchCard implements Propagatable, Constr, Undoable,
while ((this.lits[indFalsified] ^ 1) != p) {
indFalsified++;
}
assert this.watchCumul > this.degree;
assert this.watchCumul >= this.degree;
// Recherche du litt?ral swap
int indSwap = this.savedindex;
......
......@@ -224,8 +224,10 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
}
public boolean propagatePI(MandatoryLiteralListener l, int p) {
// TODO: implement this method !
throw new UnsupportedOperationException("Not implemented yet!");
for (int i = 0; i < clauses.size(); i++) {
l.isMandatory(clauses.get(i));
}
return true;
}
public Constr toConstraint() {
......
......@@ -50,6 +50,8 @@ public final class LearntWLClause extends WLClause {
* @see org.sat4j.minisat.constraints.cnf.WLClause#register()
*/
public void register() {
if (this.lits.length == 0)
return;
assert this.lits.length > 1;
// prendre un deuxieme litt???ral ??? surveiller
int maxi = 1;
......
......@@ -82,7 +82,6 @@ public class UnitClause implements Constr {
}
public void register() {
throw new UnsupportedOperationException();
}
public void remove(UnitPropagationListener upl) {
......
......@@ -1178,7 +1178,7 @@ public class Solver<D extends DataStructureFactory> implements ISolverService,
protected void cancelUntilTrailLevel(int level) {
while (!trail.isEmpty() && trail.size() > level) {
undoOne();
if (trailLim.last() == trail.size()) {
if (!trailLim.isEmpty() && trailLim.last() == trail.size()) {
trailLim.pop();
decisions.pop();
}
......@@ -2116,13 +2116,24 @@ public class Solver<D extends DataStructureFactory> implements ISolverService,
}
public IConstr discardCurrentModel() throws ContradictionException {
return addClause(createBlockingClauseForCurrentModel());
IVecInt blockingClause = createBlockingClauseForCurrentModel();
if (blockingClause.isEmpty()) {
throw new ContradictionException();
}
return addBlockingClause(blockingClause);
}
public IVecInt createBlockingClauseForCurrentModel() {
IVecInt clause = new VecInt(decisions.size());
for (int i = 0; i < decisions.size(); i++) {
clause.push(-decisions.get(i));
if (realNumberOfVariables() > nVars()) {
// we rely on the model projection in that case
for (int p : this.model) {
clause.push(-p);
}
} else {
for (int i = 0; i < decisions.size(); i++) {
clause.push(-decisions.get(i));
}
}
return clause;
}
......
......@@ -30,6 +30,8 @@
package org.sat4j.opt;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
......@@ -69,6 +71,11 @@ public abstract class AbstractSelectorVariablesDecorator extends
private boolean isSolutionOptimal;
/**
* @since 2.3.6
*/
private IVecInt prevBlockingClause;
public AbstractSelectorVariablesDecorator(ISolver solver) {
super(solver);
}
......@@ -100,6 +107,8 @@ public abstract class AbstractSelectorVariablesDecorator extends
}
this.prevfullmodel = super.modelWithInternalVariables();
this.prevmodel = super.model();
this.prevBlockingClause = super
.createBlockingClauseForCurrentModel();
calculateObjectiveValue();
} else {
this.isSolutionOptimal = true;
......@@ -119,6 +128,16 @@ public abstract class AbstractSelectorVariablesDecorator extends
return this.prevboolmodel[var - 1];
}
@Override
public IConstr discardCurrentModel() throws ContradictionException {
return addBlockingClause(this.prevBlockingClause);
}
@Override
public IVecInt createBlockingClauseForCurrentModel() {
return this.prevBlockingClause;
}
public boolean isOptimal() {
return this.isSolutionOptimal;
}
......
......@@ -31,9 +31,11 @@ package org.sat4j.tools;
import java.io.ObjectInputStream;
import java.io.PrintWriter;
import java.util.Collection;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IGroupSolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
......@@ -45,7 +47,8 @@ import org.sat4j.specs.IteratorInt;
* @author leberre
*
*/
public class DimacsOutputSolver extends AbstractOutputSolver {
public class DimacsOutputSolver extends AbstractOutputSolver implements
IGroupSolver {
/**
*
......@@ -214,4 +217,18 @@ public class DimacsOutputSolver extends AbstractOutputSolver {
throw new UnsupportedOperationException();
}
public IConstr addClause(IVecInt literals, int desc)
throws ContradictionException {
this.out.print(desc + "> ");
for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
this.out.print(iterator.next() + " ");
}
this.out.println("0");
return null;
}
public Collection<Integer> getAddedVars() {
throw new UnsupportedOperationException("Not implemented yet!");
}
}
......@@ -30,9 +30,11 @@
package org.sat4j.tools;
import java.io.PrintWriter;
import java.util.Collection;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IGroupSolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
......@@ -45,7 +47,8 @@ import org.sat4j.specs.IteratorInt;
* @author leberre
*
*/
public class DimacsStringSolver extends AbstractOutputSolver {
public class DimacsStringSolver extends AbstractOutputSolver implements
IGroupSolver {
/**
*
......@@ -241,4 +244,18 @@ public class DimacsStringSolver extends AbstractOutputSolver {
throw new UnsupportedOperationException();
}
public IConstr addClause(IVecInt literals, int desc)
throws ContradictionException {
this.out.append(desc + "> ");
for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
this.out.append(iterator.next() + " ");
}
this.out.append("0\n");
return null;
}
public Collection<Integer> getAddedVars() {
throw new UnsupportedOperationException("Not implemented yet!");
}
}
......@@ -44,7 +44,7 @@ public class TestGroupedTimeoutModelEnumeration {
private ISolver solver;
@Before
public void tearDDown() throws ContradictionException {
public void setUp() throws ContradictionException {
this.solver = new ModelIterator(SolverFactory.newDefault());
IVecInt clause = new VecInt();
for (int i = 1; i <= 1000; i++) {
......
......@@ -351,6 +351,6 @@ public class PseudoOptDecorator extends PBSolverDecorator implements
@Override
public IConstr discardCurrentModel() throws ContradictionException {
return addClause(prevModelBlockingClause);
return addBlockingClause(this.prevModelBlockingClause);
}
}
......@@ -317,26 +317,26 @@ public final class Solvers {
.forName("org.sat4j." + framework + ".SolverFactory"); //$NON-NLS-1$ //$NON-NLS-2$
Class<?>[] params = {};
Method m = clazz.getMethod("instance", params); //$NON-NLS-1$
factory = (ASolverFactory) m.invoke(null, (Object[]) null);
factory = (ASolverFactory<ISolver>) m.invoke(null, (Object[]) null);
} catch (Exception e) { // DLB Findbugs warning ok
logger.log("Wrong framework: " + framework
+ ". Using minisat instead.");
factory = org.sat4j.minisat.SolverFactory.instance();
}
ICDCL asolver;
ICDCL<?> asolver;
if (cmd.hasOption("s")) {
String solvername = cmd.getOptionValue("s");
if (solvername == null) {
logger.log("No solver for option s. Launching default solver.");
logger.log("Available solvers: "
+ Arrays.asList(factory.solverNames()));
asolver = (Solver) factory.defaultSolver();
asolver = (Solver<?>) factory.defaultSolver();
} else {
asolver = (Solver) factory.createSolverByName(solvername);
asolver = (Solver<?>) factory.createSolverByName(solvername);
}
} else {
asolver = (Solver) factory.defaultSolver();
asolver = (Solver<?>) factory.defaultSolver();
}
if (cmd.hasOption("S")) {
......
......@@ -222,6 +222,7 @@ The aim of the SAT4J library is to provide an efficient library of SAT solvers i
<version>2.7</version>
<configuration>
<source>1.5</source>
<!--
<doclet>org.umlgraph.doclet.UmlGraphDoc</doclet>
<docletArtifact>
<groupId>org.umlgraph</groupId>
......@@ -229,8 +230,8 @@ The aim of the SAT4J library is to provide an efficient library of SAT solvers i
<version>5.1</version>
</docletArtifact>
<additionalparam>
<!-- -operations -visibility -->
</additionalparam>
-->
<useStandardDocletOptions>true</useStandardDocletOptions>
</configuration>
<executions>
......
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