Commit b80c39dc authored by tfalque.ext's avatar tfalque.ext
Browse files

Start Probing - Failed Literals

parent e6657f33
Pipeline #17681 passed with stages
in 41 minutes and 3 seconds
......@@ -90,6 +90,12 @@ public class PreprocessibleSolver extends PBSolverDecorator {
return new ConstrGroup();
}
@Override
public String toString(String prefix) {
return super.toString(prefix);
}
@Override
public void preprocessing() {
super.preprocessing();
......
......@@ -86,6 +86,8 @@ public class PBSolverStats extends SolverStats {
private int nbExactlyConstraints;
private int nbChangedDegree;
private final List<GaussianEliminationGroupStat> statsGaussian = new ArrayList<>();
@Override
......@@ -105,6 +107,7 @@ public class PBSolverStats extends SolverStats {
this.numberOfRemainingUnassigned = 0;
this.numberOfRemainingAssigned = 0;
this.nbExactlyConstraints = 0;
this.nbChangedDegree = 0;
this.statsGaussian.clear();
}
......@@ -162,6 +165,8 @@ public class PBSolverStats extends SolverStats {
+ this.maxRemoved);
out.println(
prefix + "number of deleted constraints\t: " + this.nbRemoved);
out.println(
prefix + "number of changed degree " + this.nbChangedDegree);
out.println(prefix + "number of exactly constraints "
+ this.nbExactlyConstraints);
int index = 0;
......@@ -319,6 +324,14 @@ public class PBSolverStats extends SolverStats {
this.nbRemoved++;
}
public void incNbChangedDegree() {
this.nbChangedDegree++;
}
public int getNbChangedDegree() {
return this.nbChangedDegree;
}
public void incNbExactlyConstraint() {
this.nbExactlyConstraints++;
}
......
......@@ -76,12 +76,14 @@ public class DegreeModifierPBPreprocessing extends AbstractPBPreprocessing {
subset.setElements(intCoeffs);
int degree = normalized.getWeight().intValue();
while (true) {
if (subset.sumExists(degree)) {
break;
}
int oldDegree = degree;
while (!subset.sumExists(degree)) {
degree = nextDegree.applyAsInt(degree);
}
if (oldDegree != degree) {
this.stats.incNbChangedDegree();
}
return PBPreprocessingConstraint.newAtLeast(constraint.getLiterals(),
constraint.getCoeffs(), BigInteger.valueOf(degree));
......
/**
*
*/
package org.sat4j.pb.preprocessing;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
/**
* @author Thibault Falque
*
*/
public class ProbingPBPreprocessing extends AbstractPBPreprocessing {
private final IPBSolver solver = SolverFactory.newEmptySolver();
@Override
protected List<PBPreprocessingConstraint> internalPreprocess(
List<PBPreprocessingConstraint> constraints) {
constraints.forEach(c -> {
try {
c.addConstraintToSolver(solver);
} catch (ContradictionException e) {
e.printStackTrace();
}
});
IVecInt literals = new VecInt();
IVec<BigInteger> coeffs = new Vec<>();
for (int i = 1; i <= solver.nVars(); i++) {
int nb = 0;
for (int j = -1; j <= 1; j += 2) {
try {
int lit = i * j;
if (solver.isSatisfiable(VecInt.of(lit))) {
// the problem is satisfiable
} else {
literals.push(lit);
coeffs.push(BigInteger.ONE);
nb++;
}
} catch (TimeoutException e) {
}
}
if (nb == 2) {
return List.of(PBPreprocessingConstraint
.newAtLeast(VecInt.EMPTY, Vec.of(), BigInteger.ONE));
}
}
if (literals.isEmpty()) {
return constraints;
}
List<PBPreprocessingConstraint> outConstraint = new ArrayList<>(
constraints);
outConstraint.add(PBPreprocessingConstraint.newAtLeast(literals, coeffs,
BigInteger.valueOf(literals.size())));
return outConstraint;
}
}
......@@ -23,6 +23,7 @@ import org.sat4j.minisat.restarts.NoRestarts;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.OptToPBSATAdapter;
import org.sat4j.pb.PBSolverHandle;
import org.sat4j.pb.PreprocessibleSolver;
import org.sat4j.pb.PseudoOptDecorator;
import org.sat4j.pb.SolverFactory;
import org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure;
......@@ -50,6 +51,10 @@ import org.sat4j.pb.orders.BumperEffective;
import org.sat4j.pb.orders.BumperEffectiveAndPropagated;
import org.sat4j.pb.orders.DoubleBumpClashingLiteralsDecorator;
import org.sat4j.pb.orders.IBumper;
import org.sat4j.pb.preprocessing.DegreeModifierPBPreprocessing;
import org.sat4j.pb.preprocessing.GaussPBPreprocessing;
import org.sat4j.pb.preprocessing.NullPBPreprocessing;
import org.sat4j.pb.preprocessing.PBPreprocessing;
import org.sat4j.pb.reader.OPBReader2012;
import org.sat4j.pb.restarts.GrowingCoefficientRestarts;
import org.sat4j.pb.tools.InprocCardConstrLearningSolver;
......@@ -69,6 +74,9 @@ public class KTHLauncher {
public static Options createCLIOptions() {
Options options = new Options();
options.addOption("s", "solver", true,"The solver name");
options.addOption("cl", "coeflim", true,
"coefficient limit triggering division");
options.addOption("cls", "coeflim-small", true,
......@@ -107,6 +115,13 @@ public class KTHLauncher {
"Literal bumper, among any, assigned and falsified");
options.addOption("db", "double-bump-clashing", false,
"Whether clashing literal should be doubly bumped");
//Preproc
options.addOption("p", "preproc-strategy", true,
"Preprocessing strategy");
Option op = options.getOption("coeflim");
op.setArgName("limit");
op = options.getOption("coeflim-small");
......@@ -178,8 +193,8 @@ public class KTHLauncher {
}
try {
CommandLine line = parser.parse(options, args);
PBSolverCP cpsolver = SolverFactory.newCuttingPlanes();
String solverName = line.getOptionValue("solver", "CuttingPlanes");
PBSolverCP cpsolver = (PBSolverCP) SolverFactory.instance().createSolverByName(solverName);
cpsolver.setNoRemove(true);
cpsolver.setSkipAllow(SkipStrategy.NO_SKIP);
IPBSolver pbsolver = cpsolver;
......@@ -513,6 +528,23 @@ public class KTHLauncher {
return;
}
}
if (line.hasOption("preprocessing-strategy")) {
String[] value = line.getOptionValue("preprocessing-strategy").split(",");
PBPreprocessing preproc = NullPBPreprocessing.instance();
for(String v:value) {
if("gauss".equals(v)) {
preproc=new GaussPBPreprocessing(preproc);
}
if("maxdegree".equals(v)) {
preproc=DegreeModifierPBPreprocessing.newMaxDegree(preproc);
}
}
pbsolver=new PreprocessibleSolver(cpsolver, preproc);
}
System.out.println(pbsolver.toString("c "));
String[] leftArgs = line.getArgs();
if (leftArgs.length == 0) {
......
Supports Markdown
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