Reformulations of Constraint Satisfaction

Problems: A Survey

​

Huu-Phuc Vo

​

CSE 645

Presented by Ethan DeTurk

Constraint Programming

• Declarative
• Relations between variables are stated in the form of constraints
• Applications such as packing, airspace sectorisation, robotic task sequencing, doctor rostering, inference of haplotypes, scheduling and planning, vehicle routing, configuration, power and/or oil networks, and bioinformatics

Constraint Satisfaction Problems

A CSP is a combinatorial problem that is modelled as a finite set of variables, representing the objects the problem deals with, and a finite set of constraints, representing the relationships among the objects. It can be defined as a triple where

is a set of variables

is a set of domains containing the values that each variable may take

is a set of constraints

Each constraint c_i =

Constraint Satisfaction Problems: Continued

An assignment is a pair (x_i , a) that means variable x_i in X is assigned the value a in D (x_i )

A compound assignment is a set of assignments to distinct variables in X

A compound assignment satisfies a constraint <S_i , R_i> if the values assigned to variables in S_i satisfy R_i

A complete assignment is a compound assignment to all variables in X

A solution to a CSP is a complete assignment such that all constraints are satisfied

Example: Nurse Rostering Problem

A set of nurses need to be rostered from Monday to Sunday. For each day, each nurse is either on call, aiding an operation, aiding an appointment, or off work

Possible constraints:

• There must be exactly one nurse on call every day from Monday to Sunday
• The number of operations per workday (Mon-Fri) is at most two
• There are at least seven operations over the course of the week
• There are at least four appointments over the course of the week
• Each nurse has a shift type assigned for each day of the week

Example: Nurse Rostering Problem

Example: Nurse Rostering Problem

Comment: the table suggests a constraint that is not mentioned in the paper

Example: Nurse Rostering Problem

A set of nurses need to be rostered from Monday to Sunday. For each day, each nurse is either on call, aiding an operation, aiding an appointment, or off work

Possible constraints:

• There must be exactly one nurse on call every day from Monday to Sunday
• The number of operations per workday (Mon-Fri) is at most two
• There are at least seven operations over the course of the week
• There are at least four appointments over the course of the week
• Each nurse has a shift type assigned for each day of the week

Modeling the Nurse Rostering Problem in MiniZinc

set of int: Days = 1..7;

set of int: Mon2Fri = 1..5;

enum Nurses = {Nu_A, Nu_B, Nu_C, Nu_D, Nu_E};

enum ShiftTypes = {app, call, oper, none};

​

array[Nurses,Days] of var ShiftTypes: Roster;

​

constraint forall(d in Days)(count(Roster[Nurses,d],call) = 1);

constraint forall(w in Mon2Fri)(count(Roster[Nurses,w],oper) <= 2);

constraint count(Roster,oper) >= 7;

constraint count(Roster,app) >= 4;

constraint forall(N in Nurses)(regular(Roster[N,Days], "oper|none|app|call"));

solve satisfy;

​

Modeling the Nurse Rostering Problem in MiniZinc

set of int: Days = 1..7;

set of int: Mon2Fri = 1..5;

enum Nurses = {Nu_A, Nu_B, Nu_C, Nu_D, Nu_E};

enum ShiftTypes = {app, call, oper, none};

​

array[Nurses,Days] of var ShiftTypes: Roster;

​

constraint forall(d in Days)(count(Roster[Nurses,d],call) = 1);

constraint forall(w in Mon2Fri)(count(Roster[Nurses,w],oper) <= 2);

constraint count(Roster,oper) >= 7;

constraint count(Roster,app) >= 4;

constraint forall(N in Nurses)(regular(Roster[N,Days], "oper|none|app|call"));

solve satisfy;

​

Constraint Modeling

Figure 2 contrasts the paradigms of modelling and programming approaches. Solutions in a modeling approach may be obtained automatically from models, which are declaratively derived from specifications

Constraint Modeling

The general process of modeling and solving problems is using a modeling language to express models and pipelining the models to different solver languages

Modeling Language: MiniZinc

In the flattening process, a MiniZinc model is reformulated into a simplified model expressed in a subset of MiniZinc called FlatZinc. The constraints and expressions in this formulation look more similar to formal CSP definition

MiniZinc Example: Job Shop Problem

MiniZinc Example: Job Shop Problem

Loops are unrolled

MiniZinc Example: Job Shop Problem

Predicates are inlined

MiniZinc Example: Job Shop Problem

Disjunction split into two “reified” constraints

Subexpressions are flattened and intermediate variables are introduced

MiniZinc Example: Job Shop Problem

array [1..2] of int: X_INTRODUCED_6_ = [1,-1];

