Commit 42574367 authored by Thibault Falque's avatar Thibault Falque
Browse files

strategy for select next equation for the gauss elimination

parent b7310b2f
Pipeline #17640 failed with stages
in 21 minutes and 10 seconds
......@@ -92,6 +92,7 @@ public class PreprocessibleSolver extends PBSolverDecorator {
}
private boolean addConstraints() {
System.out.println("coucou");
if (!added) {
added = true;
for (PBPreprocessingConstraint c : preprocessor
......
......@@ -1331,8 +1331,8 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
public static IPBSolver newGaussPreprocessingSolver() {
return new PreprocessibleSolver(newCuttingPlanesPOS2020WL(),
new GaussPBPreprocessing(null));
return new PreprocessibleSolver(newOPBStringSolver(),
new GaussPBPreprocessing());
}
}
\ No newline at end of file
/**
* Sat4j-CSP, a CSP solver based on the Sat4j platform.
* Copyright (c) 2021-2022 - Thibault Falque and Romain Wallon.
* All rights reserved.
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
*
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
* See the GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library.
* If not, see {@link http://www.gnu.org/licenses}.
*/
package org.sat4j.pb.preprocessing;
import java.util.Iterator;
import java.util.List;
/**
* The AbstractEquationSelectionStrategy
*
* @author Thibault Falque
* @author Romain Wallon
*
* @version 0.1.0
*/
public abstract class AbstractEquationSelectionStrategy
implements Iterable<PBEquationSelectionStrategyIteratorObject>,
Iterator<PBEquationSelectionStrategyIteratorObject> {
protected List<PBPreprocessingConstraint> equations;
public AbstractEquationSelectionStrategy(
List<PBPreprocessingConstraint> equations) {
this.equations = equations;
}
}
......@@ -24,6 +24,7 @@ public abstract class AbstractPBPreprocessing implements PBPreprocessing {
@Override
public List<PBPreprocessingConstraint> preprocess(
List<PBPreprocessingConstraint> constraints) {
return next.preprocess(internalPreprocess(constraints));
}
......
/**
* Sat4j-CSP, a CSP solver based on the Sat4j platform.
* Copyright (c) 2021-2022 - Thibault Falque and Romain Wallon.
* All rights reserved.
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
*
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
* See the GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library.
* If not, see {@link http://www.gnu.org/licenses}.
*/
package org.sat4j.pb.preprocessing;
/**
* The AllConstraintGroupSelectionStrategy
*
* @author Thibault Falque
* @author Romain Wallon
*
* @version 0.1.0
*/
public class AllConstraintGroupSelectionStrategy
implements IConstraintGroupSelectionStrategy {
/*
* (non-Javadoc)
*
* @see
* org.sat4j.pb.preprocessing.IConstraintGroupSelectionStrategy#add(org.
* sat4j.pb.preprocessing.PBPreprocessingConstraintGroup,
* org.sat4j.pb.preprocessing.PBPreprocessingConstraint)
*/
@Override
public boolean add(PBPreprocessingConstraintGroup group,
PBPreprocessingConstraint constraint) {
group.add(constraint);
return true;
}
}
/**
* Sat4j-CSP, a CSP solver based on the Sat4j platform.
* Copyright (c) 2021-2022 - Thibault Falque and Romain Wallon.
* All rights reserved.
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
*
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
* See the GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library.
* If not, see {@link http://www.gnu.org/licenses}.
*/
package org.sat4j.pb.preprocessing;
import java.math.BigInteger;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.TreeSet;
import org.sat4j.specs.IteratorInt;
/**
* The DefaultEquationSelectionStrategy
*
* @author Thibault Falque
* @author Romain Wallon
*
* @version 0.1.0
*/
public class DefaultEquationSelectionStrategy
extends AbstractEquationSelectionStrategy {
private int currentLine;
private final Set<Integer> variables = new TreeSet<>();
private final Iterator<Integer> iterator;
public DefaultEquationSelectionStrategy(
List<PBPreprocessingConstraint> equations) {
super(equations);
currentLine = 0;
for (PBPreprocessingConstraint constraint : this.equations) {
for (IteratorInt it = constraint.getLiterals().iterator(); it
.hasNext();) {
this.variables.add(it.next());
}
}
iterator = variables.iterator();
}
@Override
public Iterator<PBEquationSelectionStrategyIteratorObject> iterator() {
return this;
}
@Override
public boolean hasNext() {
return iterator.hasNext() && currentLine < equations.size();
}
@Override
public PBEquationSelectionStrategyIteratorObject next() {
Integer lit = iterator.next();
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;
}
}
currentLine++;
return new PBEquationSelectionStrategyIteratorObject(
equations.get(bestEquation), bestEquation, lit);
}
}
......@@ -12,7 +12,7 @@ import java.util.List;
*/
public class GaussPBPreprocessing extends AbstractPBPreprocessing {
private final List<PBPreprocessingConstraintGroup> groups;
private IConstraintGroupSelectionStrategy strategy;
private final IConstraintGroupSelectionStrategy strategy;
/**
* @param next
......@@ -21,17 +21,23 @@ public class GaussPBPreprocessing extends AbstractPBPreprocessing {
public GaussPBPreprocessing(PBPreprocessing next) {
super(next);
this.groups = new ArrayList<>();
this.strategy = new AllConstraintGroupSelectionStrategy();
}
public GaussPBPreprocessing() {
super();
this.groups = new ArrayList<>();
this.strategy = new AllConstraintGroupSelectionStrategy();
}
@Override
protected List<PBPreprocessingConstraint> internalPreprocess(
List<PBPreprocessingConstraint> constraints) {
for (PBPreprocessingConstraint pbCtr : constraints) {
if (pbCtr.getType() != PBPreprocessingConstraintType.EQ) {
continue;
}
pbCtr = pbCtr.translateToVarOnly();
if (!strategy.add(groups, pbCtr)) {
PBPreprocessingConstraintGroup group = new PBPreprocessingConstraintGroup();
group.add(pbCtr);
......@@ -50,7 +56,8 @@ public class GaussPBPreprocessing extends AbstractPBPreprocessing {
private List<PBPreprocessingConstraint> applyGauss(
List<PBPreprocessingConstraint> constraints) {
SystemPreprocessing system = new SystemPreprocessing(constraints);
SystemPreprocessing system = new SystemPreprocessing(constraints,
new DefaultEquationSelectionStrategy(constraints));
return system.compute();
}
......
/**
* Sat4j-CSP, a CSP solver based on the Sat4j platform.
* Copyright (c) 2021-2022 - Thibault Falque and Romain Wallon.
* All rights reserved.
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
*
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
* See the GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library.
* If not, see {@link http://www.gnu.org/licenses}.
*/
package org.sat4j.pb.preprocessing;
import java.util.Iterator;
import java.util.List;
/**
* The MinCoeffEquationSelectionStrategy
*
* @author Thibault Falque
* @author Romain Wallon
*
* @version 0.1.0
*/
public class MinCoeffEquationSelectionStrategy
extends AbstractEquationSelectionStrategy {
public MinCoeffEquationSelectionStrategy(
List<PBPreprocessingConstraint> equations) {
super(equations);
}
/*
* (non-Javadoc)
*
* @see java.lang.Iterable#iterator()
*/
@Override
public Iterator<PBEquationSelectionStrategyIteratorObject> iterator() {
return this;
}
/*
* (non-Javadoc)
*
* @see java.util.Iterator#hasNext()
*/
@Override
public boolean hasNext() {
// TODO Auto-generated method stub
return false;
}
/*
* (non-Javadoc)
*
* @see java.util.Iterator#next()
*/
@Override
public PBEquationSelectionStrategyIteratorObject next() {
// TODO Auto-generated method stub
return null;
}
}
/**
* Sat4j-CSP, a CSP solver based on the Sat4j platform.
* Copyright (c) 2021-2022 - Thibault Falque and Romain Wallon.
* All rights reserved.
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
*
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
* See the GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library.
* If not, see {@link http://www.gnu.org/licenses}.
*/
package org.sat4j.pb.preprocessing;
/**
* The PBEquationSelectionStrategyIteratorObject
*
* @author Thibault Falque
* @author Romain Wallon
*
* @version 0.1.0
*/
public class PBEquationSelectionStrategyIteratorObject {
private final PBPreprocessingConstraint constraint;
private final int indexConstraint;
private final int lit;
public PBEquationSelectionStrategyIteratorObject(
PBPreprocessingConstraint constraint, int indexConstraint,
int lit) {
this.lit = lit;
this.constraint = constraint;
this.indexConstraint = indexConstraint;
}
public PBPreprocessingConstraint getConstraint() {
return constraint;
}
public int getLit() {
return lit;
}
public int getIndexConstraint() {
return indexConstraint;
}
}
......@@ -39,6 +39,50 @@ public class PBPreprocessingConstraint implements ITransformConstraint {
return coeffs.get(index);
}
public PBPreprocessingConstraint translateToVarOnly() {
IVecInt variables = new VecInt(literals.size());
IVec<BigInteger> localCoeffs = new Vec<>(literals.size());
BigInteger degree = weight;
for (int i = 0; i < literals.size(); i++) {
int lit = literals.get(i);
BigInteger coeff = coeffs.get(i);
if (lit > 0) {
variables.push(lit);
localCoeffs.push(coeff);
} else {
variables.push(-lit);
localCoeffs.push(coeff.negate());
degree = degree.subtract(coeff);
}
}
return new PBPreprocessingConstraint(variables, localCoeffs, degree,
type);
}
public PBPreprocessingConstraint normalize() {
IVecInt localLiterals = new VecInt(literals.size());
IVec<BigInteger> localCoeffs = new Vec<>(literals.size());
BigInteger degree = weight;
for (int i = 0; i < literals.size(); i++) {
int lit = literals.get(i);
BigInteger coeff = coeffs.get(i);
if (coeff.signum() > 0) {
localLiterals.push(lit);
localCoeffs.push(coeff);
} else {
localLiterals.push(-lit);
localCoeffs.push(coeff.negate());
degree = degree.subtract(coeff);
}
}
return new PBPreprocessingConstraint(localLiterals, localCoeffs, degree,
type);
}
/**
* @return the coeffs
*/
......
......@@ -45,6 +45,9 @@ public enum PBPreprocessingConstraintType {
public void addConstraintToSolver(IVecInt literals,
IVec<BigInteger> coeffs, BigInteger degree, IPBSolver solver)
throws ContradictionException {
System.out.println(literals);
System.out.println(coeffs);
System.out.println(degree);
solver.addExactly(literals, coeffs, degree);
}
......
......@@ -5,11 +5,8 @@ package org.sat4j.pb.preprocessing;
import java.math.BigInteger;
import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import org.sat4j.specs.IteratorInt;
/**
* @author Thibault Falque
......@@ -17,20 +14,16 @@ import org.sat4j.specs.IteratorInt;
*/
public class SystemPreprocessing {
private final List<PBPreprocessingConstraint> equations;
private final Set<Integer> variables = new HashSet<>();
private final AbstractEquationSelectionStrategy strategy;
/**
*
* @param constraints
*/
public SystemPreprocessing(List<PBPreprocessingConstraint> constraints) {
public SystemPreprocessing(List<PBPreprocessingConstraint> constraints,
AbstractEquationSelectionStrategy strategy) {
this.equations = constraints;
for (PBPreprocessingConstraint constraint : this.equations) {
for (IteratorInt it = constraint.getLiterals().iterator(); it
.hasNext();) {
this.variables.add(it.next());
}
}
this.strategy = strategy;
}
/**
......@@ -39,16 +32,25 @@ public class SystemPreprocessing {
*/
public List<PBPreprocessingConstraint> compute() {
int currentLine = 0;
for (Integer i : variables) {
int bestEquation = computeBestEquation(currentLine, i);
Collections.swap(equations, currentLine, bestEquation);
applyGaussianElimination(currentLine, i);
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 null;
return equations;
}
/**
......@@ -57,21 +59,21 @@ public class SystemPreprocessing {
* @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;
}
// 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;
// }
/**
*
......
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