Circuit Complexity and Decompositions of Global Constraints

1 Introduction

Global constraints are a vital component of constraint toolkits. They permit users to model common patterns and to exploit efficient propagation algorithms to reason about these patterns. A promising mechanism to implement such global constraints is to develop decompositions into sets of primitive constraints that do not hinder propagation. For example, Bacchus has shown how to decompose global propagators for the generic TABLE constraint, as well as for the REGULAR, AMONG and SEQUENCE constraints into conjunctive normal form (CNF) [Bacchus, 2007]. Such decompositions can then be used in SAT solvers, allowing us to profit from techniques like clause learning and backjumping. In recent years, many other decompositions have been proposed for a wide range of global constraints including REGULAR and GRAMMAR [Quimper and Walsh, 2006; 2007; 2008; Katsirelos et al., 2008], SEQUENCE [Brand et al., 2007], PRECEDENCE [Walsh, 2006], CARDPATH and SLIDE [Bessiere et al., 2008]. Many other global constraints can Toby Walsh†

∗Supported by the project ANR-06-BLAN-0383-02.

†NICTA is funded by the Australian Government through the Department of Broadband, Communications and the Digital Economy and the Australian Research Council.

NICTA and UNSW Sydney

toby.walsh@nicta.com.au

be decomposed using ROOTS and RANGE, which can themselves be propagated effectively using some simple decompositions [Bessiere et al., 2005; 2006a; 2006b]. Finally, many global constraints specified by automata can be decomposed into signature and transition constraints without hindering propagation [Beldiceanu et al., 2005].

This raises the important open question of which global constraints can be effectively propagated using simple encodings [Bessiere and Van Hentenryck, 2003]. We show that circuit complexity can be used to resolve this question. Our main result is that there is a polynomial sized decomposition of a constraint propagator into CNF if and only if the propagator can be computed by a polynomial size monotone Boolean circuit. It follows therefore that bounds on the size of monotone Boolean circuits give bounds on the size of decompositions of global constraints into CNF. For instance, a super-polynomial lower bound on the size of a Boolean circuit for perfect matching in a bipartite graph gives a super-polynomial lower bound on the size of a CNF decomposition of the domain consistency propagator for the ALLDIFFERENT constraint. Our results directly extend to decompositions into CSP constraints of bounded arity with domains given in extension since such decompositions can be translated into clauses of polynomial size [Bessiere et al., 2003]. The tools of circuit complexity are thus useful in understanding the limits of what we can achieve with decompositions.

2 Background

CSP. A constraint satisfaction problem (CSP) P consists of a set of variables X, each of which has a finite domain D(Xi), and a set of constraints C. An assignment to a variable Xi is a mapping of Xi to a value j ∈ D(Xi), called literal, and written Xi = j. We write D(X) (resp. D′ (X)) for sets of literals {Xi = j | Xi ∈ X∧ j ∈ D(Xi)} (resp. {Xi = j | Xi ∈ X∧j ∈ D′ (Xi)}) and P(D) for the set of all such sets. An assignment to a set of variables X is a set that contains exactly one assignment to each variable in X. A constraint C ∈ C has a scope, denoted scope(C) ⊆ X and allows a subset of the possible assignments to the variables scope(C), called solutions of C. A solution of P is an assignment of one value to each variable such that all constraints are satisfied.

A propagator for a constraint C is an algorithm which takes as input the domains of the variables in scope(C) and returns restrictions of these domains. Following [Schulte and Stuckey, 2004], we can formally define a propagation algorithm as a function:

Definition 1 (Propagator) A propagator f for a constraint C is a polynomial time computable function f : P(D) → P(D), such that f is monotone, i.e., D′ (X) ⊆ D(X) =⇒ f(D′ (X)) ⊆ f(D(X)), contracting, i.e., f(D(X)) ⊆ D(X), and idempotent, i.e., f(f(D(X))) = f(D(X)). If a literal Xi = j is inD(X)\f(D(X)) thenXi = j does not belong to any solution of C given D(X). If f detects that C has no solutions under D(X) then f(D(X)) = ∅.

