Skip to content

Commit

Permalink
CSP: Make use of linear expression builder
Browse files Browse the repository at this point in the history
  • Loading branch information
@Apfelbeet
Apfelbeet committed Nov 20, 2024
1 parent f7cd5e9 commit 6093cd7
Show file tree
Hide file tree
Showing 7 changed files with 33 additions and 91 deletions.
20 changes: 0 additions & 20 deletions csp/src/main/java/com/booleworks/logicng/csp/datastructures/LinearExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,17 +51,6 @@ public LinearExpression(final IntegerVariable v0) {
this(1, v0, 0);
}

/**
* Construct a linear expression from a map of variables and coefficients and a constant offset.
* @param coef the map of variables and coefficients
* @param b the constant offset
*/
public LinearExpression(final SortedMap<IntegerVariable, Integer> coef, final int b) {
this.coef = new TreeMap<>(coef);
this.coef.entrySet().removeIf(e -> e.getValue() == 0);
this.b = b;
}

/**
* Copy a linear expression from an existing linear expression.
* @param e the existing linear expression
Expand Down Expand Up @@ -362,15 +351,6 @@ public Builder(final LinearExpression e) {
expression = new LinearExpression(e);
}

/**
* Construct a builder from a map of variables and coefficients and a constant offset.
* @param coef the map of variables and coefficients
* @param b the constant offset
*/
public Builder(final SortedMap<IntegerVariable, Integer> coef, final int b) {
expression = new LinearExpression(coef, b);
}

