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

Gauss OK

parent f2fb44bb
Pipeline #17671 passed with stages
in 41 minutes and 16 seconds
......@@ -8,7 +8,8 @@ import java.util.ArrayList;
import java.util.List;
import org.sat4j.core.ConstrGroup;
import org.sat4j.pb.preprocessing.IConstraintGroupSelectionStrategy;
import org.sat4j.pb.core.PBSolver;
import org.sat4j.pb.core.PBSolverStats;
import org.sat4j.pb.preprocessing.PBPreprocessing;
import org.sat4j.pb.preprocessing.PBPreprocessingConstraint;
import org.sat4j.specs.ContradictionException;
......@@ -24,7 +25,6 @@ import org.sat4j.specs.TimeoutException;
*/
public class PreprocessibleSolver extends PBSolverDecorator {
private final List<PBPreprocessingConstraint> constraints;
private IConstraintGroupSelectionStrategy strategy;
private final PBPreprocessing preprocessor;
private boolean added;
......@@ -33,6 +33,8 @@ public class PreprocessibleSolver extends PBSolverDecorator {
PBPreprocessing preprocessor) {
super(solver);
this.preprocessor = preprocessor;
this.preprocessor
.setStats((PBSolverStats) ((PBSolver) decorated()).getStats());
this.constraints = new ArrayList<>();
}
......@@ -74,6 +76,9 @@ public class PreprocessibleSolver extends PBSolverDecorator {
BigInteger weight) throws ContradictionException {
constraints.add(
PBPreprocessingConstraint.newExactly(literals, coeffs, weight));
PBSolver solver = (PBSolver) decorated();
((PBSolverStats) solver.getStats()).incNbExactlyConstraint();
return new ConstrGroup();
}
......@@ -92,7 +97,6 @@ public class PreprocessibleSolver extends PBSolverDecorator {
}
private boolean addConstraints() {
System.out.println("coucou");
if (!added) {
added = true;
for (PBPreprocessingConstraint c : preprocessor
......
......@@ -1323,8 +1323,18 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver;
}
public static IPBSolver newGaussPreprocessingSolver() {
return new PreprocessibleSolver(newOPBStringSolver(),
public static IPBSolver newGaussPreprocessingCuttingPlanesPOS2020Solver() {
return new PreprocessibleSolver(newCuttingPlanesPOS2020(),
new GaussPBPreprocessing());
}
public static IPBSolver newGaussPreprocessingPartialRoundingSatPOS2020Solver() {
return new PreprocessibleSolver(newPartialRoundingSatPOS2020(),
new GaussPBPreprocessing());
}
public static IPBSolver newGaussPreprocessingRoundingSatPOS2020Solver() {
return new PreprocessibleSolver(newRoundingSatPOS2020(),
new GaussPBPreprocessing());
}
......
......@@ -31,8 +31,11 @@ package org.sat4j.pb.core;
import java.io.PrintWriter;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.pb.preprocessing.GaussianEliminationGroupStat;
public class PBSolverStats extends SolverStats {
......@@ -81,6 +84,10 @@ public class PBSolverStats extends SolverStats {
private int nbRemoved;
private int nbExactlyConstraints;
private final List<GaussianEliminationGroupStat> statsGaussian = new ArrayList<>();
@Override
public void reset() {
super.reset();
......@@ -97,6 +104,8 @@ public class PBSolverStats extends SolverStats {
this.numberOfDerivationSteps = 0;
this.numberOfRemainingUnassigned = 0;
this.numberOfRemainingAssigned = 0;
this.nbExactlyConstraints = 0;
this.statsGaussian.clear();
}
@Override
......@@ -153,6 +162,15 @@ public class PBSolverStats extends SolverStats {
+ this.maxRemoved);
out.println(
prefix + "number of deleted constraints\t: " + this.nbRemoved);
out.println(prefix + "number of exactly constraints "
+ this.nbExactlyConstraints);
int index = 0;
for (GaussianEliminationGroupStat s : this.statsGaussian) {
out.println(prefix + " group " + index);
s.printStat(out, prefix);
index++;
}
}
public long getNumberOfReductions() {
......@@ -301,4 +319,18 @@ public class PBSolverStats extends SolverStats {
this.nbRemoved++;
}
public void incNbExactlyConstraint() {
this.nbExactlyConstraints++;
}
/**
* @return the nbExactlyConstraints
*/
public int getNbExactlyConstraints() {
return nbExactlyConstraints;
}
public void addGaussianStat(GaussianEliminationGroupStat s) {
this.statsGaussian.add(s);
}
}
......@@ -5,6 +5,8 @@ package org.sat4j.pb.preprocessing;
import java.util.List;
import org.sat4j.pb.core.PBSolverStats;
/**
* @author Thibault Falque
*
......@@ -12,6 +14,7 @@ import java.util.List;
public abstract class AbstractPBPreprocessing implements PBPreprocessing {
private final PBPreprocessing next;
protected PBSolverStats stats;
public AbstractPBPreprocessing(PBPreprocessing next) {
this.next = next;
......@@ -28,6 +31,12 @@ public abstract class AbstractPBPreprocessing implements PBPreprocessing {
return next.preprocess(internalPreprocess(constraints));
}
@Override
public void setStats(PBSolverStats stats) {
this.stats = stats;
this.next.setStats(stats);
}
protected abstract List<PBPreprocessingConstraint> internalPreprocess(
List<PBPreprocessingConstraint> constraints);
......
......@@ -57,7 +57,7 @@ public class GaussPBPreprocessing extends AbstractPBPreprocessing {
List<PBPreprocessingConstraint> constraints) {
SystemPreprocessing system = new SystemPreprocessing(constraints,
new DefaultEquationSelectionStrategy(constraints));
new MinCoeffEquationSelectionStrategy(constraints));
return system.compute();
}
......
/**
*
*/
package org.sat4j.pb.preprocessing;
import java.io.PrintWriter;
/**
* @author Thibault Falque
*
*/
public class GaussianEliminationGroupStat {
private final int size;
private int nbGaussianElimination;
/**
* @param size
* @param nbGaussianElimination
*/
public GaussianEliminationGroupStat(int size) {
super();
this.size = size;
this.nbGaussianElimination = 0;
}
/**
* @return the size
*/
public int getSize() {
return size;
}
/**
* @return the nbGaussianElimination
*/
public int getNbGaussianElimination() {
return nbGaussianElimination;
}
public void incGaussianElimination() {
nbGaussianElimination++;
}
public void printStat(PrintWriter out, String prefix) {
out.println(prefix + " sizeGroup = " + this.size);
out.println(prefix + " GaussianElimination = "
+ this.nbGaussianElimination);
}
}
......@@ -20,6 +20,7 @@
package org.sat4j.pb.preprocessing;
import java.math.BigInteger;
import java.util.Iterator;
import java.util.List;
......@@ -34,6 +35,8 @@ import java.util.List;
public class MinCoeffEquationSelectionStrategy
extends AbstractEquationSelectionStrategy {
private int currentLine;
public MinCoeffEquationSelectionStrategy(
List<PBPreprocessingConstraint> equations) {
super(equations);
......@@ -56,8 +59,7 @@ public class MinCoeffEquationSelectionStrategy
*/
@Override
public boolean hasNext() {
// TODO Auto-generated method stub
return false;
return currentLine < equations.size();
}
/*
......@@ -67,8 +69,28 @@ public class MinCoeffEquationSelectionStrategy
*/
@Override
public PBEquationSelectionStrategyIteratorObject next() {
// TODO Auto-generated method stub
return null;
int bestEquation = currentLine;
int minLit = equations.get(currentLine).getVarWithMinCoeff();
BigInteger min = equations.get(currentLine).getCoeff(minLit).abs();
for (int i = currentLine + 1; i < equations.size(); i++) {
int localMinLit = equations.get(i).getVarWithMinCoeff();
BigInteger currentCoeff = equations.get(i).getCoeff(localMinLit)
.abs();
if (currentCoeff.compareTo(min) < 0) {
minLit = localMinLit;
min = currentCoeff;
bestEquation = i;
}
}
currentLine++;
return new PBEquationSelectionStrategyIteratorObject(
equations.get(bestEquation), bestEquation, minLit);
}
}
......@@ -5,6 +5,8 @@ package org.sat4j.pb.preprocessing;
import java.util.List;
import org.sat4j.pb.core.PBSolverStats;
/**
* @author Thibault Falque
*
......@@ -26,4 +28,9 @@ public final class NullPBPreprocessing implements PBPreprocessing {
return constraints;
}
@Override
public void setStats(PBSolverStats stats) {
}
}
......@@ -5,6 +5,8 @@ package org.sat4j.pb.preprocessing;
import java.util.List;
import org.sat4j.pb.core.PBSolverStats;
/**
* @author Thibault Falque
*
......@@ -12,4 +14,6 @@ import java.util.List;
public interface PBPreprocessing {
List<PBPreprocessingConstraint> preprocess(
List<PBPreprocessingConstraint> constraints);
void setStats(PBSolverStats stats);
}
......@@ -39,6 +39,18 @@ public class PBPreprocessingConstraint implements ITransformConstraint {
return coeffs.get(index);
}
public int getVarWithMinCoeff() {
int indexMin = 0;
BigInteger min = coeffs.get(indexMin).abs();
for (int i = indexMin + 1; i < coeffs.size(); i++) {
if (coeffs.get(i).abs().compareTo(min) < 0) {
min = coeffs.get(i).abs();
indexMin = i;
}
}
return literals.get(indexMin);
}
public PBPreprocessingConstraint translateToVarOnly() {
IVecInt variables = new VecInt(literals.size());
IVec<BigInteger> localCoeffs = new Vec<>(literals.size());
......
......@@ -16,6 +16,8 @@ public class SystemPreprocessing {
private final List<PBPreprocessingConstraint> equations;
private final AbstractEquationSelectionStrategy strategy;
private final GaussianEliminationGroupStat stats;
/**
*
* @param constraints
......@@ -24,6 +26,7 @@ public class SystemPreprocessing {
AbstractEquationSelectionStrategy strategy) {
this.equations = constraints;
this.strategy = strategy;
this.stats = new GaussianEliminationGroupStat(constraints.size());
}
/**
......@@ -34,47 +37,14 @@ public class SystemPreprocessing {
int currentLine = 0;
for (Iterator<PBEquationSelectionStrategyIteratorObject> it = strategy
.iterator(); it.hasNext();) {
System.out.println("toto");
PBEquationSelectionStrategyIteratorObject obj = it.next();
Collections.swap(equations, currentLine, obj.getIndexConstraint());
applyGaussianElimination(currentLine, obj.getLit());
currentLine++;
}
// for (Integer i : variables) {
// int bestEquation = computeBestEquation(currentLine, i);
// Collections.swap(equations, currentLine, bestEquation);
// applyGaussianElimination(currentLine, i);
// currentLine++;
// if (currentLine >= equations.size()) {
// break;
// }
// }
return equations;
}
/**
*
* @param currentLine
* @param lit
* @return
*/
// private int computeBestEquation(int currentLine, int lit) {
// int bestEquation = currentLine;
// BigInteger min = equations.get(currentLine).getCoeff(lit);
// for (int i = currentLine + 1; i < equations.size(); i++) {
// BigInteger currentCoeff = equations.get(i).getCoeff(lit);
// if (currentCoeff.equals(BigInteger.ZERO))
// continue;
// if ((min.equals(BigInteger.ZERO))
// || (min.compareTo(currentCoeff) == 1)) {
// bestEquation = i;
// min = currentCoeff;
// }
// }
// return bestEquation;
// }
/**
*
* @param currentLine
......@@ -88,6 +58,7 @@ public class SystemPreprocessing {
if (e.getCoeff(v).equals(BigInteger.ZERO))
continue;
equations.set(i, p.mult(e.getCoeff(v)).sub(e.mult(c)));
this.stats.incGaussianElimination();
}
}
......
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