A propagator detects dis-entailment if when no possible assignment is a solution of C then f(D(X)) = ∅. A propagator enforces domain consistency (DC) when Xi = j ∈ f(D(X)) implies that there exists a solution of C that contains Xi = j.

We also define the consistency checker for a constraint C as a function that returns 0 when it detects that no possible assignment is a solution of the constraint and 1 otherwise, rather than restricting domains.

Definition 2 (Consistency checker) A consistency checker f for a constraint C is a polynomial time computable function f : P(D) → {0, 1} such that f is monotone, i.e., D′ (X) ⊆ D(X) =⇒ f(D′ (X)) ≤ f(D(X)). If f(D(X)) = 0 then no possible assignment under D(X) is a solution of C.

We can obtain a polynomial time consistency checker fC of a constraint C from a polynomial time propagator fP for C and vice versa [Bessiere et al., 2007]. Given the propagator fP , the corresponding consistency checker fC is defined as:

Conversely, given fC, the propagator fP is

SAT. The Boolean satisfiability problem (SAT) is a special case of the CSP where variables are Boolean. For each Boolean variable xi there exist two literals xi and xi. Constraints in conjunctive normal form (CNF) are disjunctions of literals, called clauses and sometimes written simply as tuples of literals.

Unit propagation forces a literal to TRUE if it appears in a clause where all other literals are FALSE and continues until a fix-point is reached. If all literals in a clause are made FALSE, we say that the empty clause is produced. A stronger form of inference is the failed literal test [Freeman, 1995]. For each literal l of an unset variable x, the failed literal test sets l to TRUE, performs unit propagation, checks whether the empty clause was produced and retracts l and its consequences. If the empty clause was produced, l is set to FALSE.

A CSP instance can be encoded as a SAT instance. The most widely used mapping of CSP variables to Boolean variables is the direct encoding. Each CSP variable Xi with domain D(Xi) is encoded in SAT as a set of propositions xi,j, Xi ∈ X, j ∈ D(Xi) such that Xi ̸= j ⇐⇒ xi,j. The property that each CSP variable has at most one value is enforced by the set of clauses (xi,j , xi,k) for all k ∈ D(Xi), k ̸= j and the property that each CSP variable has at least one value is enforced by the set of clauses ∨j∈D(Xi) xi,j . We denote this propositional representation of D(X) as Dsat (X).

Note that the propositional representation Dsat (X) represents the current state of the domains D(X) during search. This means that when the domains change, we need to be able to make the corresponding change in the direct encoding. Consequently, the fact (Xi = j) ∈ D(X) is represented by xi,j being unset, rather than TRUE. When the value Xi = j is pruned, then xi,j is set to FALSE. Only when Xi = j is the only possible assignment for Xi is xi,j set to TRUE. This means that the same domain can be represented by different partial instantiations of the direct encoding. For example, given the CSP variable X1 with initial domain {1, 2, 3}, the instantiation Dsat ({X1}) = {x1,2, x1,3} (with x1,1 unset) corresponds to the same domain as Dsat ({X1}) = {x1,1, x1,2, x1,3}, which is D({X1}) = {X1 = 1}.

Boolean Circuits. ABoolean circuit S is a directed acyclic graph (DAG). Each source vertex of the DAG is an input gate and the unique sink of the DAG is the output gate. Each noninput vertex is labelled with a logical connective, such as and (∧), or (∨) and not (¬). An input b to the circuit is an assignment of a value 0 or 1 to each input gate. 1 The value of a non-input gate is computed by applying the connective that it is labelled with to the values of its ancestor gates. The value of the circuit S(b) is the value of its output gate.

