Fix CAD filtering

paultristanwagner · Mar 6, 2024 · 4355677 · 4355677
1 parent 7dc927b
commit 4355677
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 13 deletions.
diff --git a/src/main/java/me/paultristanwagner/satchecking/theory/nonlinear/CAD.java b/src/main/java/me/paultristanwagner/satchecking/theory/nonlinear/CAD.java
@@ -44,7 +44,8 @@ public Set<Cell> compute(
       String previousVariable = variableOrdering.get(r);
 
       // todo: highestVariable could cause errors
-      p.get(r + 1).removeIf(poly -> !poly.highestVariable().equals(previousVariable));
+      List<String> finalVariableOrdering = variableOrdering;
+      p.get(r + 1).removeIf(poly -> !poly.highestVariable(finalVariableOrdering).equals(previousVariable));
     }
 
     // phase 2: lifting

diff --git a/src/main/java/me/paultristanwagner/satchecking/theory/nonlinear/MultivariatePolynomial.java b/src/main/java/me/paultristanwagner/satchecking/theory/nonlinear/MultivariatePolynomial.java
@@ -45,18 +45,32 @@ public static MultivariatePolynomial ZERO() {
     return multivariatePolynomial(new HashMap<>(), new ArrayList<>());
   }
 
-  public String highestVariable() {
+  public String highestVariable(List<String> variableOrdering) {
     if (this.variables.isEmpty()) {
       throw new IllegalStateException("There are no variables");
     }
 
-    int highestVariableIndex = 0;
+    int highestVariableOrderingIndex = -1;
     for (Exponent exponent : coefficients.keySet()) {
-      int variableIndex = exponent.highestNonZeroIndex();
-      highestVariableIndex = Math.max(highestVariableIndex, variableIndex);
+      if (coefficients.get(exponent).isZero()) {
+        continue;
+      }
+
+      for (int r = variableOrdering.size() - 1; r >= 0; r--) {
+        String variable = variableOrdering.get(r);
+        int variableIndex = this.variables.indexOf(variable);
+
+        if (variableIndex == -1) {
+          continue;
+        }
+
+        if (exponent.get(variableIndex) != 0 && (highestVariableOrderingIndex == -1 || r > highestVariableOrderingIndex)) {
+          highestVariableOrderingIndex = r;
+        }
+      }
     }
 
-    return variables.get(highestVariableIndex);
+    return variables.get(variables.indexOf(variableOrdering.get(highestVariableOrderingIndex)));
   }
 
   public int degree(String variable) {
@@ -174,7 +188,8 @@ public MultivariatePolynomial multiply(MultivariatePolynomial other) {
   public MultivariatePolynomial pow(int exponent) {
     if (exponent < 0) {
       if (this.isConstant()) {
-        Number c = this.coefficients.getOrDefault(getLeadMonomial(), Number.ZERO());
+        Exponent constantExponent = constantExponent(variables.size());
+        Number c = this.coefficients.getOrDefault(constantExponent, Number.ZERO());
         return constant(c.pow(-exponent));
       }
 
@@ -193,12 +208,12 @@ public MultivariatePolynomial pow(int exponent) {
     return result;
   }
 
-  public Exponent getLeadMonomial() {
+  public Exponent getLeadMonomial(List<String> variableOrdering) {
     if (this.variables.isEmpty()) {
       return constantExponent(0);
     }
 
-    return getLeadMonomial(highestVariable());
+    return getLeadMonomial(highestVariable(variableOrdering));
   }
 
   public Exponent getLeadMonomial(String variable) {

diff --git a/...in/java/me/paultristanwagner/satchecking/theory/solver/NonLinearRealArithmeticSolver.java b/...in/java/me/paultristanwagner/satchecking/theory/solver/NonLinearRealArithmeticSolver.java
@@ -4,14 +4,14 @@
 import me.paultristanwagner.satchecking.theory.TheoryResult;
 import me.paultristanwagner.satchecking.theory.nonlinear.*;
 import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.MultivariateMaximizationConstraint;
+import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.MultivariateMinimizationConstraint;
 import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.MultivariateOptimizationConstraint;
 import org.apache.commons.lang3.tuple.Pair;
 
 import java.util.*;
 
 import static me.paultristanwagner.satchecking.theory.TheoryResult.satisfiable;
 import static me.paultristanwagner.satchecking.theory.TheoryResult.unsatisfiable;
-import static me.paultristanwagner.satchecking.theory.nonlinear.Interval.IntervalBoundType.CLOSED;
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomial.variable;
 
 public class NonLinearRealArithmeticSolver implements TheorySolver<MultivariatePolynomialConstraint> {
@@ -59,7 +59,7 @@ public TheoryResult<MultivariatePolynomialConstraint> solve() {
     // if we have an optimization objective, we need to add a fresh variable and fix the variable ordering
     List<String> variableOrdering = null;
     String freshVariableName = null;
-    if(objective != null) {
+    if (objective != null) {
       freshVariableName = freshVariableName(variablesSet);
       MultivariatePolynomial freshVariable = variable(freshVariableName);
       MultivariatePolynomialConstraint helper = MultivariatePolynomialConstraint.equals(freshVariable, objective.getObjective());
@@ -85,7 +85,7 @@ public TheoryResult<MultivariatePolynomialConstraint> solve() {
     if (objective != null) {
       Comparator<Interval> comparator;
 
-      if(objective instanceof MultivariateMaximizationConstraint) {
+      if (objective instanceof MultivariateMaximizationConstraint) {
         comparator = new Interval.LowerBoundIntervalComparator().reversed();
       } else {
         comparator = new Interval.LowerBoundIntervalComparator();
@@ -113,7 +113,12 @@ public TheoryResult<MultivariatePolynomialConstraint> solve() {
           variableAssignment.remove(freshVariableName);
 
           Interval targetInterval = cell.getIntervals().get(0);
-          if (targetInterval.getLowerBoundType() != CLOSED) {
+
+          boolean unboundedInDirection =
+              (objective instanceof MultivariateMaximizationConstraint && targetInterval.getUpperBoundType() != Interval.IntervalBoundType.CLOSED) ||
+                  (objective instanceof MultivariateMinimizationConstraint && targetInterval.getLowerBoundType() != Interval.IntervalBoundType.CLOSED);
+
+          if (unboundedInDirection) {
             return unsatisfiable(constraints);
           } else {
             return satisfiable(new VariableAssignment(variableAssignment));