var 0..14: X_INTRODUCED_0_;

var 0..14: X_INTRODUCED_1_;

var 0..14: X_INTRODUCED_2_;

var 0..14: X_INTRODUCED_3_;

var 0..14: end:: output_var;

var bool: X_INTRODUCED_9_ ::var_is_introduced :: is_defined_var;

var bool: X_INTRODUCED_10_ ::var_is_introduced :: is_defined_var;

var bool: X_INTRODUCED_12_ ::var_is_introduced :: is_defined_var;

var bool: X_INTRODUCED_13_ ::var_is_introduced :: is_defined_var;

array [1..4] of var int: s:: output_array([1..2,1..2]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_];

constraint int_lin_le(X_INTRODUCED_6_,[X_INTRODUCED_0_,X_INTRODUCED_1_],-2);

constraint int_lin_le(X_INTRODUCED_6_,[X_INTRODUCED_1_,end],-5);

constraint array_bool_or([X_INTRODUCED_9_,X_INTRODUCED_10_],true);

constraint int_lin_le(X_INTRODUCED_6_,[X_INTRODUCED_2_,X_INTRODUCED_3_],-3);

constraint int_lin_le(X_INTRODUCED_6_,[X_INTRODUCED_3_,end],-4);

constraint array_bool_or([X_INTRODUCED_12_,X_INTRODUCED_13_],true);

constraint int_lin_le_reif(X_INTRODUCED_6_,[X_INTRODUCED_2_,X_INTRODUCED_0_],-3,X_INTRODUCED_9_):: defines_var(X_INTRODUCED_9_);

constraint int_lin_le_reif(X_INTRODUCED_6_,[X_INTRODUCED_0_,X_INTRODUCED_2_],-2,X_INTRODUCED_10_):: defines_var(X_INTRODUCED_10_);

constraint int_lin_le_reif(X_INTRODUCED_6_,[X_INTRODUCED_3_,X_INTRODUCED_1_],-4,X_INTRODUCED_12_):: defines_var(X_INTRODUCED_12_);

constraint int_lin_le_reif(X_INTRODUCED_6_,[X_INTRODUCED_1_,X_INTRODUCED_3_],-5,X_INTRODUCED_13_):: defines_var(X_INTRODUCED_13_);

solve minimize end;

Data file:

size = 2;

d = [|2,5|3,4|];

​

Categorization of CSP Reformulation

Three proposed types of reformulation:

• Type 1 - A model is reformulated to model’ within the same modeling language
• Type 2 - A model with non-CP standard types is compiled to another model with CP standard types
• Type 3 - A model is reformulated into SAT, MIP, MILP, or SMT

Type 1

A model is reformulated to model’, within the same modeling language

Examples:

• Symmetry breaking
• Implied constraints
• Precomputation
• Changing viewpoint

Symmetry Breaking

Solvers waste time visiting symmetric branches of the search space.

Constraints are added to eliminate symmetric solutions and speed up the search

Example: Social Golfers Problem

g*s golfers want to play in g groups of s slots each week, so that any two golfers play in the same group at most once, for w weeks

Example: Social Golfers Problem

Many symmetries

The weeks/rows can be permuted: there are 4! variable symmetries. The groups can be permuted within a week: there are 4!⁴ variable symmetries. The group slots can be permuted: there are 3!¹⁶ variable symmetries. The player names can be permuted: there are 12! value symmetries.

Symmetry breaking reformulation: switch from a 3D array of integer variables to a 2D array of set variables, which gets rid of 3!¹⁶ symmetries

Implied Constraints

Adding redundant constraints can reduce the search space without changing the set of solutions

Example: Car Sequencing Problem

A number of cars are being produced, each of which requires some subset of a set of customization options. The assembly line has a different station for each option, and station i can serve at most p_i out of any q_i consecutive cars in the assembly line. The task is to sequence the cars so that no station’s capacity is ever exceeded.

Example: Car Sequencing Problem

Explicit Constraint: no station can go over capacity

For n = 30, n₁ = 12, p₁ = 1, and q₁ = 2

Implied Constraint: In the first 28 cars of the sequence, there must be at least 11 that require option 1. Otherwise, the last two cars in the sequence would have to take option 1, which would put station 1 over capacity.

It follows that there must be at least 10 option 1 cars in the first 26 cars of the sequence, 9 option 1 cars in the first 24 cars of the sequence, etc.

Example: Car Sequencing Problem

Explicit Constraint: no station can go over capacity

Implied Constraint: no station can go under capacity for too long. Suppose that n_i of the n cars require option i. Since at most p_i of the last q_i consecutive cars can have option i, at least n_i - p_i of the cars that need option i must be in the first n - q_i cars of the sequence