Any polynomial time decision algorithm can be encoded as a Boolean circuit of polynomial size for a fixed length input [Papadimitriou and Steiglitz, 1982].

In this paper, we will use a restriction of Boolean circuits to ∧-gates and ∨-gates, called monotone circuits. The family of functions that are computable by monotone circuits is exactly all the monotone Boolean functions. Note that there exist families of polynomial time computable monotone Boolean functions such that the smallest monotone circuit that computes them is super-polynomial in size [Razborov, 1985].

Definition 3 (Monotone Boolean function) A Boolean function f is monotone iff f(b) = 0 implies f(b′ ) = 0 for all b′ ≤ b, where ≤ is the pairwise vector comparison, i.e., b′i ≤ bi for all i.

A consistency checker fC, previously defined as a monotone function over sets, can also be formalised as a monotone Boolean function whose input is the characteristic function of the set D(X). Literals Xi = j are mapped to arguments bi,j of the function, with bi,j = 1 iff Xi = j ∈ D(X). We use Db (X) to denote the setting of the bi,j inputs for a given set of domains D(X).

3 Properties of CNF decompositions

In this section, we define formally a CNF decomposition of a propagator and of a consistency checker. As with propagators and consistency checkers [Bessiere et al., 2007], we show that there exists a polynomial time conversion between the CNF decompositions of a propagator and of the corresponding consistency checker.

1 This is in contrast to TRUE and FALSE for SAT variables.

Definition 4 (CNF Decomposition of a propagator) A

CNF decomposition of a propagation algorithm fP is a formula in CNF CP over variables x ∪ y such that

• The input variables x are the propositional representation Dsat (X) of D(X) and y is a set of auxiliary variables whose size is polynomial in |x|.
• xi,j is set to FALSE by unit propagation if and only if Xi = j /∈ fP (D(X)).
• Unit propagation on CP produces the empty clause when fP (D(X)) = ∅.

Example 1 To illustrate Definition 4, consider a TABLE constraint over the variables X1,X2 with D(X1) = D(X2) = {a, b} and the satisfying assignments: {〈a, a〉 , 〈b, b〉 〈a, b〉}. [Bacchus, 2007] decomposes such a TABLE constraint into CNF using the following set of clauses:

where x = {xi,j}, i ∈ {1, 2}, j ∈ {a, b} is the propositional representation Dsat (X) of D(X) and y = {yi}, i ∈ {1, 2, 3} are auxiliary variables that correspond to satisfying tuples. Note that we have extended Bacchus's encoding with the clause (y1 ∨ y2 ∨ y3) to detect failure. Suppose the value a is removed from the domain of X1. The assignment x1a = FALSE forces the variable y1 to FALSE, which in turn causes the variable x2a to FALSE, removing the value a from the domain of X2 as well.

In example 1, we have decomposed a constraint into clauses by introducing variables. In general, an encoding might be exponentially bigger if auxiliary variables are not used (e.g., the parity function [Darwiche and Marquis, 2002]).

Definition 5 (CNF Decomposition of a consistency checker) A CNF decomposition of a consistency checker fC is a CNF CC over variables x ∪ y ∪ {z} such that

• The input variables x are the propositional representation Dsat (X) of D(X) and y is a set of auxiliary variables whose size is polynomial in |x|. The variable z is the output variable.
• Unit propagation on CC never forces any variable from x or generates the empty clause if no variable in y is set externally to CC, i.e., every variable y ∈ y is either unset or forced by a clause in CC.
• z is set to FALSE by unit propagation if and only if fC(D(X)) = 0.

Example 2 Consider the TABLE constraint from Example 1. We construct a CNF decomposition of a consistency checker using the CNF decomposition of a propagator. The clauses that cause pruning of input variables domains are removed and the last clause is augmented with the output variable z to avoid generation of the empty clause in the case of failure:

