1 of 33

Automatically Improving Constraint Models in Savile Row

Peter Nightingale, Ozgur Akgun, Ian Gent, Christopher Jefferson, Ian Miguel, Patrick Spracklen�School of Computer Science, Univ. of St Andrews, UK

1

Presented by Kumar Shivam for CSE 645: Seminar in Languages

2 of 33

Topics/Sections to be covered

  • Abstract and introduction to the paper
  • Contributions
  • Introducing Savile Row
  • Experimental results
  • Conclusion and future work
  • References

​

2

3 of 33

Abstract and Introduction to the paper

  • Modelling and formulation are vital and difficult task when solving combinatorial problem using Constraint Programming (CP) or Satisfiability (SAT).
  • The paper introduces a new algorithm, X-CSE to perform Associative-Commutative Common Subexpression Elimination (AC-CSE) in constraint problems.
  • The reformulation techniques are integrated in a single automated constraint modelling tool, called Savile Row.
  • Savile Row is used as an experimental testbed to evaluate each reformulation on a set of 50 problem classes.
  • SAT solver has a speedup of 2.15 times, and CP solver has a speedup of 5.96 times (geometric mean speedup, for instances taking 10 seconds to solve) when compared to tailored model without recommended reformulations.

3

4 of 33

Contributions of the paper

​

  • Evaluation of a range of reformulations for use in automated modelling. Contribution to new algorithms for Identical CSE and Active CSE that improve existing work.
  • A new algorithm, X-CSE, to perform AC-CSE. Application of X-CSE results in substantial gain in performance.
  • Reformulations described above can be reformulated in single automated modelling tool, Savile Row (SR). SR is used as an experimental testbed to evaluate each reformulation on a set of 50 problem classes with 596 instances in total.

4

5 of 33

Combinatorial Problem

  • Problems involving finding grouping, ordering, or assignment of discrete, finite set of objects that satisfies given conditions.
  • Eg; Planning, Scheduling, Sequencing

5

6 of 33

Constraint Programming

  • Paradigm for solving combinatorial problems, where constraints on feasible solutions for a set of decision variables are declaratively stated.
  • A Constraint satisfaction problem (CSP) on finite domain is defined as (X, D, C)
    • X = {x1, …, xn} is the set of variables of the problem
    • D = {D1, …, Dn} is the set of domain of the variables
    • C = {C1, …, Cm} is a set of constraints.

6

7 of 33

Satisfiability

​

  • The problem of determining if there exists an interpretation that satisfies a given boolean formula, ie., if the variables of a given boolean formula can be consistently replaced by the values TRUE or FALSE in a way so that the formula evaluates to TRUE.
  • Eg, (¬x ∨ y) ∧ (¬y ∨ z) is satisfiable if x = false, y = false, z = false

​

7

8 of 33

Common Subexpression Elimination (CSE)

  • Same expression appears in more than one place
    • x + y < 10 -> 1
    • x + y + z > 15 -> 2
    • Here, “x + y” can be replaced by an auxiliary variable, say, “aux1”, and the above expressions can be transformed to,
      • aux < 10
      • aux + z > 15
  • Associative-Commutative CSE are expressions containing associative and commutative operators such as +, -.

8

9 of 33

Ways of improving constraint models (Reformulations)

  • Domain Filtering
    • Removes values from variable domain that cannot take part in any solution
  • Variable Unification
    • Removes certain decision variables, replacement with constants
  • Simplification
    • Evaluation of constant expression, simplification of sum expression
  • Aggregation
    • Replacement of a set of constraint with a different formulation (eg, not-equal to allDifferent)
  • Extraction of common subsets (type of CSE)
    • Extraction of common subsets of terms, performing common subexpression elimination

9

10 of 33

Savile Row. Why the name?

  • Savile Row is a street in Mayfair, Central London.
  • Savile Row's reputation is built on bespoke tailoring, where each suit is made to individually fit.

10

11 of 33