For all k for which n - kq_i > 0 and n_i - kp_i > 0, at least n_i - kp_i of the cars that need option i must be in the first n - kq_i cars of the sequence

Reformulation by Precomputation

Another way to reformulate a model so that it can be solved more quickly is to precompute the possible solutions to a predicate or subproblem. Here is a toy example

Reformulation by Precomputation

This type of reformulation can be performed automatically. Dekker et al. [50] propose an extension to the MiniZinc toolchain that auto-tables annotated predicate definitions.

Reformulation by Changing Viewpoint

A viewpoint is the choice of variables and domains used to model a problem. For example, here are two different CSP representations of the n-queens problem:

The second viewpoint is more awkward and will usually take longer to solve. Sometimes a more efficient model of a problem can be found by looking for different viewpoints

Rossi et al. [127]

Type 2

A model with non-CP standard types is compiled to another model with CP standard types

Most solvers don’t support string and set constraints, so they have to be reformulated

Examples:

• Translation of string variables
• Translation of non-binary constraints to binary constraints

Reformulation of String Variables

In “MiniZinc with Strings,” Amadini et al. extend MiniZinc to include string variables of unknown length. During the flattening process, bounded-length string constraints (non-CP standard type) can be converted to integer constraints (CP standard type)

Reformulation of String Variables

[9] Amadini et al.

Reformulation of String Variables

[9] Amadini et al.

Reformulation to Binary Constraints

A CSP is binary iff for all of its constraints c_i = <S_i , R_i>, the arity of the relation R_i is 2 (this is the same as the cardinality of S_i ). Most of the attention on constraint satisfaction problems has been focused on binary CSPs because a non-binary CSP can always be converted to a binary one.

“On the Conversion between Non-Binary and Binary Constraint Satisfaction Problems” by Bacchus et al. presents two methods of converting non-binary CSPs to binary CSPs: the dual method and the hidden method

Reformulation to Binary Constraints: Dual Method

The constraints in the original problem become variables in the binary CSP known as c-variables. There is a binary constraint between every pair of c-variables sharing the same variable that prohibits them from assigning different values to that variable

[15] Bacchus et al.

Reformulation to Binary Constraints: Hidden Method

All of the variables of the original CSP remain, and an h-variable is added for each constraint. Binary constraints are added between an h-variable and an original variable iff the original variable is in the scope of the constraint corresponding to the h-variable

[15] Bacchus et al.

Reformulation to Binary Constraints: Hidden Method

An h-variable H_i for constraint <S_i , R_i> has a domain value corresponding to each tuple in R_i. For each variable X_j in S_i , the binary constraint between X_j and H_i allows to take a particular value iff X_j takes the value defined in the tuple corresponding to the value of H_i .

[15] Bacchus et al.

Type 3

A model is reformulated into SAT, MIP, MILP, or SMT.

General-purpose solvers may have to do this. For example, Simply and WSimply solve CSPs by reformulating them to SMT - [138] Palahi et al.

​

Reformulation to SAT

There are several ways to encode a CSP as an instance of SAT:

• Direct encoding
• One propositional variable per domain value per CSP variable
• Uses conflict clauses
• Support encoding
• Same variables as the direct encoding
• Uses support clauses (given a binary constraint, an assignment to one variable implies the possible values of the other)
• Log encoding
• …

Direct and Support Encodings Example

A’s domain is {0, 1}

B’s domain is {0, 1, 2}

​

Reformulation to MILP and SMT

MILP:

• Linear arithmetic constraints can be translated directly
• Other types of constraints must be linearized

SMT:

• Depending on the theory, many variable definitions and constraints can be translated directly
• Some constraints must be reformulated, for example:

[138] Palahi et al.

References

This is a presentation of “Reformulations of Constraint Satisfaction Problems: A Survey” by Huu-Phuc Vo. Footnotes in the presentation follow the same numbering scheme as the paper:

9. Amadini, R., Flener, P., Pearson, J., Scott, J.D., Stuckey, P.J., Tack, G.: MiniZinc with strings. In: Hermenegildo, M., López-García, P. (eds.) LOPSTR 2016: Revised Selected Papers. pp. 59–75. No. 10184 in LNCS, Springer (2017)

15. Bacchus, F., Van Beek, P.: On the conversion between non-binary and binary constraint satisfaction problems. In: AAAI/IAAI. pp. 310–318 (1998)

127. Rossi, F., Van Beek, P., Walsh, T.: Handbook of constraint programming. Elsevier (2006)

138. Palahí i Sitges, M., et al.: Reformulation of constraint models into SMT. Ph.D. thesis, Universitat de Girona (2015)

​