In this case, if the value a is removed from the domain of X1, unit propagation will not deduce that a has to be removed from the domain of X2. Consider instead the case when the values a and b are removed from the domains of X1 and X2, respectively. The literals x1a = FALSE and x2b = FALSE force the auxiliary variables y1, y2 and y3 to be FALSE. Therefore, the output variable z is forced to FALSE, signalling that the TABLE constraint does not have a solution under D(X).

In example 2, we transformed the propagator of example 1 into a consistency checker in an ad-hoc manner. The next theorem shows that this can be done in a generic way. We give a polynomial transformation of CNF decompositions of a propagator into consistency checkers This mirrors the results of [Bessiere et al., 2007] for CNF decompositions.

Theorem 1 There exists a polynomial time and space conversion between the CNF decomposition of a propagator fP and that of the corresponding consistency checker fC.

Proof: (→) We construct CC as a transformation of CP such that the output variable z of CC is FALSE iff unit propagation on CP produces the empty clause.

Let the set of clauses of CP be c1 . . . cm. For each variable p ∈ x∪y, we introduce 2 variables pt and pf in CC so that pt and pf are true if p is forced to TRUE or FALSE, respectively:

Then, we simulate unit propagation for each clause ck by replacing it with 3 implications 2 that contain the variables pt and pf rather than p. For example, to simulate unit propagation for the clause c1 = (p, q, r), we replace it with

Unit propagation on (4) can never derive the empty clause, because the true and false values of p are encoded in different variables pt and pf , which may be true simultaneously. When this happens, unit propagation on CP would generate the empty clause, therefore we must set the output variable z to FALSE, using the following clauses:

The union of the clauses (3), (4) and (5) is a CNF decomposition of fC with size O(|x∪y|+|CP |) = O(|CP |), therefore the transformation is polynomial.

(←) We outline the proof here. We replicate the equation (2) by simulating the failed literal test on CC∪{(z)}. For each literal xi,j we create a copy of CC, denoted by CC|xi,j , in which all literals xi,k, k ̸= j are FALSE. We use CC|xi,j to record the results of unit propagation when Xi = j. When unit propagation sets the output variable zxi,j of the copy CC|xi,j to FALSE then the propositional literal xi,j is made FALSE by the additional clause (zxi,j =⇒ xi,j).

2 We assume that formulas are given in 3-CNF form. We can convert any CNF formula to 3-CNF, increasing its size by at most a constant factor and without hindering unit propagation [Garey and Johnson, 1979, section 3.1.1].

The decomposition CP is then the union of the copies of CC and the clauses (zxi,j =⇒ xi,j):

The size of CP is O(|x| · |CC|), therefore the transformation is polynomial. ✷

Using the encoding of theorem 1, a CNF decomposition of a consistency checker that detects dis-entailment can be made into a propagator that enforces domain consistency. As an example, consider the CNF decomposition of a propagator that detects dis-entailment for the SEQUENCE constraint, proposed in [Bacchus, 2007]. The size of this decomposition is O(n2 ), where n is the number of variables in the SEQUENCE constraint. These variables are binary, hence the transformation of theorem 1 yields a decomposition of a DC propagator with size O(n3 ). This is also the complexity of the DC propagator proposed in [van Hoeve et al., 2006].

Since all definitions of CNF decompositions that we introduced in this section are polynomially equivalent, in the remainder of this paper we only prove results for CNF decompositions of consistency checkers.

4 Equivalence to monotone circuits

In this section, we show our main result, which establishes a connection between CNF decompositions of constraints and circuit complexity.

Theorem 2 A consistency checker fC can be decomposed to a CNF of polynomial size if and only if it can be computed by a monotone circuit of polynomial size.

The proof of theorem 2 is constructive. We will first show the reverse direction, using the Tseitin encoding [Tseitin, 1983] of a monotone circuit.

