Commit 1100b7a6 authored by lonca's avatar lonca
Browse files

Implemented minimization/maximization of single objectives for XCSP3.

Other test cases are coming soon.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2551 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent a69beae6
......@@ -20,20 +20,18 @@ package org.sat4j.csp.constraints3;
import java.math.BigInteger;
import java.util.Arrays;
import java.util.LinkedHashMap;
import java.util.Map;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.csp.Domain;
import org.sat4j.csp.Var;
import org.sat4j.csp.intension.ICspToSatEncoder;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.reader.XMLCSP3Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.xcsp.common.Types.TypeObjective;
import org.xcsp.common.predicates.XNodeParent;
import org.xcsp.parser.entries.XDomains.XDomInteger;
import org.xcsp.parser.entries.XVariables.XVarInteger;
......@@ -46,178 +44,177 @@ import org.xcsp.parser.entries.XVariables.XVarInteger;
*/
public class ObjBuilder {
/** the solver in which the problem is encoded */
private IPBSolver solver;
private final ICspToSatEncoder cspToSatEncoder;
private IIntensionCtrEncoder intensionEnc;
/** a mapping from the CSP variable names to Sat4j CSP variables */
private Map<String, Var> varmapping = new LinkedHashMap<String, Var>();
public ObjBuilder(final IPBSolver solver, final IIntensionCtrEncoder intensionEnc) {
this.intensionEnc = intensionEnc;
this.cspToSatEncoder = intensionEnc.getSolver();
}
/** a mapping from a Sat4j CSP variable to the first solver internal variable used to encode it */
private Map<Var, Integer> firstInternalVarMapping;
public ObjBuilder(IPBSolver solver, Map<String, Var> varmapping, Map<Var, Integer> firstInternalVarMapping) {
this.solver = solver;
this.varmapping = varmapping;
this.firstInternalVarMapping = firstInternalVarMapping;
public void buildObjToMinimize(final String id, final XVarInteger x) {
this.cspToSatEncoder.setObjectiveFunction(buildObjForVar(x));
}
public void buildObjToMaximize(String id, TypeObjective type, XVarInteger[] xlist, int[] xcoeffs) {
ObjectiveFunction globalObj = null;
switch(type) {
case SUM:
case MAXIMUM:
globalObj = buildObjForVarSum(xlist, xcoeffs);
globalObj.negate();
break;
case MINIMUM:
try {
globalObj = buildObjForVarMin(xlist, xcoeffs);
} catch (ContradictionException e) {
throw new IllegalStateException("Contradiction must not occur while setting objective function !!");
}
break;
default:
throw new UnsupportedOperationException("This kind of objective function is not handled yet");
private ObjectiveFunction buildObjForVar(final XVarInteger x) {
final String varId = x.id;
int[] domain = this.cspToSatEncoder.getCspVarDomain(varId);
final IVecInt literals = new VecInt(domain.length);
final IVec<BigInteger> coeffs = new Vec<BigInteger>(domain.length);
for(Integer val : domain) {
literals.push(this.cspToSatEncoder.getSolverVar(varId, val));
coeffs.push(BigInteger.valueOf(val));
}
this.solver.setObjectiveFunction(globalObj);
return new ObjectiveFunction(literals, coeffs);
}
public void buildObjToMinimize(String id, TypeObjective type, XVarInteger[] list) {
int[] coeffs = new int[list.length];
Arrays.fill(coeffs, 1);
buildObjToMinimize(id, type, list, coeffs);
}
public void buildObjToMinimize(String id, XVarInteger x) {
ObjectiveFunction obj = buildObjForVar(x);
this.solver.setObjectiveFunction(obj);
}
private ObjectiveFunction buildObjForVar(XVarInteger x) {
Var var = this.varmapping.get(x.id);
Domain dom = var.domain();
IVecInt literals = new VecInt(dom.size());
IVec<BigInteger> coeffs = new Vec<BigInteger>(dom.size());
Integer firstIndex = this.firstInternalVarMapping.get(var);
for(int i=0; i<dom.size(); ++i) {
literals.push(firstIndex+i);
coeffs.push(BigInteger.valueOf(dom.get(i)));
}
ObjectiveFunction obj = new ObjectiveFunction(literals, coeffs);
return obj;
public void buildObjToMaximize(final String id, final XVarInteger x) {
this.cspToSatEncoder.setObjectiveFunction(buildObjForVar(x).negate());
}
public void buildObjToMaximize(String id, XVarInteger x) {
buildObjToMinimize(id, x);
this.solver.getObjectiveFunction().negate();
private String opExpr(final String op, final XVarInteger[] xlist, final int[] xcoeffs) {
final StringBuffer sb = new StringBuffer();
sb.append(op);
sb.append('(');
sb.append(chainObjVars(xlist, xcoeffs));
sb.append(')');
return sb.toString();
}
public void buildObjToMinimize(String id, TypeObjective type, XVarInteger[] xlist, int[] xcoeffs) {
ObjectiveFunction globalObj = null;
private String chainObjVars(final XVarInteger[] xlist, final int[] xcoeffs) {
final StringBuffer sb = new StringBuffer();
for(int i=0; i<xlist.length; ++i) {
if(i>0) sb.append(',');
if(xcoeffs[i] == 1) {
sb.append(CtrBuilderUtils.normalizeCspVarName(xlist[i].id));
} else {
sb.append("mul(");
sb.append(CtrBuilderUtils.normalizeCspVarName(xlist[i].id));
sb.append(',');
sb.append(xcoeffs[i]);
sb.append(")");
}
}
sb.append(')');
return sb.toString();
}
public void buildObjToMinimize(final String id, final TypeObjective type, final XVarInteger[] xlist, final int[] xcoeffs) {
ObjectiveFunction obj = null;
switch(type) {
case SUM:
case MINIMUM:
globalObj = buildObjForVarSum(xlist, xcoeffs);
obj = buildSumObjToMinimize(xlist, xcoeffs);
break;
case PRODUCT:
obj = buildExprObjToMinimize(opExpr("mul", xlist, xcoeffs));
break;
case MAXIMUM:
try {
globalObj = buildObjForVarMax(xlist, xcoeffs);
} catch (ContradictionException e) {
throw new IllegalStateException("Contradiction must not occur while setting objective function !!");
}
obj = buildExprObjToMinimize(opExpr("max", xlist, xcoeffs));
break;
case MINIMUM:
obj = buildExprObjToMinimize(opExpr("min", xlist, xcoeffs));
break;
case NVALUES:
obj = buildExprObjToMinimize(nValuesExpr(xlist, xcoeffs));
break;
default:
throw new UnsupportedOperationException("This kind of objective function is not handled yet");
case LEX:
obj = buildLexObjToMinimize(xlist, xcoeffs);
break;
case EXPRESSION:
throw new UnsupportedOperationException();
}
this.solver.setObjectiveFunction(globalObj);
this.cspToSatEncoder.setObjectiveFunction(obj);
}
public void buildObjToMaximize(String id, TypeObjective type, XVarInteger[] list) {
int[] coeffs = new int[list.length];
Arrays.fill(coeffs, 1);
buildObjToMaximize(id, type, list, coeffs);
}
private ObjectiveFunction buildObjForVarSum(XVarInteger[] xlist,
int[] xcoeffs) {
IVecInt lits = new VecInt();
IVec<BigInteger> coeffs = new Vec<BigInteger>();
for(int i=0; i<xlist.length; ++i) {
ObjectiveFunction subObj = buildObjForVar(xlist[i]);
for(int j=0; j<subObj.getVars().size(); ++j) {
lits.push(subObj.getVars().get(j));
coeffs.push(subObj.getCoeffs().get(j).multiply(BigInteger.valueOf(xcoeffs[i])));
private String nValuesExpr(final XVarInteger[] list, final int[] coeffs) {
final StringBuffer sbuf = new StringBuffer();
boolean firstAddMember = true;
sbuf.append("add(");
for(int i=0; i<list.length; ++i) {
if(!firstAddMember) {
sbuf.append(',');
}
if(i == 0) {
sbuf.append('1');
firstAddMember = false;
continue;
}
final String normVar = coeffs[i] == 1 ? CtrBuilderUtils.normalizeCspVarName(list[i].id) : "mul("+CtrBuilderUtils.normalizeCspVarName(list[i].id)+","+coeffs[i]+")";
sbuf.append("if(and(");
boolean firstAndMember = true;
for(int j=0; j<i; ++j) {
if(!firstAndMember) {
sbuf.append(',');
firstAndMember = false;
}
final String normOtherVar = coeffs[j] == 1 ? CtrBuilderUtils.normalizeCspVarName(list[j].id) : "mul("+CtrBuilderUtils.normalizeCspVarName(list[j].id)+","+coeffs[j]+")";
sbuf.append("ne(").append(normVar).append(',').append(normOtherVar).append(')');
firstAndMember = false;
}
sbuf.append("),1,0)");
firstAddMember = false;
}
ObjectiveFunction globalObj = new ObjectiveFunction(lits, coeffs);
return globalObj;
sbuf.append(')');
return sbuf.toString();
}
private ObjectiveFunction buildObjForVarMax(XVarInteger[] xlist,
int[] xcoeffs) throws ContradictionException {
ObjectiveFunction[] varObjs = new ObjectiveFunction[xlist.length];
public void buildObjToMaximize(final String id, final TypeObjective type, final XVarInteger[] xlist, final int[] xcoeffs) {
buildObjToMinimize(id, type, xlist, xcoeffs);
this.cspToSatEncoder.getObjectiveFunction().negate();
}
private ObjectiveFunction buildLexObjToMinimize(final XVarInteger[] xlist, final int[] xcoeffs) {
long max = Long.MIN_VALUE;
long min = Long.MAX_VALUE;
for(int i=0; i<xlist.length; ++i) {
max = Math.max(max, ((XDomInteger) xlist[i].dom).getLastValue());
varObjs[i] = buildObjForVar(xlist[i]);
min = Math.min(max, ((XDomInteger) xlist[i].dom).getLastValue());
}
ObjectiveFunction finalObj = buildBoundObj(max);
for(ObjectiveFunction obj : varObjs) {
ObjectiveFunction boundCstrParams = buildBoundConstraintParams(obj,
finalObj);
this.solver.addAtLeast(boundCstrParams.getVars(), boundCstrParams.getCoeffs(), BigInteger.ZERO);
if(min < 0) throw new UnsupportedOperationException("negative coeff");
final ObjectiveFunction obj = new ObjectiveFunction();
final BigInteger step = BigInteger.valueOf(max+1);
BigInteger fact = BigInteger.ONE;
for(int i=xlist.length; i>=0; --i) {
obj.add(buildObjForVar(xlist[i]).multiply(fact));
fact = fact.multiply(step);
}
return finalObj;
return obj;
}
private ObjectiveFunction buildObjForVarMin(XVarInteger[] xlist,
int[] xcoeffs) throws ContradictionException {
ObjectiveFunction[] varObjs = new ObjectiveFunction[xlist.length];
long max = Long.MIN_VALUE;
for(int i=0; i<xlist.length; ++i) {
max = Math.max(max, ((XDomInteger) xlist[i].dom).getLastValue());
varObjs[i] = buildObjForVar(xlist[i]);
}
ObjectiveFunction finalObj = buildBoundObj(max);
for(ObjectiveFunction obj : varObjs) {
ObjectiveFunction boundCstrParams = buildBoundConstraintParams(obj,
finalObj);
this.solver.addAtMost(boundCstrParams.getVars(), boundCstrParams.getCoeffs(), BigInteger.ZERO);
private ObjectiveFunction buildExprObjToMinimize(String expr) {
return this.intensionEnc.encodeObj(expr);
}
private ObjectiveFunction buildSumObjToMinimize(final XVarInteger[] xlist, final int[] xcoeffs) {
final ObjectiveFunction obj = new ObjectiveFunction();
final int size = xlist.length;
for(int i=0; i<size; ++i) {
obj.add(buildObjForVar(xlist[i]).multiply(BigInteger.valueOf(xcoeffs[i])));
}
return finalObj;
return obj;
}
public void buildObjToMinimize(String id, TypeObjective type, XVarInteger[] list) {
final int[] coeffs = new int[list.length];
Arrays.fill(coeffs, 1);
buildObjToMinimize(id, type, list, coeffs);
}
private ObjectiveFunction buildBoundConstraintParams(
ObjectiveFunction varObj, ObjectiveFunction finalObj) {
IVec<BigInteger> objCoeffs = varObj.getCoeffs();
IVecInt cstrLits = new VecInt(objCoeffs.size() + finalObj.getVars().size());
IVec<BigInteger> cstrCoeffs = new Vec<>(objCoeffs.size() + finalObj.getVars().size());
finalObj.getVars().copyTo(cstrLits);
finalObj.getCoeffs().copyTo(cstrCoeffs);
varObj.getVars().copyTo(cstrLits);
for(int i=0; i<objCoeffs.size(); ++i) {
cstrCoeffs.push(objCoeffs.get(i).negate());
}
ObjectiveFunction boundCstrParams = new ObjectiveFunction(cstrLits, cstrCoeffs);
return boundCstrParams;
public void buildObjToMaximize(String id, TypeObjective type, XVarInteger[] list) {
final int[] coeffs = new int[list.length];
Arrays.fill(coeffs, 1);
buildObjToMaximize(id, type, list, coeffs);
}
private ObjectiveFunction buildBoundObj(long max) {
int nNewVars = 0;
while(max > 0) {
++nNewVars;
max >>= 1;
}
IVecInt maxVarLits = new VecInt(nNewVars);
IVec<BigInteger> maxVarCoeffs = new Vec<>(nNewVars);
BigInteger fact = BigInteger.ONE;
for(int i=0; i<nNewVars; ++i) {
maxVarLits.push(solver.nextFreeVarId(true));
maxVarCoeffs.push(fact);
fact = fact.shiftLeft(1);
}
ObjectiveFunction finalObj = new ObjectiveFunction(maxVarLits, maxVarCoeffs);
return finalObj;
public void buildObjToMinimize(String id, XNodeParent<XVarInteger> syntaxTreeRoot) {
buildExprObjToMinimize(CtrBuilderUtils.syntaxTreeRootToString(syntaxTreeRoot));
}
public void buildObjToMaximize(String id, XNodeParent<XVarInteger> syntaxTreeRoot) {
buildExprObjToMinimize(CtrBuilderUtils.syntaxTreeRootToString(syntaxTreeRoot));
this.cspToSatEncoder.getObjectiveFunction().negate();
}
}
......@@ -30,6 +30,7 @@ import org.sat4j.csp.Domains;
import org.sat4j.csp.Var;
import org.sat4j.csp.constraints3.CtrBuilderUtils;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.specs.ContradictionException;
import org.xcsp.parser.entries.XVariables.XVarInteger;
......@@ -138,4 +139,14 @@ public class CspToPBSolverDecorator implements ICspToSatEncoder {
return mapping;
}
@Override
public void setObjectiveFunction(final ObjectiveFunction obj) {
this.solver.setObjectiveFunction(obj);
}
@Override
public ObjectiveFunction getObjectiveFunction() {
return this.solver.getObjectiveFunction();
}
}
......@@ -20,10 +20,11 @@ package org.sat4j.csp.intension;
import java.util.Map;
import org.sat4j.pb.ObjectiveFunction;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
* A SAT solver with the ability to build a mapping between bollean variables and CSP variables.
* A SAT solver with the ability to build a mapping between boolean variables and CSP variables.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
......@@ -42,5 +43,9 @@ public interface ICspToSatEncoder {
void newCspVar(XVarInteger var, int minDom, int maxDom);
boolean addClause(int[] clause);
void setObjectiveFunction(ObjectiveFunction obj);
ObjectiveFunction getObjectiveFunction();
}
......@@ -18,6 +18,8 @@
*******************************************************************************/
package org.sat4j.csp.intension;
import org.sat4j.pb.ObjectiveFunction;
/**
* An interfacer to be implemented by classes able to encode intension constraints and store them in a solver.
*
......@@ -29,4 +31,6 @@ public interface IIntensionCtrEncoder {
public ICspToSatEncoder getSolver();
public ObjectiveFunction encodeObj(String expr);
}
......@@ -25,6 +25,8 @@ import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import org.sat4j.pb.ObjectiveFunction;
/**
* Encodes {@link IExpression} expressions into an {@link ICspToSatEncoder}.
* Given the expression, generates all nogoods and store them in the solver.
......@@ -367,4 +369,9 @@ public class NogoodBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
return this.solver;
}
@Override
public ObjectiveFunction encodeObj(String expr) {
throw new UnsupportedOperationException("use another intension constraint encoder");
}
}
......@@ -20,6 +20,7 @@ package org.sat4j.csp.intension;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
......@@ -27,6 +28,12 @@ import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
/**
* Encodes {@link IExpression} expressions into an {@link ICspToSatEncoder}.
* Encode the expression using a Tseiting-like encoding ; given all the values an expression may
......@@ -50,6 +57,21 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
final IExpression expression = parser.getExpression();
return encodeExpression(expression);
}
@Override
public ObjectiveFunction encodeObj(String expr) {
Parser parser = new Parser(expr);
parser.parse();
final IExpression expression = parser.getExpression();
Map<Integer, Integer> map = encodeWithTseitin(expression);
IVecInt vars = new VecInt(map.size());
IVec<BigInteger> coeffs = new Vec<BigInteger>(map.size());
for(Map.Entry<Integer, Integer> entry : map.entrySet()) {
vars.push(entry.getValue());
coeffs.push(BigInteger.valueOf(entry.getKey()));
}
return new ObjectiveFunction(vars, coeffs);
}
private boolean encodeExpression(IExpression expression) {
Map<Integer, Integer> map = encodeWithTseitin(expression);
......
package org.sat4j.csp.constraints3;
import java.util.List;
import org.junit.Before;
import org.junit.Test;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
import org.sat4j.reader.XMLCSP3Reader;
public class ObjBuilderTest {
private IPBSolver solver;
@Before
public void setUp() {
this.solver = SolverFactory.newDefault();
}
@Test
public void testMinimizeFunctionalForm() {
XMLCSP3Reader reader = new XMLCSP3Reader(solver);
String varSection = TestUtils.buildVariablesSection(TestUtils.buildBinaryVars(5));
String ctrSection = TestUtils.buildConstraintsSection(""
+ "<count>"
+ "<list> b0 b1 b2 b3 b4 </list>"
+ "<values> 1 </values>"
+ "<condition> (ge,1) </condition>"
+ "</count>", ""
+ "<count>"
+ "<list> b0 b1 b2 b3 b4 </list>"
+ "<values> 0 </values>"
+ "<condition> (ge,1) </condition>"
+ "</count>");
String optSection = TestUtils.buildObjectivesSection(""
+ "<minimize type=\"sum\">"
+ "<list> b0 b1 b2 b3 b4 </list>"
+ "</minimize>");
List<String> sortedModels = TestUtils.computeModels(reader, solver, varSection, ctrSection, optSection);
TestUtils.assertEqualsSortedModels(sortedModels, "0 0 0 0 1", "0 0 0 1 0", "0 0 1 0 0", "0 1 0 0 0", "1 0 0 0 0");
}
@Test
public void testMaximizeFunctionalForm() {
XMLCSP3Reader reader = new XMLCSP3Reader(solver);
String varSection = TestUtils.buildVariablesSection(TestUtils.buildBinaryVars(5));
String ctrSection = TestUtils.buildConstraintsSection(""
+ "<count>"
+ "<list> b0 b1 b2 b3 b4 </list>"
+ "<values> 1 </values>"
+ "<condition> (ge,1) </condition>"
+ "</count>", ""
+ "<count>"
+ "<list> b0 b1 b2 b3 b4 </list>"
+ "<values> 0 </values>"
+ "<condition> (ge,1) </condition>"
+ "</count>");
String optSection = TestUtils.buildObjectivesSection(""
+ "<maximize type=\"sum\">"
+ "<list> b0 b1 b2 b3 b4 </list>"
+ "</maximize>");
List<String> sortedModels = TestUtils.computeModels(reader, solver, varSection, ctrSection, optSection);
TestUtils.assertEqualsSortedModels(sortedModels, "0 1 1 1 1", "1 0 1 1 1", "1 1 0 1 1", "1 1 1 0 1", "1 1 1 1 0");
}
}
......@@ -6,6 +6,7 @@ import java.io.ByteArrayInputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.UnsupportedEncodingException;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.LinkedList;
......@@ -14,6 +15,7 @@ import java.util.SortedSet;
import java.util.TreeSet;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.XMLCSP3Reader;
import org.sat4j.specs.ContradictionException;
......@@ -53,9 +55,13 @@ public class TestUtils {
}
}
}
public static List<String> computeModels(XMLCSP3Reader reader, IPBSolver solver, String varSection, String ctrSection) {
String strInstance = TestUtils.buildInstance(varSection, ctrSection);
return TestUtils.computeModels(reader, solver, varSection, ctrSection, null);
}
public static List<String> computeModels(XMLCSP3Reader reader, IPBSolver solver, String varSection, String ctrSection, String objSection) {
String strInstance = TestUtils.buildInstance(varSection, ctrSection, objSection);
try {
reader.parseInstance(stringAsStream(strInstance));
} catch (ParseFormatException | IOException e) {
......@@ -63,26 +69,37 @@ public class TestUtils {
} catch (ContradictionException e) {
return new ArrayList<>();
}
List<String> sortedModels = TestUtils.getSortedStringModels(reader, solver);
List<String> sortedModels = TestUtils.getSortedStringModels(reader