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

updates Sat4j

parent b80c39dc
Pipeline #17731 passed with stages
in 59 minutes
......@@ -3,6 +3,7 @@
*/
package org.sat4j.pb;
import java.io.PrintWriter;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;
......@@ -92,8 +93,11 @@ public class PreprocessibleSolver extends PBSolverDecorator {
@Override
public String toString(String prefix) {
return super.toString(prefix);
StringBuilder sb = new StringBuilder();
sb.append(prefix + "Sequence of preprocessing techniques:\n");
sb.append(this.preprocessor.toString(prefix));
sb.append(super.toString(prefix));
return sb.toString();
}
@Override
......@@ -150,4 +154,11 @@ public class PreprocessibleSolver extends PBSolverDecorator {
return super.isSatisfiable(assumps);
}
@Override
public void printInfos(PrintWriter out, String prefix) {
out.println(prefix + "Sequence of preprocessing techniques:");
out.println(this.preprocessor.toString(prefix));
super.printInfos(out);
}
}
......@@ -40,4 +40,14 @@ public abstract class AbstractPBPreprocessing implements PBPreprocessing {
protected abstract List<PBPreprocessingConstraint> internalPreprocess(
List<PBPreprocessingConstraint> constraints);
public String toString(String prefix) {
StringBuilder sb = new StringBuilder();
sb.append(next.toString(prefix));
sb.append(prefix);
sb.append(" - ");
sb.append(getClass().getSimpleName());
sb.append("\n");
return sb.toString();
}
}
......@@ -88,4 +88,5 @@ public class DegreeModifierPBPreprocessing extends AbstractPBPreprocessing {
return PBPreprocessingConstraint.newAtLeast(constraint.getLiterals(),
constraint.getCoeffs(), BigInteger.valueOf(degree));
}
}
......@@ -33,4 +33,9 @@ public final class NullPBPreprocessing implements PBPreprocessing {
}
@Override
public String toString(String prefix) {
return "";
}
}
......@@ -16,4 +16,6 @@ public interface PBPreprocessing {
List<PBPreprocessingConstraint> constraints);
void setStats(PBSolverStats stats);
String toString(String prefix);
}
......@@ -6,14 +6,20 @@ package org.sat4j.pb.preprocessing;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
import org.sat4j.pb.tools.PBSearchListener;
import org.sat4j.pb.tools.PBSearchListenerAdapter;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolverService;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.TimeoutException;
/**
......@@ -23,6 +29,20 @@ import org.sat4j.specs.TimeoutException;
public class ProbingPBPreprocessing extends AbstractPBPreprocessing {
private final IPBSolver solver = SolverFactory.newEmptySolver();
private IVecInt[] propagatedLiterals;
private final List<PBPreprocessingConstraint> inferredConstraints = new ArrayList<>();
private final PBSearchListener<ISolverService> listener(int lit) {
propagatedLiterals[LiteralsUtils.toInternal(lit)] = new VecInt();
return new PBSearchListenerAdapter<ISolverService>() {
@Override
public void enqueueing(int p, org.sat4j.specs.IConstr reason) {
propagatedLiterals[LiteralsUtils.toInternal(lit)]
.push(LiteralsUtils.toDimacs(p));
}
};
}
@Override
protected List<PBPreprocessingConstraint> internalPreprocess(
......@@ -37,35 +57,78 @@ public class ProbingPBPreprocessing extends AbstractPBPreprocessing {
});
IVecInt literals = new VecInt();
IVec<BigInteger> coeffs = new Vec<>();
propagatedLiterals = new IVecInt[(solver.nVars() << 1) + 2];
for (int i = 1; i <= solver.nVars(); i++) {
int nb = 0;
for (int j = -1; j <= 1; j += 2) {
int lit = i * j;
try {
int lit = i * j;
solver.setSearchListener(listener(lit));
if (solver.isSatisfiable(VecInt.of(lit))) {
// the problem is satisfiable
} else {
literals.push(lit);
coeffs.push(BigInteger.ONE);
if (!literals.contains(lit)) {
literals.push(lit);
coeffs.push(BigInteger.ONE);
}
nb++;
continue;
}
} catch (TimeoutException e) {
}
inferConstraint(lit).ifPresent(inferredConstraints::add);
}
if (nb == 2) {
return List.of(PBPreprocessingConstraint
.newAtLeast(VecInt.EMPTY, Vec.of(), BigInteger.ONE));
}
checkRequiredLiterals(i, literals, coeffs);
}
if (literals.isEmpty()) {
return constraints;
}
List<PBPreprocessingConstraint> outConstraint = new ArrayList<>(
constraints);
outConstraint.addAll(inferredConstraints);
outConstraint.add(PBPreprocessingConstraint.newAtLeast(literals, coeffs,
BigInteger.valueOf(literals.size())));
return outConstraint;
}
private void checkRequiredLiterals(int i, IVecInt literals,
IVec<BigInteger> coeffs) {
for (IteratorInt it = propagatedLiterals[LiteralsUtils.posLit(i)]
.iterator(); it.hasNext();) {
int l = it.next();
if (propagatedLiterals[LiteralsUtils.negLit(i)].contains(l)) {
if (!literals.contains(l)) {
literals.push(l);
coeffs.push(BigInteger.ONE);
}
}
}
}
private Optional<PBPreprocessingConstraint> inferConstraint(int lit) {
IVecInt literals = new VecInt();
IVec<BigInteger> coeffs = new Vec<>();
for (IteratorInt it = propagatedLiterals[LiteralsUtils.toInternal(lit)]
.iterator(); it.hasNext();) {
int p = it.next();
if (p != lit) {
literals.push(p);
coeffs.push(BigInteger.ONE);
}
}
if (literals.isEmpty()) {
return Optional.empty();
}
BigInteger degree = BigInteger.valueOf(literals.size());
literals.push(-lit);
coeffs.push(degree);
return Optional.of(
PBPreprocessingConstraint.newAtLeast(literals, coeffs, degree));
}
}
......@@ -119,7 +119,7 @@ public class KTHLauncher {
//Preproc
options.addOption("p", "preproc-strategy", true,
options.addOption("p", "preprocessing-strategy", true,
"Preprocessing strategy");
Option op = options.getOption("coeflim");
......
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