/**
* Builds the linear expression. This invalidates this builder.
* @return the built linear expression
Expand Down
2 changes: 1 addition & 1 deletion csp/src/main/java/com/booleworks/logicng/csp/encodings/CompactOrderReduction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ private static ReductionResult adjustClauses(final Set<IntegerClause> clauses,
for (final Map.Entry<IntegerVariable, Integer> es : ls.getCoef().entrySet()) {
b += context.getOffset(es.getKey()) * es.getValue();
}
final LinearExpression newLs = new LinearExpression(ls.getCoef(), b);
final LinearExpression newLs = new LinearExpression.Builder(ls).setB(b).build();
final LinearLiteral newLl = new LinearLiteral(newLs, ll.getOperator());
newClause.addArithmeticLiteral(newLl);
} else if (lit instanceof ProductLiteral) {
Expand Down
14 changes: 4 additions & 10 deletions csp/src/main/java/com/booleworks/logicng/csp/encodings/OrderReduction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,6 @@
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;
import java.util.SortedMap;
import java.util.TreeMap;

/**
* A class grouping functions for reducing a problem for the order encoding.
Expand Down Expand Up @@ -187,20 +185,16 @@ private static Set<IntegerClause> reduceProductLiteralToLinearLE(final ProductLi
final LinearLiteral xgea =
new LinearLiteral(new LinearExpression(-1, sv, a + 1), LinearLiteral.Operator.LE);

final SortedMap<IntegerVariable, Integer> ls1Coefs = new TreeMap<>();
ls1Coefs.put(v, -1);
ls1Coefs.put(lv, a);
final LinearLiteral ls1 = new LinearLiteral(new LinearExpression(ls1Coefs, 0), LinearLiteral.Operator.LE);
final LinearExpression le1 = new LinearExpression.Builder(0).setA(-1, v).setA(a, lv).build();
final LinearLiteral ls1 = new LinearLiteral(le1, LinearLiteral.Operator.LE);
final IntegerClause.Builder cls1 = new IntegerClause.Builder();
cls1.addBooleanLiterals(boolLiterals);
cls1.addArithmeticLiterals(simpleLiterals);
cls1.addArithmeticLiterals(ls1, xlea, xgea);
ret.add(cls1.build());

final SortedMap<IntegerVariable, Integer> ls2Coefs = new TreeMap<>();
ls2Coefs.put(v, 1);
ls2Coefs.put(lv, -a);
final LinearLiteral ls2 = new LinearLiteral(new LinearExpression(ls2Coefs, 0), LinearLiteral.Operator.LE);
final LinearExpression le2 = new LinearExpression.Builder(0).setA(1, v).setA(-a, lv).build();
final LinearLiteral ls2 = new LinearLiteral(le2, LinearLiteral.Operator.LE);
final IntegerClause.Builder cls2 = new IntegerClause.Builder();
cls2.addBooleanLiterals(boolLiterals);
cls2.addArithmeticLiterals(simpleLiterals);
Expand Down
10 changes: 4 additions & 6 deletions csp/src/main/java/com/booleworks/logicng/csp/literals/LinearLiteral.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@
import com.booleworks.logicng.csp.terms.IntegerVariable;

import java.util.Set;
import java.util.SortedMap;
import java.util.TreeMap;

/**
* Represents a relation with a linear sum:
Expand Down Expand Up @@ -104,7 +102,7 @@ public boolean isUnsat() {

@Override
public LinearLiteral substitute(final IntegerVariableSubstitution assignment) {
final SortedMap<IntegerVariable, Integer> newCoefs = new TreeMap<>();
final LinearExpression.Builder le = new LinearExpression.Builder(sum.getB());
int replaced = 0;
for (final IntegerVariable key : sum.getCoef().keySet()) {
if (assignment.containsKey(key)) {
Expand All @@ -113,13 +111,13 @@ public LinearLiteral substitute(final IntegerVariableSubstitution assignment) {
return null;
}
++replaced;
newCoefs.put(assignment.get(key), sum.getCoef().get(key));
le.setA(sum.getCoef().get(key), assignment.get(key));
} else {
newCoefs.put(key, sum.getCoef().get(key));
le.setA(sum.getCoef().get(key), key);
}
}
if (replaced > 0) {
return new LinearLiteral(new LinearExpression(newCoefs, sum.getB()), op);
return new LinearLiteral(le.build(), op);
} else {
return this;
}
Expand Down
19 changes: 5 additions & 14 deletions csp/src/test/java/com/booleworks/logicng/csp/functions/CspDecompositionTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,6 @@

import java.util.Collections;
import java.util.List;
import java.util.SortedMap;
import java.util.TreeMap;

import static org.assertj.core.api.Assertions.assertThat;

Expand Down Expand Up @@ -70,24 +68,17 @@ public void testFormulas(final CspFactory cf) throws ParserException {
}

private static LinearLiteral lt(final int c0, final IntegerVariable a0) {
final SortedMap<IntegerVariable, Integer> coefs = new TreeMap<>();
coefs.put(a0, c0);
return new LinearLiteral(new LinearExpression(coefs, 0), LinearLiteral.Operator.EQ);
return new LinearLiteral(new LinearExpression(c0, a0, 0), LinearLiteral.Operator.EQ);
}

private static LinearLiteral lt(final int c0, final IntegerVariable a0, final int c1, final IntegerVariable a1) {
final SortedMap<IntegerVariable, Integer> coefs = new TreeMap<>();
coefs.put(a0, c0);
coefs.put(a1, c1);
return new LinearLiteral(new LinearExpression(coefs, 0), LinearLiteral.Operator.EQ);
final LinearExpression le = new LinearExpression.Builder(0).setA(c0, a0).setA(c1, a1).build();
return new LinearLiteral(le, LinearLiteral.Operator.EQ);
}

private static LinearLiteral lt(final int c0, final IntegerVariable a0, final int c1, final IntegerVariable a1,
final int c2, final IntegerVariable a2) {
final SortedMap<IntegerVariable, Integer> coefs = new TreeMap<>();
coefs.put(a0, c0);
coefs.put(a1, c1);
coefs.put(a2, c2);
return new LinearLiteral(new LinearExpression(coefs, 0), LinearLiteral.Operator.EQ);
final LinearExpression le = new LinearExpression.Builder(0).setA(c0, a0).setA(c1, a1).setA(c2, a2).build();
return new LinearLiteral(le, LinearLiteral.Operator.EQ);
}
}
44 changes: 15 additions & 29 deletions csp/src/test/java/com/booleworks/logicng/csp/predicates/AllDifferentPredicateTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,6 @@

import java.util.Collections;
import java.util.List;
import java.util.SortedMap;
import java.util.TreeMap;

import static org.assertj.core.api.Assertions.assertThat;

Expand Down Expand Up @@ -104,24 +102,12 @@ public void testDecomposition(final CspFactory cf) {
final CspPredicate.Decomposition pred2 = cf.allDifferent(List.of(a, b, c)).decompose(cf);
final CspPredicate.Decomposition pred3 = cf.allDifferent(List.of(a, b, c, d)).decompose(cf);

final SortedMap<IntegerVariable, Integer> coefsAB = new TreeMap<>();
final SortedMap<IntegerVariable, Integer> coefsAC = new TreeMap<>();
final SortedMap<IntegerVariable, Integer> coefsAD = new TreeMap<>();
final SortedMap<IntegerVariable, Integer> coefsBC = new TreeMap<>();
final SortedMap<IntegerVariable, Integer> coefsBD = new TreeMap<>();
final SortedMap<IntegerVariable, Integer> coefsCD = new TreeMap<>();
coefsAB.put(a, 1);
coefsAB.put(b, -1);
coefsAC.put(a, 1);
coefsAC.put(c, -1);
coefsAD.put(a, 1);
coefsAD.put(d, -1);
coefsBC.put(b, 1);
coefsBC.put(c, -1);
coefsBD.put(b, 1);
coefsBD.put(d, -1);
coefsCD.put(c, 1);
coefsCD.put(d, -1);
final LinearExpression leAB = new LinearExpression.Builder(0).setA(1, a).setA(-1, b).build();
final LinearExpression leAC = new LinearExpression.Builder(0).setA(1, a).setA(-1, c).build();
final LinearExpression leAD = new LinearExpression.Builder(0).setA(1, a).setA(-1, d).build();
final LinearExpression leBC = new LinearExpression.Builder(0).setA(1, b).setA(-1, c).build();
final LinearExpression leBD = new LinearExpression.Builder(0).setA(1, b).setA(-1, d).build();
final LinearExpression leCD = new LinearExpression.Builder(0).setA(1, c).setA(-1, d).build();

assertThat(pred0.getClauses()).isEmpty();
assertThat(pred1.getClauses()).hasSize(3);
Expand All @@ -134,9 +120,9 @@ public void testDecomposition(final CspFactory cf) {
assertThat(pred1.getAuxiliaryIntegerVariables()).isEmpty();
assertThat(pred2.getClauses()).hasSize(5);
assertThat(pred2.getClauses()).containsExactlyInAnyOrder(
new IntegerClause(new LinearLiteral(new LinearExpression(coefsAB, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsAC, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsBC, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leAB, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leAC, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leBC, LinearLiteral.Operator.NE)),
new IntegerClause(Collections.emptySet(), Common.setFrom(
new LinearLiteral(new LinearExpression(-1, a, 2), LinearLiteral.Operator.LE),
new LinearLiteral(new LinearExpression(-1, b, 2), LinearLiteral.Operator.LE),
Expand All @@ -152,12 +138,12 @@ public void testDecomposition(final CspFactory cf) {
assertThat(pred3.getClauses()).hasSize(7);
assertThat(pred3.getClauses()).containsExactlyInAnyOrder(
new IntegerClause(),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsAB, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsAC, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsAD, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsBC, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsBD, 0), LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(new LinearExpression(coefsCD, 0), LinearLiteral.Operator.NE))
new IntegerClause(new LinearLiteral(leAB, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leAC, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leAD, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leBC, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leBD, LinearLiteral.Operator.NE)),
new IntegerClause(new LinearLiteral(leCD, LinearLiteral.Operator.NE))
);
assertThat(pred3.getAuxiliaryBooleanVariables()).isEmpty();
assertThat(pred3.getAuxiliaryIntegerVariables()).isEmpty();
Expand Down
15 changes: 4 additions & 11 deletions csp/src/test/java/com/booleworks/logicng/csp/predicates/ComparisonPredicateTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,6 @@
import org.junit.jupiter.params.ParameterizedTest;
import org.junit.jupiter.params.provider.MethodSource;

import java.util.SortedMap;
import java.util.TreeMap;

import static org.assertj.core.api.Assertions.assertThat;

public class ComparisonPredicateTest extends ParameterizedCspTest {
Expand Down Expand Up @@ -157,11 +154,9 @@ public void testDecomposition(final CspFactory cf) {
assertThat(pred2.getAuxiliaryBooleanVariables()).isEmpty();
assertThat(pred2.getAuxiliaryIntegerVariables()).isEmpty();
assertThat(pred3.getClauses()).hasSize(1);
final SortedMap<IntegerVariable, Integer> coef3 = new TreeMap<>();
coef3.put(a, -1);
coef3.put(b, -1);
final LinearExpression le3 = new LinearExpression.Builder(19).setA(-1, a).setA(-1, b).build();
assertThat(pred3.getClauses().iterator().next()).isEqualTo(
new IntegerClause(new LinearLiteral(new LinearExpression(coef3, 19), LinearLiteral.Operator.LE)));
new IntegerClause(new LinearLiteral(le3, LinearLiteral.Operator.LE)));
assertThat(pred3.getAuxiliaryBooleanVariables()).isEmpty();
assertThat(pred3.getAuxiliaryIntegerVariables()).isEmpty();
assertThat(pred4.getClauses()).isEmpty();
Expand All @@ -171,11 +166,9 @@ public void testDecomposition(final CspFactory cf) {
assertThat(pred5.getAuxiliaryBooleanVariables()).isEmpty();
assertThat(pred5.getAuxiliaryIntegerVariables()).isEmpty();
assertThat(pred6.getClauses()).hasSize(1);
final SortedMap<IntegerVariable, Integer> coef6 = new TreeMap<>();
coef6.put(a, 1);
coef6.put(b, 1);
final LinearExpression le6 = new LinearExpression.Builder(-20).setA(1, a).setA(1, b).build();
assertThat(pred6.getClauses().iterator().next()).isEqualTo(
new IntegerClause(new LinearLiteral(new LinearExpression(coef6, -20), LinearLiteral.Operator.NE)));
new IntegerClause(new LinearLiteral(le6, LinearLiteral.Operator.NE)));
assertThat(pred6.getAuxiliaryBooleanVariables()).isEmpty();
assertThat(pred6.getAuxiliaryIntegerVariables()).isEmpty();
}
Expand Down

0 comments on commit 6093cd7

Please sign in to comment.