Commit 3610d72b authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Merge branch 'VERIPB2' into 'master'

Add support for veripb in CP based solvers

See merge request !9
parents 0e8589ac d3266770
Pipeline #15943 passed with stages
in 38 minutes and 24 seconds
......@@ -25,7 +25,7 @@ maven38-java11:
except:
- master
script:
- mvn $MAVEN_CLI_OPTS clean org.jacoco:jacoco-maven-plugin:prepare-agent --settings settings.xml deploy
- mvn $MAVEN_CLI_OPTS clean package -Dmaven.javadoc.skip=true -Djacoco.skip=true
cache:
paths:
- .m2/repository
......
......@@ -497,8 +497,8 @@ public class Solver<D extends DataStructureFactory>
public IConstr addExactly(IVecInt literals, int n)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
group.add(addAtMost(literals, n));
group.add(addAtLeast(literals, n));
group.add(addAtMost(literals, n));
return group;
}
......
/*******************************************************************************
* 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.minisat.orders;
import static org.sat4j.core.LiteralsUtils.negLit;
import static org.sat4j.core.LiteralsUtils.var;
import org.sat4j.core.LiteralsUtils;
/**
* Keeps track of the phase of the latest assignment during search, while
* preserving the one of the latest solution found (typically for optimization).
*
* (implemented after seeing a talk at PoS 18 :
* https://easychair.org/smart-program/FLoC2018/POS-2018-07-07.html#talk:72764)
*
* @author leberre
*
*/
public final class SolutionPhaseSelectionStrategy
extends AbstractPhaserecordingSelectionStrategy {
/**
*
*/
private static final long serialVersionUID = 1L;
@Override
public void init(int nlength) {
if (this.phase == null || this.phase.length < nlength) {
this.phase = new int[nlength];
for (int i = 1; i < nlength; i++) {
this.phase[i] = negLit(i);
}
}
}
public void assignLiteral(int p) {
this.phase[var(p)] = p;
}
@Override
public String toString() {
return "lightweight component caching from RSAT plus solution phase";
}
public void updateVar(int p) {
}
public void updateVarAtDecisionLevel(int p) {
}
public void onModelFound(int[] model) {
for (int l : model) {
this.phase[Math.abs(l)] = LiteralsUtils.toInternal(l);
}
}
}
......@@ -106,4 +106,28 @@ public interface IConstr {
* rebuilding it.
*/
String dump();
/**
* Get a unique id for this constraint.
*
* @return a unique integral id for the constraint.
* @throws UnsupportedOperationException
* if no such identifier is available
* @since 3.0
*/
default int getId() {
throw new UnsupportedOperationException();
}
/**
* Allow the user to give a specific id to the constraint.
*
* The constraint may ignore it.
*
* @param nbConstraintsRead
* @since 3.0
*/
default void setId(int nbConstraintsRead) {
// do nothing
}
}
......@@ -191,7 +191,13 @@ public class DotSearchTracing<T> extends SearchListenerAdapter<ISolverService>
@Override
public final void learn(final IConstr constr) {
String learned = this.currentNodeName + "_learned";
saveLine(lineTab("\"" + learned + "\" [label=\"" + constr.toString(this)
String text;
if (constr == null) {
text = "0 >= 1";
} else {
text = constr.toString(this);
}
saveLine(lineTab("\"" + learned + "\" [label=\"" + text
+ "\", shape=box, color=\"orange\", style=dotted]"));
saveLine("\"" + learned + "\"" + "--" + "\"" + this.currentNodeName
+ "\"" + "[label=\"\", color=orange, style=dotted]");
......
package org.sat4j.tools;
import java.io.PrintWriter;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
/**
* Decorator design pattern for the IProblem interface.
*
* @author leberre
*
* @param <T>
* @since 2.3.6
*/
public class ProblemDecorator<T extends IProblem> implements IProblem {
private final T decorated;
public ProblemDecorator(T decorated) {
this.decorated = decorated;
}
@Override
public boolean model(int var) {
return decorated.model(var);
}
@Override
public int[] model() {
return decorated.model();
}
@Override
public int[] primeImplicant() {
return decorated.primeImplicant();
}
@Override
public boolean primeImplicant(int p) {
return decorated.primeImplicant(p);
}
@Override
public boolean isSatisfiable() throws TimeoutException {
return decorated.isSatisfiable();
}
@Override
public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
throws TimeoutException {
return decorated.isSatisfiable(assumps, globalTimeout);
}
@Override
public boolean isSatisfiable(boolean globalTimeout)
throws TimeoutException {
return decorated.isSatisfiable(globalTimeout);
}
@Override
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
return decorated.isSatisfiable(assumps);
}
@Override
public int[] findModel() throws TimeoutException {
return decorated.findModel();
}
@Override
public int[] findModel(IVecInt assumps) throws TimeoutException {
return decorated.findModel(assumps);
}
@Override
public int nConstraints() {
return decorated.nConstraints();
}
@Override
public int newVar(int howmany) {
return decorated.newVar(howmany);
}
@Override
public int nVars() {
return decorated.nVars();
}
@Override
public void printInfos(PrintWriter out, String prefix) {
decorated.printInfos(out, prefix);
}
@Override
public void printInfos(PrintWriter out) {
decorated.printInfos(out);
}
public T decorated() {
return decorated;
}
@Override
public int[] decisions() {
return decorated.decisions();
}
}
package org.sat4j.minisat.constraints;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertFalse;
import static org.junit.Assert.assertTrue;
import org.junit.Test;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.ModelIterator;
public class TestParityConstraint {
@Test
public void testParityTwo() throws TimeoutException {
ISolver solver = SolverFactory.newDefault();
solver.newVar(2);
solver.addParity(VecInt.of(1, 2), true);
assertTrue(solver.isSatisfiable());
ModelIterator iterator = new ModelIterator(solver);
assertTrue(iterator.isSatisfiable());
iterator.model();
assertTrue(iterator.isSatisfiable());
iterator.model();
assertFalse(iterator.isSatisfiable());
}
@Test
public void testParityThree() throws TimeoutException {
ISolver solver = SolverFactory.newDefault();
solver.newVar(3);
solver.addParity(VecInt.of(1, 2, 3), false);
assertTrue(solver.isSatisfiable());
ModelIterator iterator = new ModelIterator(solver);
while (iterator.isSatisfiable()) {
iterator.model();
}
assertEquals(4, iterator.numberOfModelsFoundSoFar());
}
@Test
public void testParityThreeUnsat() throws TimeoutException {
ISolver solver = SolverFactory.newDefault();
solver.newVar(3);
solver.addParity(VecInt.of(1, 2, 3), false);
solver.addParity(VecInt.of(1, 2, 3), true);
assertFalse(solver.isSatisfiable());
}
}
......@@ -34,9 +34,12 @@ import org.sat4j.DecisionMode;
import org.sat4j.core.ASolverFactory;
import org.sat4j.pb.reader.OPBReader2012;
import org.sat4j.pb.tools.OptimalModelIterator;
import org.sat4j.pb.tools.PBSearchListener;
import org.sat4j.pb.tools.VERIPBSearchListener;
import org.sat4j.reader.DimacsReader;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.ISolverService;
/**
* Launcher for the Pseudo Boolean 2007 competition.
......@@ -61,6 +64,13 @@ public class LanceurPseudo2007 extends LanceurPseudo2005 {
@Override
protected Reader createReader(ISolver theSolver, String problemname) {
String veripb = System.getProperty("veripb");
if (veripb != null) {
PBSearchListener<ISolverService> listener = new VERIPBSearchListener(
problemname);
this.solver.setSearchListener(listener);
log("using VERIPB proof format");
}
if (problemname.endsWith(".cnf"))
return new DimacsReader(theSolver);
return new OPBReader2012(handle);
......
......@@ -39,6 +39,8 @@ import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.learning.NoLearningButHeuristics;
import org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy;
import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy;
import org.sat4j.minisat.orders.RandomLiteralSelectionStrategy;
import org.sat4j.minisat.orders.RandomWalkDecorator;
import org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.ArminRestarts;
......@@ -1207,6 +1209,15 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver;
}
public static IPBSolver newCuttingPlanesGreedy() {
PBSolverCP solver = newCuttingPlanes();
IOrder order = new RandomWalkDecorator((VarOrderHeap) solver.getOrder(),
1.0);
order.setPhaseSelectionStrategy(new RandomLiteralSelectionStrategy());
solver.setOrder(order);
return solver;
}
public static IPBSolver newPartialRoundingSatPOS2020() {
PBSolverCP solver = (PBSolverCP) newPartialRoundingSat();
......
......@@ -154,4 +154,16 @@ public final class AtLeastPB extends AtLeast implements PBConstr {
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
private int id;
@Override
public void setId(int id) {
this.id = id;
}
@Override
public int getId() {
return id;
}
}
......@@ -31,11 +31,14 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.pb.IPBSolverService;
import org.sat4j.pb.core.PBSolverStats;
import org.sat4j.pb.tools.PBSearchListener;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
......@@ -176,6 +179,11 @@ public class ConflictMap extends MapPb implements IConflict {
}
}
@Override
public void setListener(PBSearchListener<IPBSolverService> listener) {
this.listener = listener;
}
/**
* convert level into an index in the byLevel structure
*
......@@ -278,6 +286,7 @@ public class ConflictMap extends MapPb implements IConflict {
public BigInteger resolve(PBConstr cpb, int litImplied,
VarActivityListener val) {
assert litImplied > 1;
listener.withReason(cpb);
preProcess();
int nLitImplied = litImplied ^ 1;
if (cpb == null || !this.weightedLits.containsKey(nLitImplied)) {
......@@ -388,6 +397,7 @@ public class ConflictMap extends MapPb implements IConflict {
// coefficients of the conflict must be multiplied by coefMult
long before = System.nanoTime();
if (!this.coefMult.equals(BigInteger.ONE)) {
listener.multiplyConflict(coefMult);
for (int i = 0; i < size(); i++) {
changeCoef(i, this.weightedLits.getCoef(i)
.multiply(this.coefMult));
......@@ -720,6 +730,7 @@ public class ConflictMap extends MapPb implements IConflict {
this.possReducedCoefs = this.possReducedCoefs.subtract(coefsBis[lit]);
coefsBis[lit] = BigInteger.ZERO;
assert this.possReducedCoefs.equals(possConstraint(wpb, coefsBis));
listener.weakenOnReason(LiteralsUtils.toDimacs(wpb.get(lit)));
// saturation of the constraint
degUpdate = saturation(coefsBis, degUpdate, wpb);
......@@ -735,6 +746,7 @@ public class ConflictMap extends MapPb implements IConflict {
assert degree.signum() > 0;
BigInteger degreeResult = degree;
boolean isMinimumEqualsToDegree = true;
boolean useSaturation = false;
int comparison;
for (int i = 0; i < coefs.length; i++) {
comparison = coefs[i].compareTo(degree);
......@@ -745,6 +757,7 @@ public class ConflictMap extends MapPb implements IConflict {
this.possReducedCoefs = this.possReducedCoefs.add(degree);
}
coefs[i] = degree;
useSaturation = true;
} else if (comparison < 0 && coefs[i].signum() > 0) {
isMinimumEqualsToDegree = false;
}
......@@ -764,6 +777,10 @@ public class ConflictMap extends MapPb implements IConflict {
}
}
}
listener.divideReason(degree);
}
if (useSaturation) {
listener.saturateReason();
}
return degreeResult;
}
......@@ -1023,7 +1040,6 @@ public class ConflictMap extends MapPb implements IConflict {
}
this.byLevel[0].push(lit);
}
}
}
......@@ -31,6 +31,8 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
public final class ConflictMapClause extends ConflictMap {
public ConflictMapClause(PBConstr cpb, int level) {
......@@ -68,8 +70,14 @@ public final class ConflictMapClause extends ConflictMap {
reducedCoefs[i] = BigInteger.ONE;
} else {
reducedCoefs[i] = BigInteger.ZERO;
listener.weakenOnReason(LiteralsUtils.toDimacs(wpb.get(i)));
}
}
// FIXME This is mostly a hack (maybe?)
listener.divideReason(degree);
listener.saturateReason();
this.coefMultCons = this.weightedLits.get(litImplied ^ 1);
this.coefMult = BigInteger.ONE;
return BigInteger.ONE;
......
......@@ -32,6 +32,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.pb.core.PBSolverStats;
/**
......@@ -236,11 +237,14 @@ public class ConflictMapDivideByPivot extends ConflictMap {
BigInteger[] tmp = divisionStrategy.divide(reducedCoefs[i],
coeffImplied);
reducedCoefs[i] = tmp[0];
listener.weakenOnReason(tmp[1],
LiteralsUtils.toDimacs(weightedLits.getLit(i)));
outputDegree = outputDegree.subtract(tmp[1]);
}
}
outputDegree = saturation(reducedCoefs,
ceildiv(outputDegree, coeffImplied), wpb);
listener.divideReason(coeffImplied);
}
this.stats.incNumberOfRoundingOperations();
this.reduceConflict.reduceConflict(this, litImplied ^ 1);
......
......@@ -34,6 +34,7 @@ import java.math.BigInteger;
import java.util.Map;
import java.util.TreeMap;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.pb.core.PBSolverStats;
......@@ -103,6 +104,7 @@ public class ConflictMapMinimizeWeakening extends ConflictMap {
this.possReducedCoefs = this.possReducedCoefs.subtract(coefsBis[lit]);
coefsBis[lit] = BigInteger.ZERO;
assert this.possReducedCoefs.equals(possConstraint(wpb, coefsBis));
listener.weakenOnReason(LiteralsUtils.toDimacs(wpb.get(lit)));
// saturation of the constraint
degUpdate = saturation(coefsBis, degUpdate, wpb);
......
......@@ -2,6 +2,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.pb.core.PBSolverStats;
/**
......@@ -98,8 +99,16 @@ public class ConflictMapReduceToCard extends ConflictMap {
cpt++;
} else {
reducedCoefs[i] = tmpCoefs[i];
if (tmpCoefs[i].equals(BigInteger.ZERO)) {
listener.weakenOnReason(LiteralsUtils.toDimacs(wpb.get(i)));
}
}
}
// FIXME We must notify the listener that the degree has changed, but
// how?
// listener.?
return BigInteger.valueOf(cpt + 1L);
}
......
......@@ -31,6 +31,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.pb.core.PBSolverStats;
public final class ConflictMapReduceToClause extends ConflictMap {
......@@ -102,8 +103,14 @@ public final class ConflictMapReduceToClause extends ConflictMap {
reducedCoefs[i] = BigInteger.ONE;
} else {
reducedCoefs[i] = BigInteger.ZERO;
listener.weakenOnReason(LiteralsUtils.toDimacs(wpb.get(i)));
}
}
// FIXME This is mostly a hack (maybe?)
listener.divideReason(degree);
listener.saturateReason();
return BigInteger.ONE;
}
}