CODEWITHSUNDEEP
constraint-programming
alex137
alex137

Reputation: 178

Conditional Constraint Solving

How would you approach the following constraint optimization problem:

Edit: because I have a large (thousands) number of variables and constraints and performance is critical, I’m looking for a dedicated algorithm, not using a general-purpose constraint solver.

Upvotes: 0

Views: 289

Answers (2)

alex137
alex137

Reputation: 178

Actually, there is a fairly simple and efficient algorithm for this particular problem. It is enough to maintain and propagate intervals and start propagating the conditional constraints when the lower bounds become >= 2. At the end, if the interval is exactly [3,4], the optimal solution is to select 4.

More precisely:

  • initialize l[i]:=1, u[i]:=4
  • propagate constraints until fixpoint as follows:
    • Constraint "C<=x[i]": l[i]:=max(l[i],C)
    • Constraint "x[i]<=C": u[i]:=min(u[i],C)
    • Constraint "x[i]<=x[j]": l[j]:=max(l[j],l[i]) and u[i]:=min(u[i],u[j])
    • Constraint 2<=x[i] ==> 3<=x[j]: if 2<=l[i], then l[j]:=max(l[j], 3)
  • If u[i]<l[i], there is no solution
  • Otherwise, select:
    • x[i]=l[i] if u[i]<=3
    • x[i]=u[i] otherwise

This is correct and optimal because:

  • any solution is such that l[i]<=x[i]<=u[i], so if u[i]<l[i], there is no solution
  • otherwise, x[i]=l[i] is clearly a solution (but NOT x[i]=u[i] because it can be that u[i]>=2 but u[j] is not >=3)
  • bumping all x[i] from 3 to 4 when possible is still a solution because this change doesn't activate any new conditional constraints
  • what remains are the variables that are forced to be 3 (l[i]=u[i]=3), so we have found a solution with the minimal number of 3

In more details, here is a full proof:

  • assume that a solution x[i] is such that l[i]<=x[i]<=u[i] and let's prove that this invariant is preserved by application of any propagation rule:
    • Constraint "x[i]<=x[j]": x[i]<=x[j]<=u[j] and so x[i] is both <=u[i] and <=u[j] and hence <=min(u[i],u[j]). Similarly, l[i]<=x[i]<=x[j] so max(l[i],l[j])<=x[j]
    • The constraints "x[i]<=C" and "C<=x[i]" are similar
    • For the constraint "2<=x[i] ==> 3<=x[j]": either l[i]<2 and the propagation rule doesn't apply or 2<=l[i] and then 2<=l[i]<=x[i] implying 3<=x[j]. So 3<=x[j] and l[j]<=x[j] hence max(3,l[j])<=x[j]
  • as a result, when the fixpoint is reached and no rule can be applied anymore, if any i is such that u[i]<l[i], then there is no solution
  • otherwise, let's prove that this x[i] is a solution where: x[i]=l[i] if u[i]<=3 and x[i]=u[i] otherwise:
    • Note that x[i] is either l[i] or u[i], so l[i]<=x[i]<=u[i]
    • For all constraints "C<=x[i]", at fixpoint, we have l[i]=max(l[i],C), i.e., C<=l[i]<=x[i] and the constraint is satisfied
    • For all constraints "x[i]<=C", at fixpoint, we similarly have u[i]<=C and x[i]<=u[i]<=C and the constraint is satisfied
    • For all "x[i]<=x[j]", at fixpoint, we have: u[i] = min(u[i],u[j]) so u[i]<=u[j] and l[j] = max(l[j],l[i]), so l[i]<=l[j]. Then:
      • If u[j]<=3 then u[i]<=u[j]<=3 so x[i]=l[i]<=l[j]=x[j]
      • Otherwise, x[j]=u[j] and x[i]<=u[i]<=u[j]=x[j]
    • For all "2<=x[i] ==> 3<=x[j]": assume 2<=x[i]:
      • If u[i]<=3, then either:
        • l[i]<=2 and the fixpoint means l[j]:=max(l[j], 3) so 3<=l[j]<=x[j]
        • or l[i]=3 and 3=l[i]<=l[j]<=x[j]
      • If u[i]>3, then 3<u[i]<=u[j] and 3<u[i]<=u[j]=x[j]
  • Finally the solution is optimal because:
    • if l[i]=u[i]=3, any solution must have x[i]=3
    • otherwise, x[i] != 3: if u[i]<=3, then either u[i]=3 and x[i]=l[i]<3 or x[i]<=u[i]<3; and if u[i]>3 then x[i]=u[i]!=3

Upvotes: 0

Axel Kemper
Axel Kemper

Reputation: 11322

You could encode each variable as a pair of binary variables:

x[i] = 1 + 2*x2[i] + x1[i]

The inequality constraints can now be partly resolved:

1 <= x[i]   can be ignored, as always true for any variable
2 <= x[i]   implies (x2[i] or x1[i])
3 <= x[i]   implies x2[i]
4 <= x[i]   implies (x2[i] and x1[i])

1 >= x[i]   implies (!x2[i] and !x1[i])
2 >= x[i]   implies !x2[i]
3 >= x[i]   implies (!x2[i] or !x1[i])
4 >= x[i]   can be ignored, as always true for any variable

x[i] <= x[j] implies (!x2[i] or x2[j]) and 
                     (!x1[i] or x2[j] o x1[j]) and
                     (!x2[i] or !x1[i] or x1[j])

Conditional constraint

if 2 <= x[i] then 3 <= x[j]

translates to

x2[j] or !x1[i]

The encoding shown above can be directly written as Conjunctive Normal Form (CNF) suitable for a SAT solver. Tools like SATInterface or bc2cnf help to automate this translation.

To minimize the number of variables which have value 3, a counting circuit combined with a digital comparator could be constructed/modelled.

Variable x[i] has value 3, if (x2[i] and !x1[i]) is true. These expressions could be inputs of a counter. The counting result could then be compared to some value which is decreased until no more solutions can be found.

Bottom line:
The problem can be solved with a general purpose solver like a SAT solver (CaDiCal, Z3, Cryptominisat) or a constraint solver like Minizinc. I am not aware of a dedicated algorithm which would outperform the general purpose solvers.

Upvotes: 1

Related Questions