---
title: "Variable Elimination in Binary CSPs (Extended Abstract)"
authors:
  - "Martin C. Cooper"
  - "Achref El Mouelhi"
  - "Cyril Terrioux"
doi: "10.24963/ijcai.2020/702"
url: "https://ijcai.org/proceedings/2020/702"
pdf: "https://ijcai.org/proceedings/2020/0702.pdf"
venue: "Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence"
year: 2020
pages: "5035-5039"
track: "Journal track"
keywords:
  - "Constraints and SAT: Constraint Satisfaction"
---

# Variable Elimination in Binary CSPs (Extended Abstract)

Martin C. Cooper, Achref El Mouelhi, Cyril Terrioux

*Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence*, pages 5035-5039. DOI: [10.24963/ijcai.2020/702](https://doi.org/10.24963/ijcai.2020/702)

## Abstract

We investigate rules which allow variable elimination in binary CSP (constraint satisfaction problem) instances while conserving satisfiability. We propose new rules and compare them, both theoretically and experimentally. We give optimised algorithms to apply these rules and show that each defines a novel tractable class. Using our variable-elimination rules in preprocessing allowed us to solve more benchmark problems than without.

## Full text

## 1 Introduction

Constraint satisfaction provides a generic model for many NP-hard problems encountered in fields such as artificial intelligence, bioinformatics and operations research. In this paper, we study binary CSP instances, in which each constraint concerns at most two variables. Since the binary CSP is NPcomplete, it is of practical interest to find polynomial-time operations which reduce the size of the search space. One obvious way to reduce search space size is by variable elimination.

Variable elimination is classic in those families of constraint problems in which variables can be eliminated without changing the nature of the constraints: we can cite Gaussian elimination in systems of linear equations over a field [Schrijver, 1999] or variable-elimination resolution in boolean formulae in CNF [Subbarayan and Pradhan, 2004]. Indeed, any variable xi can be eliminated from a general-arity CSP instance by joining all constraints whose scope includes xi and projecting the resulting relation R with scope Y onto the variables Y \ {xi} [Dechter, 1999; Larrosa and Dechter, 2003]. Call this relation R-xi . Unfortunately, this often introduces a high-arity constraint and this can be counterproductive in terms of both memory and time. Under certain conditions, a binary CSP instance will remain binary after this joinand-project variable elimination of xi. For example, this is clearly the case if xi is constrained by only two other variables since, in this case, R-xi is binary. A more interesting case is when all constraints with xi in their scope share a majority polymorphism since, in this case, the relation R-xi is equivalent to the join of its binary projections [Jeavons et al., 1998]. Fourier's algorithm for variable elimination applied to a system of binary linear inequalities [Koubarakis, 2006; Schrijver, 1999] can be viewed as just one example of this general rule, since binary linear inequalities are all closed under the majority polymorphism median. Another interesting case is when there is a functional constraint of the form xi = f(xj) (where f is a function) for some other variable xj: the relation R-xi is then equivalent to the join of its projections onto the pairs of variables (xj , xk) (k ̸= i, j) [Zhang and Yap, 2011].

∗This paper is an extended abstract of [Cooper et al., JAIR, 2019]

†Contact Author

Unfortunately, the introduction of a large number of new constraints, even if they are still binary, may again be counterproductive. Therefore, we concentrate in this paper on rules which do not introduce new constraints when a variable is eliminated.

Various rules have been found which allow the elimination of a variable without introducing new constraints and without changing the satisfiability of the instance [Cohen et al., 2015; Cooper, 2014; Cooper et al., 2010]. Such rules were used, for example, in the deep optimisation solution to the spectrum repacking problem [Newman et al., 2018]. Discovery of new variable-elimination rules may have not only practical but also theoretical applications. For example, simple rules for variable or value elimination are used by Beigel and Eppstein (1995) in their algorithms with low worst-case time bounds for such NP-complete problems as 3-COLOURING and 3SAT: these simplification operations are an essential first step before the use of decompositions into subproblems with smaller domains. In the theory of fixed-parameter tractability, variable elimination is often an essential ingredient of polynomial kernalisation algorithms. For example, in the Point Line Cover problem (find k straight lines which cover n points), if at least k + 1 points lie on a line, then they can be effectively eliminated since they must be covered by this line [Kratsch et al., 2016].

We study the following generic NP-hard problem.

Definition 1 A binary CSP instance I = 〈X,D,R〉 comprises

- a set X of n variables x1, . . . , xn,
- a domain D(xi) for each variable xi (i = 1, . . . , n), and
- a binary constraint relation Rij for each pair of distinct variables xi,xj (i,j∈{1, . . . , n}).

For notational convenience, we assume that there is exactly one binary relation Rij for each pair of variables. We say that xi constrains xj if Rij is different fromD(xi) ×D(xj), and we use e to denote the number of pairs of variables {xi, xj} such that xi constrains xj. An assignment 〈v1, . . . , vm〉 to variables 〈xi1 , . . . , xim 〉 is consistent if vj ∈ D(xij ) (for j = 1, . . . ,m) and (vj, vk) ∈ Rij,ik (for all j, k such that 1 ≤ j &lt; k ≤ m). A solution to I is a consistent assignment to all variables in X.

We can associate a binary CSP instance with its microstructure, a labelled graph whose vertices are the variablevalue assignments and which has positive and negative edges. If (vi, vj) ∈ Rij, we say that the assignments 〈xi, vi〉, 〈xj, vj〉 (or more simply vi, vj) are compatible and that vivj is a positive edge, otherwise vi, vj are incompatible and vivj is a negative edge. In figures, broken lines represent negative edges (incompatible pairs) and solid lines represent positive edges (compatible pairs). For simplicity of notation we can assume that variable domains are disjoint, so that using vi as a shorthand for 〈xi, vi〉 is unambiguous. We say that vi ∈ D(xi) has a support at variable xj if there exists vj ∈ D(xj) such that vivj is a positive edge. A binary CSP instance I is arc consistent if for all pairs of distinct variables xi, xj, each vi ∈ D(xi) has a support at xj. Arc consistency is ubiquitous in constraint solvers: it is applied both before and during search in binary CSPs since it can be established in O(ed2 ) time, where e is the number of binary constraints and d the maximum domain size [Bessi`ere et al., 2005].

All proofs of results given in this extended abstract can be found in the full version of the paper [Cooper et al., 2019], together with details of the experimental trials.

## 2 Variable-Elimination Rules

We study conditions under which a variable xi can be eliminated from a binary CSP instance while conserving satisfiability. A simple example of such a condition is that there exists a value vi ∈ D(xi) which is compatible with all assignments to all other variables. Clearly any solution s to the instance I ′ obtained by eliminating xi can be extended to a solution to the original instance I by setting s(xi) = vi. Another simple example is that the variable xi has a singleton domain {vi}. This second example demonstrates that when eliminating the variable xi we need to retain the projections onto X \ {xi} of all constraints whose scope includes xi, since in this example we must first eliminate from all domains D(xj) (j ̸= i) those values that are not compatible with 〈xi, vi〉. Thus, the instance I ′ obtained by eliminating a variable xi from a binary CSP instance I is identical to I except that (1) ∀j ̸= i, we have deleted from D(xj) all values vj such that 〈xj, vj〉 has no support at xi in I, and (2) we have deleted the variable xi and all constraints with xi in their scope.

We require the following formal definition in order to study provably-correct variable-elimination rules [Cohen et al., 2015].

Definition 2 A satisfiability-conserving variable-elimination condition (or a var-elim condition) is a polytime-computable property P(xi) of a variable xi in a binary CSP instance I

Figure 1: The DE-snake property: for some value vi ∈ D(xi), for each value vj incompatible with vi, there is a value v′j such that (1) v′j is compatible with vi, and (2) v′j is compatible with all assignments vk to a third variable xk which are compatible with vj .

![Image](https://ijcai.org/proceedings/2020/fulltext/702/image_000000_2e9cd1b744f0450f4e9c37946b9fac39a2c33a04edb31ca7cec958babf945b92.png)

such that when P(xi) holds the instance I ′ obtained from I by eliminating xi is satisfiable if and only if I is satisfiable. Such a property P(xi) is a solution-conserving variableelimination condition (sol-var-elim condition) if it is possible to construct a solution to I from any solution s′ to I ′ in polynomial time.

A sol-var-elim condition not only allows us to eliminate variables while conserving satisfiability but also allows the polynomial-time recovery of at least one solution to the original instance I from a solution to the reduced instance I ′ . All the var-elim properties given in this paper are also sol-varelim properties.

## 3 Variable Elimination by the DE-snake Rule

Definition 3 A variable xi satisfies the DE-snake property if ∃vi ∈ D(xi) such that ∀xj ∈ X \ {xi}, ∀vj ∈ D(xj) with (vi, vj) /∈ Rij, ∃v′j ∈ D(xj) such that (1) (v′j , vi) ∈ Rji and (2) ∀xk ∈ X \ {xi, xj}, ∀vk ∈ D(xk), we do not have (vj, vk) ∈ Rjk and (v′j , vk) /∈ Rjk.

The DE-snake property is illustrated in Figure 1. The intuition behind this property is that any solution to the instance obtained after elimination of xi can be extended to a solution to the original instance by assigning vi to xi and changing those values vj which are incompatible with vi to some other value v′j .

Theorem 1 The DE-snake property is a sol-var-elim condition in binary CSP instances.

The following proposition shows that the worst-case complexity of applying the DE-snake rule is no worse than the complexity of applying the weaker ∃snake rule [Cohen et al., 2015].

Proposition 1 Variable eliminations by the DE-snake property can be applied until convergence in O(ed3 ) time and O(ed2 ) space.

## 4 The Triangle Property

The variable-elimination rule presented in this section says that xi can be eliminated if for some variable xj ̸= xi, for all assignments vj ∈ D(xj) to y, in I[〈xj, vj〉] (the reduced instance consisting of the set of variable-value assignments compatible with 〈xj , vj 〉) there is an assignment 〈xi, vi〉 compatible with all assignments to all variables xk ∈ X\{xi, xj}.

☞

✌

Figure 2: The open-triangle pattern.

![Image](https://ijcai.org/proceedings/2020/fulltext/702/image_000001_d9919c5306c69aef8fce274899a1cf7b97c1aafa95841afcc0bfa97914894be4.png)

In other words, there is some variable xj ̸= xi such that for all vj ∈ D(xj), there exists vi ∈ D(xi) such that (vj, vi) ∈ Rji and the open-triangle pattern shown in Figure 2 does not occur on (vi, vj, vk) for any vk.

Definition 4 A variable xi satisfies the triangle property if ∃xj ∈ X \ {xi} such that ∀vj ∈ D(xj), ∃vi ∈ D(xi) with (vi, vj) ∈ Rij such that ∀xk ∈ X \ {xi, xj}, ∀vk ∈ D(xk), (vj, vk) ∈ Rjk implies that (vi, vk) ∈ Rik.

Theorem 2 The triangle property is a sol-var-elim condition in binary CSP instances.

Proposition 2 Variable eliminations by the triangle property can be applied until convergence in O(end3 ) time and O(end2 ) space.

## 5 Variable Elimination by Broken Polyhedra

The broken-triangle property is a property of the microstructure of instances of the binary CSP which when satisfied allows either value merging [Cooper et al., 2016], variable elimination or the definition of a tractable class [Cooper et al., 2010]. In this section, we generalise the notion of broken triangle to broken polyhedron, which allows us to define rules for variable elimination parameterised by the dimension k of the polyhedron. We begin by recalling the definition of the broken-triangle property (BTP) [Cooper et al., 2010].

Definition 5 Let I = 〈X, D, R〉 be a binary CSP instance. A pair of values v′k , v′′ k ∈ D(xk) satisfies BTP if for each pair of variables (xi, xj) (with i, j ̸= k), ∀vi ∈ D(xi), ∀vj ∈ D(xj), if (vi, vj) ∈ Rij, (vi, v′k ) ∈ Rik and (vj, v′′ k ) ∈ Rjk, then (vi, v′′ k ) ∈ Rik or (vj, v′k ) ∈ Rjk. A variable xk satisfies BTP if each pair of values of D(xk) satisfies BTP. If I is equipped with an order &lt; on its variables, then I satisfies BTP for the variable order &lt; if each variable xk satisfies BTP in the sub-instance of I restricted to the variables xi such that xi ≤ xk.

If (vi, vj) ∈Rij,(vi, v′k ) ∈Rik, (vj, v′′ k ) ∈Rjk, (vi, v′′ k ) /∈ Rik and (vj, v′k ) /∈ Rjk (as in Figure 3), then the quadruple (v′k , vi, vj , v′′ k ) constitutes a broken triangle on xk. I satisfies the BTP on xk if no broken triangles occur on xk.

We now generalise the notion of broken triangle to broken polyhedron and show that this notion can be used to define variable elimination rules that are stronger than BTP. A broken triangle is a broken polyhedron of dimension 2. We now define a broken k-dimensional polyhedron for k ≥ 2.

Definition 6 A broken k-dimensional polyhedron on xm consists of

Figure 3: A broken triangle (v′k, vi, vj , v′′ k ).

![Image](https://ijcai.org/proceedings/2020/fulltext/702/image_000002_940862b6509a7428e71a1cb4b8df3d317462b58d869e35d5461cce05a588a88c.png)

- a consistent assignment 〈v1, . . . , vk〉 to distinct variables 〈xi1 , . . . , xik 〉 (where each xij (j = 1, . . . , k) is distinct from xm),
- k distinct values u1, . . . , uk ∈ Dm,

## such that

- ∀j ∈ {1, . . . , k}, (vj, uj) /∈ Rijm,
- ∀h, j ∈ {1, . . . , k}, if h ̸= j then (vh, uj) ∈ Rijm,

The assignment 〈v1, . . . , vk〉 to variables 〈xi1 , . . . , xik 〉 is known as the base of the broken polyhedron, and each assignment 〈xm, uj〉 (j = 1, . . . , k) is an apex.

A broken 3-dimensional polyhedron (i.e. a broken tetrahedron) is shown in Figure 4. A broken triangle (Figure 3) is a broken 2-dimensional polyhedron. We show that the notion of broken k-dimensional polyhedron allows us to define novel variable-elimination rules and tractable classes.

The broken-triangle property (BTP) has been generalised to the ∀∃BTP rule for variable elimination which allows us to eliminate more variables [Cooper, 2014] than BTP. Eliminating a variable satisfying the ∀∃BTP rule is strictly stronger than the BTP rule. This is demonstrated by the fact that ∀∃BTP, but not BTP, subsumes the rule that allows us to eliminate a variable xm when an assignment to xm is compatible with all assignments to all other variables. Another generic example is when all occurrences of the broken-triangle pattern on variable xm occur on pairs of values vm, v′m ∈ S ⊂ D(xm) and each assignment vi to each other variable xi ̸= xm has a support at xm in D(xm) \ S.

We first given the definition of the ∀∃ broken-triangle property [Cooper, 2014], in order to generalise it to k dimensions.

Definition 7 A binary CSP instance satisfies the ∀∃ brokentriangle property on variable xm if for all i1 ̸= m, for all v1 ∈ D(xi1 ), there exists vm ∈ D(xm) such that

1. 〈v1, vm〉 is a consistent assignment to variables 〈xi1 , xm〉, and
2. for all i2 /∈ {i1,m}, for all v2 ∈ D(xi2 ), there is no broken triangle on xm with base the assignment 〈v1, v2〉 to variables 〈xi1 , xi2 〉 and with an apex 〈xm, vm〉.

We now generalise the ∀∃BTP rule for variable elimination to the case of broken polyhedra of any dimension k ≥ 2. When k = 2 the following definition coincides with Definition 7 of the ∀∃BTP rule.

Figure 4: A broken tetrahedron.

![Image](https://ijcai.org/proceedings/2020/fulltext/702/image_000003_5f296781cd1f5e1122eecb398cda96dccf204f6204ecf384bd415aa875e04f48.png)

Definition 8 A binary CSP instance satisfies the ∀∃ broken k-dimensional polyhedron property on variable xm if for all distinct i1, . . . , ik-1 ̸= m, for all consistent assignments 〈v1, . . . , vk-1〉 to variables 〈xi1 , . . . , xik-1 〉, there exists vm ∈ D(xm) such that

1. 〈v1, . . . , vk-1, vm〉 is a consistent assignment to variables 〈xi1 , . . . , xik-1 , xm〉, and
2. for all ik /∈ {i1, . . . , ik-1,m}, for all vk ∈ D(xik ), there is no broken k-dimensional polyhedron on xm with base the assignment 〈v1, . . . , vk〉 to variables 〈xi1 , . . . , xik 〉 and with an apex 〈xm, vm〉.

The first condition of Definition 8 is a k-consistency condition on variable xm with respect to all other variables [Lecoutre, 2009]. The second condition guarantees that this k-consistency condition is sufficient for any consistent assignment to the variables X \ {xm} to be extendible to a consistent assignment to all variables.

Theorem 3 The ∀∃ broken k-dimensional polyhedron property is a sol-var-elim condition in binary CSP instances I with at least k variables.

The ∀∃ broken k-dimensional polyhedron property is interesting from a theoretical point of view. However, from a practical point of view, the time complexity of detecting whether variables can be eliminated is likely to be prohibitive. Indeed, for k = 3, a naive exhaustive search for broken tetrahedra has time complexity Θ(n4d6 ).

## 6 Theoretical Comparison of Rules

We say that two variable-elimination rules are incomparable if neither is subsumed by the other.

Proposition 3 The following three variable-elimination rules are all pairwise incomparable: the DE-snake property, the triangle property and ∀∃BTP.

## 7 Variable-Elimination Rules and Tractability

We now investigate the possibility of defining tractable classes based on our variable-elimination rules. As is the case for BTP [Cooper et al., 2010], the rules we have presented in this paper also define tractable classes that can be detected in polynomial time by successive elimination of variables.

Definition 9 For a variable-elimination property P, we say that a binary CSP instance I satisfies P for the variable order &lt; if for each variable xm, except for the first variable according to the order &lt;, I satisfies the property P on xm in the sub-instance of I restricted to the variables xi such that xi ≤ xm.

Theorem 4 The class of binary CSP instances I satisfying any of the following properties (for a possibly unknown ordering of its variables) can be detected and solved in polynomial time: the ∀∃ broken k-dimensional polyhedron property (for any fixed k ≥ 2), the DE-snake property, ∀∃BTP, and the triangle property.

When not all variables can be eliminated, we are interested in maximising the number of eliminated variables.

Theorem 5 Maximising the number of variables that can be eliminated by any of the following rules can be achieved in polynomial time: the ∀∃ broken k-dimensional polyhedron property (for any fixed k ≥ 2), the DE-snake property and ∀∃BTP. Maximising the number of variable eliminations by combining the triangle property and neighbourhood substitution [Freuder, 1991] can also be achieved in polynomial time.

## 8 Discussion and Conclusion

In this paper we have given novel satisfiability-conserving variable-elimination rules for binary CSPs. In each case, if the instance is satisfiable, then a solution to the original instance can be recovered in low-order polynomial time from a solution to the reduced instance. The DE-snake rule can be applied until convergence in O(ed3 ) time, whereas the corresponding time complexity for the triangle rule is O(end3 ). However, it should be pointed out that the DE-snake rule inherits the disadvantage of the ∃snake rule that the number of solutions may actually increase after elimination of a variable [Cohen et al., 2015]: for example, it allows us to eliminate the central variable in the two-colouring of a star graph which increases the number of solutions from 2 to 2n-1 .

Extensive experimental trials (reported in [Cooper et al., 2019]) have confirmed that because of relatively high time complexity of each of the variable-elimination rules, they may only be tested exhaustively during preprocessing. Applying them in preprocessing allowed us to solve more benchmark instances than without, the triangle rule allowing us to eliminate more variables and hence solve more instances than the other rules. We observed that most variables eliminated by our rules have small domain size and/or small degree.

We generalised the notion of broken triangle to broken polyhedron, which may be of theoretical interest.

We have also shown that each of the variable-elimination rules allows us to define a novel hybrid tractable class by successive elimination of almost all variables. For each rule, this elimination order can be found in polynomial time, which we found surprising in the case of the triangle property.

## Acknowledgments

This work was funded by the Agence Nationale de la Recherche projects ANR-16-C40-0028 and ANR-19-PI3A0004 (Artificial and Natural Intelligence Toulouse Institute).

## References

1. [Beigel and Eppstein, 1995] Richard Beigel and David Epp- stein. 3-Coloring in Time O(1.3446 n ): A No-MIS Algo- rithm. In 36th Annual Symposium on Foundations of Com- puter Science, Milwaukee, Wisconsin, USA, pages 444- 452. IEEE Computer Society, 1995.
2. [Bessière et al., 2005] Christian Bessière, Jean-Charles Régin, Roland H. C. Yap, and Yuanlin Zhang. An optimal coarse-grained arc consistency algorithm. Artif. Intell., 165(2):165-185, 2005.
3. [Cohen et al., 2015] David A. Cohen, Martin C. Cooper, Guillaume Escamocher, and Stanislav Zivny. Variable and value elimination in binary constraint satisfaction via for- bidden patterns. J. Comput. Syst. Sci., 81(7):1127-1143, 2015.
4. [Cooper et al., 2010] Martin C. Cooper, Peter G. Jeavons, and András Z. Salamon. Generalizing constraint satisfac- tion on trees: Hybrid tractability and variable elimination. Artif. Intell., 174(9-10):570-584, 2010.
5. [Cooper et al., 2016] Martin C. Cooper, Aymeric Duchein, Achref El Mouelhi, Guillaume Escamocher, Cyril Ter- rioux, and Bruno Zanuttini. Broken triangles: From value merging to a tractable class of general-arity constraint sat- isfaction problems. Artif. Intell., 234:196-218, 2016.
6. [Cooper et al., 2019] Martin C. Cooper, Achref El Mouelhi, and Cyril Terrioux. Variable elimination in binary CSPs. J. Artif. Intell. Res., 66:589-624, 2019.
7. [Cooper, 2014] Martin C. Cooper. Beyond Consistency and Substitutability. In Barry O'Sullivan, editor, Principles and Practice of Constraint Programming -20th Interna- tional Conference, CP 2014, Lyon, France, volume 8656 of Lecture Notes in Computer Science, pages 256-271. Springer, 2014.
8. [Dechter, 1999] Rina Dechter. Bucket Elimination: A Unify- ing Framework for Reasoning. Artif. Intell., 113(1-2):41- 85, 1999.
9. [Freuder, 1991] Eugene C. Freuder. Eliminating inter- changeable values in constraint satisfaction problems. In
10. Thomas L. Dean and Kathleen R. McKeown, editors, Pro- ceedings of the 9th National Conference on Artificial Intel- ligence, Anaheim, CA, USA, 1991, Volume 1., pages 227- 233. AAAI Press / The MIT Press, 1991.
11. [Jeavons et al., 1998] Peter Jeavons, David A. Cohen, and Martin C. Cooper. Constraints, Consistency and Closure. Artif. Intell., 101(1-2):251-265, 1998.
12. [Koubarakis, 2006] Manolis Koubarakis. Temporal CSPs. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, volume 2 of Foun- dations of Artificial Intelligence, pages 665-697. Elsevier, 2006.
13. [Kratsch et al., 2016] Stefan Kratsch, Geevarghese Philip, and Saurabh Ray. Point Line Cover: The Easy Kernel is Essentially Tight. ACM Trans. Algorithms, 12(3):40:1- 40:16, 2016.
14. [Larrosa and Dechter, 2003] Javier Larrosa and Rina Dechter. Boosting Search with Variable Elimination in Constraint Optimization and Constraint Satisfaction Problems. Constraints, 8(3):303-326, 2003.
15. [Lecoutre, 2009] Christophe Lecoutre. Constraint Networks Techniques and Algorithms. ISTE/Wiley, 2009.
16. [Newman et al., 2018] Neil Newman, Alexandre Fréchette, and Kevin Leyton-Brown. Deep optimization for spectrum repacking. Commun. ACM, 61(1):97-104, 2018.
17. [Schrijver, 1999] Alexander Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience Series in Dis- crete Mathematics and Optimization. Wiley, 1999.
18. [Subbarayan and Pradhan, 2004] Sathiamoorthy Sub- barayan and Dhiraj K. Pradhan. NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT instances. In SAT 2004 -The 7th International Conference on Theory and Applications of Satisfiability Testing, Vancouver, Canada, Online Proceedings, 2004.
19. [Zhang and Yap, 2011] Yuanlin Zhang and Roland H. C. Yap. Solving functional constraints by variable substitu- tion. TPLP, 11(2-3):297-322, 2011.
