Commit 63801bd4 authored by sroussel's avatar sroussel

Added missing methods to encodings

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1727 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 334e1d17
......@@ -75,14 +75,18 @@ public class Binary extends EncodingStrategyAdapter {
final int p = (int) Math.ceil(Math.log(n) / Math.log(2));
final int k = (int) Math.pow(2, p) - n;
IVecInt clause = new VecInt();
String binary = "";
if (p == 0) {
return group;
}
int y[] = new int[p];
for (int i = 0; i < p; i++) {
y[i] = solver.nextFreeVarId(true);
}
IVecInt clause = new VecInt();
String binary = "";
for (int i = 0; i < k; i++) {
binary = Integer.toBinaryString(i);
while (binary.length() != p - 1) {
......@@ -182,4 +186,25 @@ public class Binary extends EncodingStrategyAdapter {
return group;
}
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
return group;
}
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
return group;
}
}
......@@ -97,4 +97,26 @@ public class Binomial extends EncodingStrategyAdapter {
return group;
}
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
return group;
}
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
return group;
}
}
......@@ -255,4 +255,26 @@ public class Commander extends EncodingStrategyAdapter {
return constrGroup;
}
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
return group;
}
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
return group;
}
}
......@@ -146,14 +146,20 @@ public class Ladder extends EncodingStrategyAdapter {
ConstrGroup group = new ConstrGroup(false);
final int n = literals.size();
IVecInt clause = new VecInt();
if (n == 1) {
clause.push(literals.get(0));
group.add(solver.addClause(clause));
return group;
}
int y[] = new int[n - 1];
for (int i = 0; i < n - 1; i++) {
y[i] = solver.nextFreeVarId(true);
}
IVecInt clause = new VecInt();
// Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
for (int i = 1; i <= n - 2; i++) {
clause.push(-y[i]);
......
......@@ -245,18 +245,6 @@ public class Product extends EncodingStrategyAdapter {
return result;
}
@Override
public IConstr addAtLeast(ISolver solver, IVecInt literals, int k)
throws ContradictionException {
IVecInt newLits = new VecInt();
for (int i = 0; i < literals.size(); i++) {
newLits.push(-literals.get(i));
}
return addAtMost(solver, newLits, literals.size() - k);
}
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
......
......@@ -68,6 +68,10 @@ public class Sequential extends EncodingStrategyAdapter {
ConstrGroup group = new ConstrGroup(false);
final int n = literals.size();
if (n == 1) {
return group;
}
int s[][] = new int[n - 1][k];
for (int j = 0; j < k; j++) {
for (int i = 0; i < n - 1; i++) {
......@@ -116,4 +120,32 @@ public class Sequential extends EncodingStrategyAdapter {
return group;
}
@Override
public IConstr addAtMostOne(ISolver solver, IVecInt literals)
throws ContradictionException {
return addAtMost(solver, literals, 1);
}
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
return group;
}
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup();
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
return group;
}
}
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