Commit 713a0843 authored by Romain Wallon's avatar Romain Wallon

Merge branch 'cdcl-strategies' of https://gitlab.ow2.org/sat4j/sat4j into cdcl-strategies

parents e72e8677 57ca63cf
Pipeline #8970 canceled with stages
in 10 minutes and 13 seconds
unitclauseprovider=A reference to an object providing unit clauses to the solver (used only in parallel SAT solving)
searchlistener=A listener to the major events in the search process.
learning=Learning policy
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
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,8 +31,9 @@ package org.sat4j;
import java.io.PrintWriter;
import org.sat4j.core.VecInt;
import org.sat4j.annotations.Feature;
import org.sat4j.reader.Reader;
import org.sat4j.specs.AssignmentOrigin;
import org.sat4j.specs.ILogAble;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
......@@ -46,11 +47,14 @@ import org.sat4j.tools.Backbone;
* @author leberre
*
*/
@Feature("solutionlistener")
final class DecisionMode implements ILauncherMode {
private ExitCode exitCode = ExitCode.UNKNOWN;
private int nbSolutionFound;
private PrintWriter out;
private long beginTime;
private Reader reader;
private ISolver solver;
public void displayResult(ISolver solver, IProblem problem, ILogAble logger,
PrintWriter out, Reader reader, long beginTime,
......@@ -96,21 +100,49 @@ final class DecisionMode implements ILauncherMode {
if (nbSolutionFound >= 1) {
logger.log("Found " + nbSolutionFound + " solution(s)");
} else {
out.print(SOLUTION_PREFIX);
reader.decode(model, out);
out.println();
printSolution(solver, out, reader, model);
}
}
logger.log("Total wall clock time (in seconds) : " + wallclocktime); //$NON-NLS-1$
}
}
private void printSolution(ISolver solver, PrintWriter out, Reader reader,
int[] model) {
out.print(SOLUTION_PREFIX);
if (System.getProperty("color") == null) {
reader.decode(model, out);
out.println();
} else {
int[] stats = new int[AssignmentOrigin.values().length];
AssignmentOrigin origin;
for (int p : model) {
origin = solver.getOriginInModel(p);
out.print(origin.getColor());
out.print(p);
out.print(AssignmentOrigin.BLANK);
out.print(" ");
stats[origin.ordinal()]++;
}
out.println("0");
out.print(solver.getLogPrefix());
for (AssignmentOrigin ao : AssignmentOrigin.values()) {
out.printf("%s%s%s: %d ", ao.getColor(), ao,
AssignmentOrigin.BLANK, stats[ao.ordinal()]);
}
out.println();
}
}
public void solve(IProblem problem, Reader reader, ILogAble logger,
PrintWriter out, long beginTime) {
this.exitCode = ExitCode.UNKNOWN;
this.out = out;
this.nbSolutionFound = 0;
this.beginTime = beginTime;
this.reader = reader;
this.solver = (ISolver) problem;
try {
if (problem.isSatisfiable()) {
if (this.exitCode == ExitCode.UNKNOWN) {
......@@ -140,8 +172,7 @@ final class DecisionMode implements ILauncherMode {
this.out.printf("c Found solution #%d (%.2f)s%n", nbSolutionFound,
(System.currentTimeMillis() - beginTime) / 1000.0);
if (System.getProperty("printallmodels") != null) {
this.out.println(SOLUTION_PREFIX
+ new VecInt(solution).toString().replace(",", " ") + " 0");
printSolution(solver, out, reader, solution);
}
}
......
......@@ -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;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
* Contributors:
* CRIL - initial API and implementation
*******************************************************************************/
package org.sat4j.annotations;
/**
* Architectural information about the design of Sat4j.
*
* @author leberre
* @since 2.3.6
*/
public @interface Feature {
String value();
String parent() default "user";
}
......@@ -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;
......
......@@ -29,9 +29,11 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.annotations.Feature;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
@Feature(value = "deletion", parent = "expert")
final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
private static final long serialVersionUID = 1L;
private final ConflictTimer timer;
......@@ -44,27 +46,27 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
}
public void reduce(IVec<Constr> learnedConstrs) {
solver.sortOnActivity();
learnedConstrs.sort(solver.getActivityComparator());
int i, j;
for (i = j = 0; i < solver.learnts.size() / 2; i++) {
Constr c = solver.learnts.get(i);
for (i = j = 0; i < learnedConstrs.size() / 2; i++) {
Constr c = learnedConstrs.get(i);
if (c.locked() || c.size() == 2) {
solver.learnts.set(j++, solver.learnts.get(i));
learnedConstrs.set(j++, learnedConstrs.get(i));
} else {
c.remove(solver);