Commit f18406c8 authored by leberre's avatar leberre

Added support for PB constraints.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@490 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 7c83c2a5
......@@ -326,6 +326,27 @@ public class DependencyHelper<T, C> {
return new DisjunctionRHS<T, C>(this, literals);
}
/**
* Create a constraint stating that at most i domain object should be set to
* true.
*
* @param i
* the maximum number of domain object to set to true.
* @param things
* the domain objects.
* @return an object used to name the constraint. The constraint MUST BE
* NAMED.
* @throws ContradictionException
*/
public void atLeast(C name, int i, T... things)
throws ContradictionException {
IVecInt literals = new VecInt();
for (T t : things) {
literals.push(getIntValue(t));
}
descs.put(solver.addAtLeast(literals, i), name);
}
/**
* Create a constraint stating that at most i domain object should be set to
* true.
......@@ -349,6 +370,27 @@ public class DependencyHelper<T, C> {
return new ImplicationNamer<T, C>(this, toName);
}
/**
* Create a constraint stating that at most i domain object should be set to
* true.
*
* @param i
* the maximum number of domain object to set to true.
* @param things
* the domain objects.
* @return an object used to name the constraint. The constraint MUST BE
* NAMED.
* @throws ContradictionException
*/
public void atMost(C name, int i, T... things)
throws ContradictionException {
IVecInt literals = new VecInt();
for (T t : things) {
literals.push(getIntValue(t));
}
descs.put(solver.addAtMost(literals, i), name);
}
/**
* Create a clause (thing1 or thing 2 ... or thingn)
*
......@@ -496,6 +538,56 @@ public class DependencyHelper<T, C> {
objCoefs.push(weight);
}
/**
* Create a PB constraint of the form <code>
* w1.l1 + w2.l2 + ... wn.ln >= degree
* </code> where wi are position integers
* and li are domain objects.
*
* @param degree
* @param wobj
* @throws ContradictionException
*/
public void atLeast(C name, BigInteger degree, WeightedObject<T>... wobj)
throws ContradictionException {
IVecInt literals = new VecInt(wobj.length);
IVec<BigInteger> coeffs = new Vec<BigInteger>(wobj.length);
for (WeightedObject<T> wo : wobj) {
literals.push(getIntValue(wo.thing));
coeffs.push(wo.getWeight());
}
descs
.put(solver.addPseudoBoolean(literals, coeffs, true, degree),
name);
}
/**
* Create a PB constraint of the form <code>
* w1.l1 + w2.l2 + ... wn.ln <= degree
* </code> where wi are position integers
* and li are domain objects.
*
* @param degree
* @param wobj
* @throws ContradictionException
*/
public void atMost(C name, BigInteger degree, WeightedObject<T>... wobj)
throws ContradictionException {
IVecInt literals = new VecInt(wobj.length);
IVec<BigInteger> coeffs = new Vec<BigInteger>(wobj.length);
for (WeightedObject<T> wo : wobj) {
literals.push(getIntValue(wo.thing));
coeffs.push(wo.getWeight());
}
descs.put(solver.addPseudoBoolean(literals, coeffs, false, degree),
name);
}
public void atMost(C name, int degree, WeightedObject<T>... wobj)
throws ContradictionException {
atMost(name, BigInteger.valueOf(degree), wobj);
}
/**
* Stop the SAT solver that is looking for a solution. The solver will throw
* a TimeoutException.
......
Markdown is supported
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