Definition 6 (Tseitin encoding of a Boolean circuit) The Tseitin encoding of a circuit S into clausal form has one propositional variable for each input of S and for each gate of S. W.l.o.g, we assume all gates have fan-in 2. For each ∧-gate g with inputs x1, x2, the Tseitin encoding contains the clauses (x1, g), (x2, g), (x1, x2, g) and for each ∨-gate it contains the clauses (x1, g), (x2, g), (x1, x2, g). Given any complete instantiation of the input variables, unit propagation on the Tseitin encoding sets the variable corresponding to the output gate of S to TRUE if the circuit computes 1 and to FALSE otherwise.

Suppose that a consistency checker fC can be encoded into a monotone circuit SC of polynomial size. The Tseitin encoding of SC turns out to be a CNF decomposition of fC. This is a direct consequence of the following lemma.

Lemma 1 Let SC be a monotone circuit and CC be its Tseitin encoding. Let I be a partial instantiation of the input variables x of CC and b be the corresponding input to SC, where bi = 0 iff xi ∈ I. Then, unit propagation on CC with I forces the output variable z to FALSE if and only if SC(b) = 0.

Proof: (→) This follows from the correctness of the Tseitin encoding.

(←). Suppose that SC(b) = 0, but the output variable z is not forced to FALSE by unit propagation under I. Consider an instantiation I ′ of the input variables of CC, which is the same as I with unset variables fixed to TRUE. Let y ∈ y ∪ {z} be an auxiliary variable that is unset under I. All such variables correspond to a gate in SC. Since CC is an encoding of the monotone circuit SC, y will be set to TRUE under I ′ . This means that the output variable z is also set to TRUE. By the correctness of the Tseitin encoding, SC(b) = 1, a contradiction. ✷

Corollary 1 Let SC be a monotone circuit and CC be its Tseitin encoding. Let I be a partial instantiation of the input variables x of CC. Then, unit propagation on CC with I forces the output variable z to FALSE if and only if SC(b) = 0, for all b where b is the input to SC that corresponds to any extension of I to a complete instantiation.

Proof: This follows from lemma 1 and the fact that SC is a monotone circuit. ✷

Interestingly, lemma 1 cannot be generalised to nonmonotone Boolean circuits. The next example shows that there exists a non-monotone Boolean circuit S that computes a monotone function, and a partial instantiation I with b the corresponding input to S, such that S(b) = 0 but unit propagation on the Tseitin encoding of S under the instantiation I does not set the output variable to FALSE.

Figure 1 A circuit whose Tseitin encoding is incomplete.

Example 3 Consider the non-monotone circuit S shown in figure 1. Note that S computes a monotone function.

The Tseitin encoding of S introduces three Boolean variables g1, g2 and g3 for the gates OR1, OR2 and AND3, respectively, and the clauses (x1, g1), (x2, g1), (g1, x1, x2), (x1, g2), (x2, g2), (g2, x1, x2), (g3, g1), (g3, g2), (g1, g2, g3).

Now suppose that I = {x1}. Then, b = {x1 = 0, x2 = 1} and S(b) = 0. Since S computes a monotone function, all possible extensions of x evaluate to 0. But in the Tseitin encoding, setting x1 to FALSE does not make any clauses unit, therefore unit propagation does not set g3 to FALSE. ✷

We now show the forward direction of theorem 2: every CNF decomposition CC of a consistency checker fC can be converted to a monotone circuit that computes fC with at most a polynomial increase in size.

This transformation exploits two properties of CNF decompositions, namely, that only positive literals of input variables appear in CC, and that unit propagation only makes auxiliary variables FALSE. We show the former property in lemma 2 and the latter in lemma 3.

Lemma 2 Let CC be the CNF decomposition of a consistency checker fC. There exists a polynomial size CNF decomposition C′C of fC such that negative literals of the input variables do not appear in any clause in C′C .

Proof: We construct C′C by removing from CC all clauses that contain a negative literal of an input variable. We show by contradiction that unit propagation on C′C and CC produces identical results for the output variable z.