Savile Row - Modelling Tool

  • Taking inspiration from the bespoke tailoring speciality of Savile Row tailors, the Savile Row Modelling tool, optimises and specialises a model for a particular solver.
  • The term tailoring was used by Andrea Rendl in the work, ‘Tailoring solver-independent constraint models: A case study with Essence and Minion.’

11

12 of 33

Savile Row - Architecture

  • Multi-pass term rewriting system.
  • Frontend reads a model in the Essence Prime language into an abstract syntax tree (AST).
  • Transformation of a model into input for a solver is the ‘tailoring process’.
  • Produces solver output for Minion, Minizinc etc

12

13 of 33

Savile Row - Tailoring Process

  • First steps of the tailoring process
    • Eg. Problem class parameters substitution, matrix comprehensions unrolling
  • Bounds of expressions
    • Estimation of lower and upper bound of value in numerical expression type
  • Simplifiers
    • Examining and re-writing an expression into semantically equivalent simpler expression
    • allDiff([1,3,4]) is rewritten as ‘true’
  • General Flattening
    • Extraction of inner expression ‘e’ to new auxiliary variable ‘a’ in a nested expression where nesting is not supported by the target solver (eg, sum containing a product).

13

14 of 33

X-CSE Algorithm for Associative Commutative CSE

(Abstract Syntax Tree - Recap)

  • Savile Row works on an abstract syntax tree.
  • Savile Row represents AC operators using non-binary trees as below (as per CP 2014)

​

14

15 of 33

X-CSE Algorithm for Associative Commutative CSE

  • X-CSE, a new algorithm to eliminate AC-CSEs.
  • Goal is to find common sets containing two or more expressions that are contained in more than one AC operator expression.

15

16 of 33

X-CSE Algorithm for Associative Commutative CSE

  • X-CSE algorithm uses a hash table map from pairs of expressions {a,b} to a list of AC expressions that both contain a and b.
  • Takes a reference to the AST representing all constraints, a reference to the Symbol Table and AC operator.

16

17 of 33

X-CSE Algorithm for Associative Commutative CSE

  • On line 3, the algorithm calls populateMapAC with the entire AST.
  • For all pair of expressions {e1, e2}, AST is added to the map[{e1,e2}].
  • A recursive call to the function with AST’s children is made.

17

18 of 33

X-CSE Algorithm for Associative Commutative CSE

  • On line 5, a pair is selected from the map according to a heuristic.
  • Lines 10-20 find an AC-CS and extract it from all relevant expressions.
  • A constraint is created on Line 14, to define the auxiliary variable.
  • Map is updated on line 19 and 20 to include all newly created expressions.

18

19 of 33

X-CSE comparison with Related Algorithms

  • X-CSE differs from the existing algorithms I-CSE (Identical CSE), since it can extract AC-CSs which are intersections of more than two expressions and AC-CSs containing auxiliary variables.
  • Eg: v + w + x + y = 0, v + w + x + z = 0, v + w + y + z = 0.
    • I-CSE would have a palette of three AC-CSs: v + w + x, v + w + y, and v + w + z. Only one of these will be chosen.
    • X-CSE would however first extract, v + w from all three sums:
      • a = v + w, a + x + y = 0, a + x + z = 0, a + y + z = 0
    • Second, X-CSE would extract one of a + x , a + y , a + z, which is not possible in I-CSE
      • a = v + w, b = a + x, b + y = 0, b + z = 0, a + y + z = 0

19

20 of 33

Reformulations in Savile Row - Identical CSE

  • First step, populateMap() collects only expressions that are candidates for CSE.
  • Second step, is to iterate through sets of expressions in decreasing size order.
  • For each set of identical expressions a new decision variable aux is created, and each of the expressions is replaced by aux.
  • Major difference between I-CSE and X-CSE is the re-population of map in line 13-14.

20

21 of 33

Reformulations in Savile Row - Identical CSE

  • For CP solver the geometric mean speed-up is 1.035, whereas for SAT solver the same statistic is 1.238.

21

22 of 33

Reformulations in Savile Row - X-CSE

