Commit 9f33062a authored by Romain Wallon's avatar Romain Wallon

Merge branch 'master' into cdcl-strategies

parents 81fa78b9 22374e5e
Pipeline #8892 failed with stages
in 1 minute and 39 seconds
......@@ -5,4 +5,7 @@ restarts=Search restarts policy
simplifications=Learned constraints simplification policy
deletion=Learned constraints deletion policy
varheuristics=Variable selection heuristics
phaseheuristics=Phase selection policy for a given variable
\ No newline at end of file
phaseheuristics=Phase selection policy for a given variable
reader=Reader responsible for feeding the solver
solver=The complexity hierarchy of solvers in Sat4j
solutionlistener=A listener called when a model is found by the solver
\ No newline at end of file
......@@ -39,6 +39,9 @@ import java.net.URL;
import java.util.Properties;
import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.core.ICDCL;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.orders.OrientedOrder;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
......@@ -213,6 +216,17 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
+ "Generating unsat proof in file " + proofFile);
}
}
if (System.getProperty("forceorder") != null) {
String orderFile = problemname + ".order";
ICDCL solverService = (ICDCL) solver;
IOrder order = new OrientedOrder(orderFile,
solverService.getOrder());
solverService.setOrder(order);
if (!this.isSilent()) {
System.out.println(this.solver.getLogPrefix()
+ "Forcing heuristics using file " + orderFile);
}
}
if (feedWithDecorated) {
return decorator;
}
......
......@@ -31,6 +31,7 @@ package org.sat4j;
import java.io.PrintWriter;
import org.sat4j.annotations.Feature;
import org.sat4j.reader.Reader;
import org.sat4j.specs.AssignmentOrigin;
import org.sat4j.specs.ILogAble;
......@@ -46,6 +47,7 @@ import org.sat4j.tools.Backbone;
* @author leberre
*
*/
@Feature("solutionlistener")
final class DecisionMode implements ILauncherMode {
private ExitCode exitCode = ExitCode.UNKNOWN;
private int nbSolutionFound;
......
......@@ -31,6 +31,7 @@ package org.sat4j;
import java.io.PrintWriter;
import org.sat4j.annotations.Feature;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.reader.Reader;
......@@ -50,6 +51,7 @@ import org.sat4j.tools.LexicoDecorator;
* @author leberre
*
*/
@Feature("solutionlistener")
final class OptimizationMode implements ILauncherMode {
private int nbSolutions;
private ExitCode exitCode = ExitCode.UNKNOWN;
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.core;
import org.sat4j.annotations.Feature;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
......@@ -42,6 +43,7 @@ import org.sat4j.specs.VarMapper;
* @since 2.0
*
*/
@Feature("constraint")
public class ConstrGroup implements IConstr {
private final IVec<IConstr> constrs = new Vec<IConstr>();
......
......@@ -33,6 +33,7 @@ import java.io.Serializable;
import java.util.HashSet;
import java.util.Set;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.Lits;
......@@ -52,6 +53,7 @@ import org.sat4j.specs.VarMapper;
/**
* @author leberre Contrainte de cardinalit?
*/
@Feature("constraint")
public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
private static final long serialVersionUID = 1L;
......
......@@ -34,6 +34,7 @@ import java.math.BigInteger;
import java.util.HashSet;
import java.util.Set;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.UnitClauses;
......@@ -47,6 +48,7 @@ import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
import org.sat4j.specs.VarMapper;
@Feature("constraint")
public final class MaxWatchCard
implements Propagatable, Constr, Undoable, Serializable {
......
......@@ -33,6 +33,7 @@ import java.io.Serializable;
import java.util.HashSet;
import java.util.Set;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.UnitClauses;
......@@ -46,6 +47,7 @@ import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
import org.sat4j.specs.VarMapper;
@Feature("constraint")
public class MinWatchCard
implements Propagatable, Constr, Undoable, Serializable {
......
......@@ -34,6 +34,7 @@ import static org.sat4j.core.LiteralsUtils.var;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
......@@ -49,6 +50,7 @@ import org.sat4j.specs.VarMapper;
* @author leberre
* @since 2.1
*/
@Feature("constraint")
public abstract class BinaryClause
implements Propagatable, Constr, Serializable {
......
......@@ -29,6 +29,7 @@ package org.sat4j.minisat.constraints.cnf;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
......@@ -43,6 +44,7 @@ import org.sat4j.specs.VarMapper;
*
* @author leberre
*/
@Feature("constraint")
public class BinaryClauses implements Constr, Propagatable, Serializable {
private static final long serialVersionUID = 1L;
......
......@@ -29,6 +29,7 @@ package org.sat4j.minisat.constraints.cnf;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Undoable;
......@@ -42,6 +43,7 @@ import org.sat4j.specs.VarMapper;
/**
* @author leberre
*/
@Feature("constraint")
public class CBClause implements Constr, Undoable, Propagatable, Serializable {
private static final long serialVersionUID = 1L;
......
......@@ -34,6 +34,7 @@ import static org.sat4j.core.LiteralsUtils.var;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
......@@ -56,6 +57,7 @@ import org.sat4j.specs.VarMapper;
* @see UnitClause
* @since 2.1
*/
@Feature("constraint")
public abstract class HTClause implements Propagatable, Constr, Serializable {
private static final long serialVersionUID = 1L;
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.annotations.Feature;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
......@@ -37,11 +38,12 @@ import org.sat4j.specs.IVecInt;
* @author daniel
* @since 2.1
*/
@Feature("constraint")
public class LearntBinaryClause extends BinaryClause {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
public LearntBinaryClause(IVecInt ps, ILits voc) {
......
......@@ -31,6 +31,7 @@ package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.core.LiteralsUtils.neg;
import org.sat4j.annotations.Feature;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
......@@ -39,6 +40,7 @@ import org.sat4j.specs.MandatoryLiteralListener;
* @author daniel
* @since 2.1
*/
@Feature("constraint")
public class LearntHTClause extends HTClause {
public LearntHTClause(IVecInt ps, ILits voc) {
......
......@@ -29,10 +29,12 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.annotations.Feature;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
@Feature("constraint")
public final class LearntWLClause extends WLClause {
public LearntWLClause(IVecInt ps, ILits voc) {
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.annotations.Feature;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.UnitPropagationListener;
......@@ -36,11 +37,12 @@ import org.sat4j.specs.UnitPropagationListener;
/**
* @since 2.1
*/
@Feature("constraint")
public class OriginalBinaryClause extends BinaryClause {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
public OriginalBinaryClause(IVecInt ps, ILits voc) {
......@@ -67,8 +69,8 @@ public class OriginalBinaryClause extends BinaryClause {
* @return the created clause or null if the clause should be ignored
* (tautology for example)
*/
public static OriginalBinaryClause brandNewClause(
UnitPropagationListener s, ILits voc, IVecInt literals) {
public static OriginalBinaryClause brandNewClause(UnitPropagationListener s,
ILits voc, IVecInt literals) {
OriginalBinaryClause c = new OriginalBinaryClause(literals, voc);
c.register();
return c;
......
......@@ -31,6 +31,7 @@ package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.core.LiteralsUtils.neg;
import org.sat4j.annotations.Feature;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
......@@ -39,6 +40,7 @@ import org.sat4j.specs.UnitPropagationListener;
/**
* @since 2.1
*/
@Feature("constraint")
public class OriginalHTClause extends HTClause {
public OriginalHTClause(IVecInt ps, ILits voc) {
......
......@@ -29,11 +29,13 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.annotations.Feature;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.UnitPropagationListener;
@Feature("constraint")
public final class OriginalWLClause extends WLClause {
public OriginalWLClause(IVecInt ps, ILits voc) {
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
......@@ -42,6 +43,7 @@ import org.sat4j.specs.VarMapper;
* @author daniel
* @since 2.1
*/
@Feature("constraint")
public class UnitClause implements Constr {
protected final int literal;
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.annotations.Feature;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
......@@ -38,6 +39,7 @@ import org.sat4j.specs.VarMapper;
/**
* @since 2.1
*/
@Feature("constraint")
public class UnitClauses implements Constr {
protected final int[] literals;
......
......@@ -33,6 +33,7 @@ import static org.sat4j.core.LiteralsUtils.var;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
......@@ -46,6 +47,7 @@ import org.sat4j.specs.VarMapper;
*
* @author leberre
*/
@Feature("constraint")
public abstract class WLClause implements Propagatable, Constr, Serializable {
private static final long serialVersionUID = 1L;
......
package org.sat4j.minisat.constraints.xor;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
......@@ -34,6 +35,7 @@ import org.sat4j.specs.VarMapper;
* @author leberre
* @since 2.3.6
*/
@Feature("constraint")
public class Xor implements Constr, Propagatable {
private final int[] lits;
......
......@@ -47,6 +47,7 @@ import java.util.Map;
import java.util.Set;
import java.util.Timer;
import java.util.TimerTask;
import java.util.TreeSet;
import java.util.logging.Level;
import java.util.logging.Logger;
......@@ -1407,6 +1408,7 @@ public class Solver<D extends DataStructureFactory>
if (classifyLiterals) {
StringBuffer stb = new StringBuffer(getLogPrefix());
int q;
String str;
for (int i = 0; i < trailLim.size(); i++) {
q = trail.get(trailLim.get(i));
stb.append(LiteralsUtils.toDimacs(q));
......@@ -1422,19 +1424,19 @@ public class Solver<D extends DataStructureFactory>
} else {
origin = AssignmentOrigin.DECIDED_PROPAGATED;
}
int max = 0;
int r;
TreeSet<Integer> levels = new TreeSet<>();
for (int j = 0; j < reason.size(); j++) {
r = reason.get(j);
if (r != q) {
max = Math.max(max, this.voc.getLevel(r));
levels.add(this.voc.getLevel(r));
}
}
stb.append(":");
stb.append(max);
if (voc.getLevel(q) == max) {
str = levels.toString().replaceAll(" ", "");
stb.append(str.substring(1, str.length() - 1));
if (voc.getLevel(q) == levels.last()) {
origin = AssignmentOrigin.DECIDED_CYCLE;
}
} else {
......
package org.sat4j.minisat.orders;
import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.PrintWriter;
import java.util.Scanner;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.IPhaseSelectionStrategy;
import org.sat4j.specs.IVecInt;
/**
* Forces the order of the heuristics for some literals. Then hand back to a
* dynamic heuristics.
*
* @author leberre
*
*/
@Feature(value = "varheuristics", parent = "expert")
public class OrientedOrder implements IOrder {
private final IVecInt orderedLits = new VecInt();
private boolean[] managed;
private ILits voc;
private final String fileName;
private final IOrder order;
public OrientedOrder(String fileName, IOrder order) {
this.fileName = fileName;
this.order = order;
}
@Override
public void setLits(ILits lits) {
order.setLits(lits);
voc = lits;
}
@Override
public int select() {
int p;
for (int i = 0; i < orderedLits.size(); i++) {
p = orderedLits.get(i);
if (voc.isUnassigned(p)) {
return p;
}
}
return order.select();
}
@Override
public void undo(int x) {
if (!managed[x >> 1]) {
order.undo(x);
}
}
@Override
public void updateVar(int p) {
if (!managed[p >> 1]) {
order.updateVar(p);
}
}
@Override
public void init() {
order.init();
managed = new boolean[voc.nVars() + 1];
try (Scanner in = new Scanner(
new BufferedReader(new FileReader(fileName)))) {
while (in.hasNext()) {
append(in.nextInt());
}
} catch (FileNotFoundException e) {
throw new IllegalStateException(e);
}
}
private void append(int l) {
int p = LiteralsUtils.toInternal(l);
orderedLits.push(p);
managed[p >> 1] = true;
}
@Override
public void printStat(PrintWriter out, String prefix) {
order.printStat(out, prefix);
}
@Override
public void setVarDecay(double d) {
order.setVarDecay(d);
}
@Override
public void varDecayActivity() {
order.varDecayActivity();
}
@Override
public double varActivity(int p) {
return order.varActivity(p);
}
@Override
public void assignLiteral(int p) {
if (!managed[p >> 1]) {
order.assignLiteral(p);
}
}
@Override
public void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy) {
order.setPhaseSelectionStrategy(strategy);
}
@Override
public IPhaseSelectionStrategy getPhaseSelectionStrategy() {
return order.getPhaseSelectionStrategy();
}
@Override
public void updateVarAtDecisionLevel(int q) {
if (!managed[q >> 1]) {
order.updateVarAtDecisionLevel(q);
}
}
@Override
public double[] getVariableHeuristics() {
return order.getVariableHeuristics();
}