Let I be a partial instantiation of the input variables such that unit propagation on CC under I sets z to FALSE but leaves z unset on C′C . Since unit propagation on CC and C′C produces different results, at least one of the removed clauses becomes unit under I in CC. By definition, CC never forces any literal of an input variable, so for any removed clause to become unit, all the literals of input variables in it have to be FALSE. Since at least one of these literals is negative, at least one input variable has to be set to TRUE in I.

We construct another partial instantiation I ′ from I by setting the same literals to FALSE as I and leaving the rest unset, i.e., I ′ = {xi,j|xi,j ∈ I}. The partial instantiations I and I ′ represent the same domains D(X), because the mapping from partial instantiation to domain depends only on the literals that are FALSE. By this and the fact that CC is a decomposition of fC, unit propagation on CC under I ′ forces the output variable z to the same value as under I, FALSE.

Consider the result of unit propagation on C′C under I ′ . Recall that by definition CC does not modify input variables and I ′ does not have literal set to TRUE by construction. Hence, none of the clauses that we remove from CC to get C′C can become unit after performing UP on CC under I ′ . Hence, unit propagation in C′C under I ′ sets z to FALSE as in CC. On the other hand, I sets a superset of the literals that I ′ sets, so unit propagation on C′C under I also sets z to FALSE, a contradiction, since we assumed that C′C leaves z unset under I. ✷

In practice, a CNF decomposition of a consistency checker may not be self contained and may depend on the existence of clauses in the direct encoding of variable domains. In this case, we cannot just remove clauses that contain negative literals of input variables, as lemma 2 suggests. However, using the clauses of the direct encoding, we can substitute negative literals with the disjunction of positive literals. For instance, consider a variable X2 with the domain {1, 2, 3} and a clause (x1,1, x2,2, y) in CC. The literal x2,2 can make this clause unit. The direct encoding of D(X2) includes a clause (x2,1, x2,2, x2,3). Note that the literal x2,2 is TRUE if and only if literals x2,1 and x2,3 are FALSE. Therefore, the literal x2,2 can be replaced with the disjunction (x2,1, x2,3) and the clause (x1,1, x2,2, y) is transformed to the clause (x1,1, x2,1, x2,3, y).

The next step is to show that we can transform a CNF decomposition so that each auxiliary variable is unset or FALSE for all inputs that make the output variable FALSE. The transformation is a renaming of the auxiliary variables. Lemma 3 describes the property that allows this transformation.

Lemma 3 Let CC be a CNF decomposition of a consistency checker fC over the variables x ∪ y ∪ {z}, I1 = Dsat 1 (X), I2 = Dsat 2 (X) be the propositional representations of any two domain settings such that unit propagation on CC forces z to FALSE under both I1 and I2. For any variable y ∈ y, if y is forced to FALSE (TRUE) by unit propagation under I1 then it is not forced to TRUE (FALSE) by unit propagation under I2.

Proof: Let a variable y be forced to TRUE by unit propagation under I1 and to FALSE under I2, but z is FALSE under both I1 and I2. Consider the partial instantiation I such that if a variable x ∈ x is FALSE in either I1 or I2, it is also FALSE in I, otherwise it is unset. Since I fixes a superset of the literals that are fixed in either I1 or I2, all clauses that became unit by either I1 or I2 will also be unit in I. Therefore, unit propagation under I will force at least the union of the sets of literals forced by I1 and I2. This means that unit propagation under I will make both y and y TRUE, which generates the empty clause. This is a contradiction, as CC can never produce the empty clause. ✷

Corollary 2 A CNF decomposition CC of a consistency checker fC over variables x ∪ y ∪ {z}, can be polynomially converted into a decomposition C′C of fC such that every variable in y is either unset or FALSE when z is FALSE.

Proof: We construct C′C from CC by flipping the polarity of those variables that are set to TRUE when z is FALSE. ✷