Killer Sudoku

  • The standard Killer Sudoku is a 9 X 9 grid where each row and column are allDifferent, and the nine non-overlapping 3 X 3 subsquares are also allDifferent.
  • The experiment found 9 X 9 Killer Sudoku instances to very easy, so a 16 X 16 grid with 4 X 4 subsquares were used.
  • 100 instances were generated by first creating 100 random assignments to the 16 X 16 grid.
  • Traditional Killer Sudoku puzzles have exactly one solution. The random 16 X 16 instances may be unsatisfiable and may have multiple solutions.

22

23 of 33

Reformulations in Savile Row - X-CSE

Killer Sudoku

  • The sums in the clues are the only AC expressions and they do not overlap.
  • The sums overlap with allDifferent constraints. Each allDifferent constraint on a row, column or subsquare represents a permutation of {1…. 16}, with a sum of 136.
  • In the first tailoring process, the implied sum will be,

Σ X = 136, where X is the set of variables in the row, column or subsquare.

  • Savile automatically adds implied constraint as “allDifferent (x,y,z) with domain {1,3,5,7} as x + y + z >= 1 + 3 + 5 and x + y + z <= 3 + 5 + 7”
  • In the second tailoring process, some variables may be assigned and deleted, with the assigned value removed from other variables in the same row, column or subsquare. The implied sum for rows, columns and subsquares will be of the form

Σ X = c, but the constant c may differ

  • X-CSE then finds AC-CSs among rows, columns, subsquares and clues

​

23

24 of 33

Reformulations in Savile Row - X-CSE

Killer Sudoku

  • Without X-CSE 44 instances times out, with X-CSE 24 instances timed out in CP.
  • The geometric mean speedup was 9.72 for CP and 2.119 for SAT solver.

24

25 of 33

Reformulations in Savile Row - X-CSE

SONET Problem

25

26 of 33

Reformulations in Savile Row - X-CSE

SONET Problem

  • SONET, a network design problem, have each node connected to a set of rings.
  • It has the following parameters:
    • n, number of nodes
    • m, upper limit on the number of rings
    • r, maximum number of nodes per ring, ring capacity
    • A set of pairs that must be connected
  • The number of node-ring connections is minimised.

26

27 of 33

Reformulations in Savile Row - X-CSE

SONET Problem

  • Boolean matrix ‘rings’ indexed by [1…m, 1…n].
  • Rings[a,b] indicates whether ring a is connected to node b.
  • For each ring a,

​

​

  • The connected constraint between nodes b1 and b2 is expressed as a disjunction of sums:

​

  • The minimisation function is the sum of rings.
    • | rings[x,y]| is to be minimised, x in {1…m} and y in {1…n}
  • AC-CSs among connectedness constraints, the ring sum constraints and the minimisation sum.

27

28 of 33

Reformulations in Savile Row - X-CSE

SONET Problem

  • X-CSE improves solving speed, with a peak speed-up of 7.17 for CP, and upto 10.7 for SAT.

28

29 of 33

Summary plots for X-CSE

​

  • The geometric mean speed-up is 1.492 when using the CP solver, and 1.323 when using the SAT solver.

29

30 of 33

Conclusions

  • Introduction and description of X-CSE to perform Associative-Commutative CSE (AC-CSE) as an automated modelling step for finite domain constraint satisfaction problems.
  • X-CSE interacts with other reformulations, and thus enhancing the efficability of them, and X-CSE.
  • X-CSE is preferable over I-CSE because of its exploitation of frequently occurring short common subexpressions.
  • X-CSE outperforms I-CSE is most cases and is thus a valuable addition to the set of automated constraint modelling techniques.

30

31 of 33

Future Work

  • X-CSE and I-CSE improve formulation when the types of two expressions are the same. Examination of every pair of types in the language to look for overlapping expressions to be exploited is the first in the roadmap.
  • Second is to improve the generation of implied constraints that is input into the system. A generic algorithm to generate implied sums from any constraints with appropriate properties could be devised.

31

32 of 33

References

​

32

33 of 33

Thank you.

33