Lemma 2 and corollary 2 allow us to precisely characterize the form of the clauses in a CNF decomposition.

Corollary 3 Let CC be a CNF decomposition of a consistency checker fC. The variables of CC can be renamed so that each clause has exactly one negative literal.

Proof: By lemma 2, all input variables are positive literals in the decomposition and by definition 5 they are never forced by unit propagation on CC. In addition, by corollary 2, we can rename the auxiliary variables so that unit propagation on CC may only ever set them to FALSE. Then, in any clause that consists of input variables and one auxiliary variable y, y must be negative, otherwise it may be set to TRUE, a contradiction.

Suppose there exists a clause c with two auxiliary variables y1 and y2 and both are negative in c. Since neither y1 nor y2 can ever be made TRUE, this clause can never become unit and can be ignored. Suppose the literals of both y1 and y2 are positive in c. Then, if c becomes unit, it makes one of the auxiliary variables TRUE, a contradiction. Thus, exactly one of the literals of y1 and y2 is negative in c. The same reasoning can be extended to clauses with more than two auxiliary variables. ✷

The condition described by corollary 3 is similar to CC being re-nameable anti-Horn, but is stronger as it requires exactly one negative literal in each clause, rather than at most one. This condition allows us to build a monotone circuit from a decomposition, using the construction of the next lemma.

Lemma 4 Let CC be a CNF decomposition of a consistency checker fC. Then, there exists a monotone circuit SC of size O(n|CC|) that computes fC.

Proof: We assume that CC is in the form described in corollary 3.

The inputs of the circuit correspond to the input variables of CC. For each input variable xi,j of CC, there exists an input bi,j of SC which is 0 if xi,j is FALSE and 1 otherwise. Internal gates of the circuit correspond to auxiliary variables after a certain number of unit propagation steps, using the same mapping.

We create a circuit with |y| layers 1 . . . |y|. Let c1, . . . , cm be the clauses of CC. The ith layer of the circuit contains an ∨-gate cij for each clause cj , called clause gates and an ∧-gate yik for each auxiliary variable yk, called variable gates. Consider a clause cj which contains y as the sole negative literal (recall that corollary 3 ensures that this is the case), the positive literals of input variables xj1 , . . . , xjq and the positive literals of auxiliary variables yjq+1 , . . . , yjq+r . The inputs of each gate cij are bj1 , . . . , bjq and yi-1 jq+1 , . . . , yi-1 jq+r . Let the clauses with yk as the sole negative literal be ck1 , . . . , cks . Then, the inputs of each gate yik are cik1 , . . . , ciks . The output of the circuit is z|y| . Note that in this construction the inputs of some the gates may not be defined. This is the case, for example, for the gate c1i , where the clause ci contains the positive literals of some auxiliary variables. If this happens for a clause gate, we omit it, while if it happens for a variable gate, we omit the undefined input. If all the inputs of a variable gate are undefined, we omit the gate.

This construction computes one breadth first application of unit propagation at each layer. Specifically, the gate yik is 0 iff yk is forced to FALSE after i or fewer breadth first steps of unit propagation, while the gate cij is 0 iff the negated variable in cj is forced to FALSE after i or fewer breadth first steps of unit propagation. We show this by induction. For the first layer, there exist gates only for clauses with no positive literals of auxiliary variables. Consider any such gate cj which contains the negative literal yk. All the propositional variables in cj except yk are FALSE iff the corresponding inputs are 0. Thus c1j is 0 iff yk is FALSE after unit propagation of cj. If many clauses contain the negative literal yk, then at least one of them sets yk to FALSE in one breadth first step iff there exists a clause gate that is 0 and is an input to the variable gate y1 k , which is an ∧-gate and is thus 0. For the inductive step, assume that the layers 1 . . . k - 1 compute k - 1 breadth first steps of unit propagation. The same reasoning as for the base case shows that the results of unit propagation are correctly computed for the kth layer. Note that the kth layer may also contain gates that were omitted at previous levels. Since the inputs of these gates are correctly computed by the inductive hypothesis, the gates that are new to the kth layer are also correctly computed.

To conclude the proof, observe that in the extreme case, unit propagation will set one more literal at every breadth first step, thus after |y| steps it must either arrive at a fixpoint or set all literals. Since the circuit has |y| layers, it will correctly compute the result of unit propagation on CC. ✷

We illustrate the construction of lemma 4 with an example.

We construct a monotone circuit SC from CC, (figure 2). For a given instantiation of the input variables, this circuit computes 0 for the corresponding Boolean inputs if and only if unit propagation on CC forces the output variable to FALSE.

The circuit consists of 3 layers, with gates 1 and 2 in the first layer, 3-8 in the second and gate 9 in the third. The gates 1-6 and 9 are clause gates, while gates 7 and 8 are variable gates. A strict application of the construction of lemma 4 would also have variable gates in layers 1 and 3, but we omit them here as they would be single-input gates. Note that in figure 2, inputs are replicated at each layer to reduce clutter.

We note also that the layered construction of lemma 4 is necessary. A circuit that attempts to capture unit propagation on all clauses without using layers would have to contain a cycle between the gates that compute y1 and y2, because y1 would need to be an input of the clause gate c3 that computes y2 and y2 would need to an input of the clause gate c4 that computes y1. Constructing a layered circuit allows us to remove such cycles. ✷

The proof of theorem 2 is now immediate from lemmas 1 and 4. Since CNF decompositions of consistency checkers can be converted in polynomial time to and from CNF decompositions of propagators, theorem 2 also holds for propagators.

5 Non decomposable global constraints

Corollary 4 now uses an existing circuit complexity result to show that, unsurprisingly, there is no polynomial size CNF decomposition of the domain consistency propagator for the ALLDIFFERENT constraint. This also applies to generalizations of ALLDIFFERENT, such as GCC.

• Corollary 4 There is no polynomial sized CNF decomposition of the ALLDIFFERENT domain consistency propagator.

Proof: R´egin [R´egin, 1994] showed that an ALLDIFFERENT constraint has a solution iff the corresponding bipartite value graph (i.e., the graph where the node representing a variable has an edge to every node that represents a value in its domain) has a perfect matching. In addition, every bipartite graph corresponds to the value graph of an ALLDIFFERENT constraint and DC propagators detect dis-entailment. Thus, if there exists a polynomial size CNF decomposition of the ALLDIFFERENT DC propagator, we can construct a monotone circuit that computes whether a bipartite graph has a perfect matching. But Razborov [Razborov, 1985] showed that the smallest monotone circuit that computes whether there exists a perfect matching for a bipartite graph is superpolynomial in the number of vertices in the graph. Therefore, the smallest CNF decomposition of the ALLDIFFERENT DC propagator is super-polynomial in size. ✷

On the other hand, bound and range consistency propagators of ALLDIFFERENT can be decomposed, as we argue in [Bessiere et al., 2009].

6 Conclusions and FutureWork

In this paper we have shown how the tools of circuit complexity can be used to study decompositions of global propagators into CNF. Our results directly extend to decompositions into CSP constraints of bounded arity with domains given in extension since such decompositions can be translated into clauses of polynomial size. An interesting next step is to consider the decomposability of constraint propagators into more expressive primitive constraints where domains are represented in logarithmic space via their bounds. CSP solvers provide this feature which is missing in CNF. We conjecture that there exists an equivalence between such CSP decompositions of constraint propagators and monotone arithmetic circuits that are generalizations of Boolean monotone circuits to real numbers and gates for addition and multiplication. Since lower bound results on monotone circuits usually transfer to monotone arithmetic circuits, this would imply that the domain consistency propagator for ALLDIFFERENT cannot be decomposed to constraints that exploit (exponentially) large domains.