Search

The stable marriage problem is a well-known problem of matching men to women so that no man and woman, who are not married to each other, both prefer each other. Such a problem has a wide variety of practical applications, ranging from matching resident doctors to hospitals, to matching students to schools or more generally to any two-sided market. In the classical stable marriage problem, both men and women express a strict preference order over the members of the other sex, in a qualitative way. Here we consider stable marriage problems with weighted preferences: each man (resp., woman) provides a score for each woman (resp., man). Such problems are more expressive than the classical stable marriage problems. Moreover, in some real-life situations it is more natural to express scores (to model, for example, profits or costs) rather than a qualitative preference ordering. In this context, we define new notions of stability and optimality, and we provide algorithms to find marriages which are stable and/or optimal according to these notions. While expressivity greatly increases by adopting weighted preferences, we show that in most cases the desired solutions can be found by adapting existing algorithms for the classical stable marriage problem. We also investigate manipulation issues in our framework. More precisely, we adapt the classical notion of manipulation to our context and we study if the procedures which return the new kinds of stable marriages are manipulable.

Many native ASP solvers exploit unfounded sets to compute consequences of a logic program via some form of well-founded negation, but disregard its contrapositive, well-founded justification WFJ, due to computational cost. However, we demonstrate that this can hinder propagation of many relevant conditions such as reachability. In order to perform WFJ with low computational cost, we devise a method that approximates its consequences by computing dominators in a flowgraph, a problem for which linear-time algorithms exist. Furthermore, our method allows for additional unfounded set inference, called well-founded domination WFD. We show that the effect of WFJ and WFD can be simulated for a important classes of logic programs that include reachability. Finally, we take a stand for native ASP solvers and show that unfounded set inference cannot be replaced by logic program transformations or translations into CNF-SAT.

We propose an adaptive heuristic for model restarts that aligns symmetry breaking with the dynamic branching heuristic. Experiments show that this method performs very well compared to other symmetry breaking methods.

We can break symmetry by eliminating solutions within each symmetry class. For instance, the Lex-Leader method eliminates all but the smallest solution in the lexicographical ordering. Unfortunately, the Lex-Leader method is intractable in general. We prove that, under modest assumptions, we cannot reduce the worst case complexity of breaking symmetry by using other orderings on solutions. We also prove that a common type of symmetry, where rows and columns in a matrix of decision variables are interchangeable, is intractable to break when we use two promising alternatives to the lexicographical ordering: the Gray code ordering (which uses a different ordering on solutions), and the Snake-Lex ordering (which is a variant of the lexicographical ordering that re-orders the variables). Nevertheless, we show experimentally that using other orderings like the Gray code to break symmetry can be beneficial in practice as they may better align with the objective function and branching heuristic.

Constraints can be exploited in paradigms outside of constraint programming. In particular, powerful global constraints can often be decomposed into small primitives and these decompositions can simulate complex propagation algorithms that perform sophisticated inference about a problem. We illustrate this approach with examples of exploiting constraints in propositional satisfiability (SAT), pseudo-Boolean (PB) solving, integer linear programming (ILP) and answer set programming (ASP).

We study propagation of a global constraint that ensures that each row of a matrix of decision variables satisfies a Regular constraint, and each column satisfies a Gcc constraint. On the negative side, we prove that propagation is NP-hard even under some strong restrictions (e.g. just 2 values, just 4 states in the automaton, just 5 columns to the matrix, or restricting to limited classes of automata). We also prove that propagation is W[2]-hard when the problem is parameterized by the number of rows in the matrix. On the positive side, we identify several cases where propagation is fixed parameter tractable.

Heterogeneous nonmonotonic multi-context systems (MCS) permit different logics to be used in different contexts, and link them via bridge rules. We investigate the role of symmetry detection and symmetry breaking in such systems to eliminate symmetric parts of the search space and, thereby, simplify the evaluation process. We propose a distributed algorithm that takes a local stance, i.e., computes independently the partial symmetries of a context and, in order to construct potential symmetries of the whole, combines them with those partial symmetries returned by neighbouring contexts. We prove the correctness of our methods. We instantiate such symmetry detection and symmetry breaking in a multi-context system with contexts that use answer set programs, and demonstrate computational benefit on some recently proposed benchmarks.

The stable marriage problem has a wide variety of practical applications, including matching resident doctors to hospitals, and students to schools. In the classical stable marriage problem, both men and women express a strict order over the members of the other sex. Here we consider a more realistic case, where both men and women can express their preferences via partial orders, i.e., by allowing ties and incomparability. This may be useful, for example, when preferences are elicited via compact preference representations like soft constraint or CP-nets that produce partial orders, as well as when preferences are obtained via multi-criteria reasoning. We study male optimality and uniqueness of stable marriages in this setting. Male optimality gives priority to one gender over the other, while uniqueness means that the solution is optimal, since it is as good as possible for all the participating agents. Uniqueness of solution is also a barrier against manipulation. We give an algorithm to find stable marriages that are male optimal. Moreover, we give sufficient conditions on the preferences (that are also necessary in some special case), that occur often in real-life scenarios, which guarantee the uniqueness of a stable marriage.

International audience; We propose ALLDIFFPREC, a new global constraint that combines together an ALLDIFFERENT constraint with precedence constraints that strictly order given pairs of variables. We identify a number of applications for this global constraint including instruction scheduling and symmetry breaking. We give an efficient propagation algorithm that enforces bounds consistency on this global constraint. We show how to implement this propagator using a decomposition that extends the bounds consistency enforcing decomposition proposed for the ALLDIFFERENT constraint. Finally, we prove that enforcing domain consistency on this global constraint is NP-hard in general.

We propose an online form of the cake cutting problem. This models situations where agents arrive and depart during the process of dividing a resource. We show that well known fair division procedures like cut-and-choose and the Dubins-Spanier moving knife procedure can be adapted to apply to such online problems. We propose some fairness properties that online cake cutting procedures can possess like online forms of proportionality and envy-freeness. We also consider the impact of collusion between agents. Finally, we study theoretically and empirically the competitive ratio of these online cake cutting procedures. Based on its resistance to collusion, and its good performance in practice, our results favour the online version of the cut-and-choose procedure over the online version of the moving knife procedure.

Symmetry can be used to help solve many problems. For instance, Einstein's famous 1905 paper ("On the Electrodynamics of Moving Bodies") uses symmetry to help derive the laws of special relativity. In artificial intelligence, symmetry has played an important role in both problem representation and reasoning. I describe recent work on using symmetry to help solve constraint satisfaction problems. Symmetries occur within individual solutions of problems as well as between different solutions of the same problem. Symmetry can also be applied to the constraints in a problem to give new symmetric constraints. Reasoning about symmetry can speed up problem solving, and has led to the discovery of new results in both graph and number theory.

Max Restricted Path Consistency (maxRPC) is a local consistency for binary constraints that can achieve considerably stronger pruning than arc consistency. However, existing maxRPC algorithms suffer from overheads and redundancies as they can repeatedly perform many constraint checks without triggering any value deletions. In this paper we propose techniques that can boost the performance of maxRPC algorithms. These include the combined use of two data structures to avoid many redundant constraint checks, and heuristics for the efficient ordering and execution of certain operations. Based on these, we propose two closely related maxRPC algorithms. The first one has optimal O(end3) time complexity, displays good performance when used stand-alone, but is expensive to apply during search. The second one has O(en2d4) time complexity, but a restricted version with O(end4) complexity can be very efficient when used during search. Both algorithms have O(ed) space complexity when used stand-alone. However, the first algorithm has O(end) space complexity when used during search, while the second retains the O(ed) complexity. Experimental results demonstrate that the resulting methods constantly outperform previous algorithms for maxRPC, often by large margins, and constitute a more than viable alternative to arc consistency.

Symmetry is a common feature of many combinatorial problems. Unfortunately eliminating all symmetry from a problem is often computationally intractable. This paper argues that recent parameterized complexity results provide insight into that intractability and help identify special cases in which symmetry can be dealt with more tractably

In sports competitions, teams can manipulate the result by, for instance, throwing games. We show that we can decide how to manipulate round robin and cup competitions, two of the most popular types of sporting competitions in polynomial time. In addition, we show that finding the minimal number of games that need to be thrown to manipulate the result can also be determined in polynomial time. Finally, we show that there are several different variations of standard cup competitions where manipulation remains polynomial.

An attractive mechanism to specify global constraints in rostering and other domains is via formal languages. For instance, the Regular and Grammar constraints specify constraints in terms of the languages accepted by an automaton and a context-free grammar respectively. Taking advantage of the fixed length of the constraint, we give an algorithm to transform a context-free grammar into an automaton. We then study the use of minimization techniques to reduce the size of such automata and speed up propagation. We show that minimizing such automata after they have been unfolded and domains initially reduced can give automata that are more compact than minimizing before unfolding and reducing. Experimental results show that such transformations can improve the size of rostering problems that we can "model and run".

Restart strategies are an important factor in the performance of conflict-driven Davis Putnam style SAT solvers. Selecting a good restart strategy for a problem instance can enhance the performance of a solver. Inspired by recent success applying machine learning techniques to predict the runtime of SAT solvers, we present a method which uses machine learning to boost solver performance through a smart selection of the restart strategy. Based on easy to compute features, we train both a satisfiability classifier and runtime models. We use these models to choose between restart strategies. We present experimental results comparing this technique with the most commonly used restart strategies. Our results demonstrate that machine learning is effective in improving solver performance.

We propose a new family of constraints which combine together lexicographical ordering constraints for symmetry breaking with other common global constraints. We give a general purpose propagator for this family of constraints, and show how to improve its complexity by exploiting properties of the included global constraints.

We investigate the global GRAMMAR constraint over restricted classes of context free grammars like deterministic and unambiguous context-free grammars. We show that detecting disentailment for the GRAMMAR constraint in these cases is as hard as parsing an unrestricted context free grammar.We also consider the class of linear grammars and give a propagator that runs in quadratic time. Finally, to demonstrate the use of linear grammars, we show that a weighted linear GRAMMAR constraint can efficiently encode the EDITDISTANCE constraint, and a conjunction of the EDITDISTANCE constraint and the REGULAR constraint.

We propose new filtering algorithms for the Sequence constraint and some extensions of the Sequence constraint based on network flows. We enforce domain consistency on the Sequence constraint in O(n2) time down a branch of the search tree. This improves upon the best existing domain consistency algorithm by a factor of O(logn). The flows used in these algorithms are derived from a linear program. Some of them differ from the flows used to propagate global constraints like Gcc since the domains of the variables are encoded as costs on the edges rather than capacities. Such flows are efficient for maintaining bounds consistency over large domains and may be useful for other global constraints.

Fuzzy constraints are a popular approach to handle preferences and over-constrained problems in scenarios where one needs to be cautious, such as in medical or space applications. We consider here fuzzy constraint problems where some of the preferences may be missing. This models, for example, settings where agents are distributed and have privacy issues, or where there is an ongoing preference elicitation process. In this setting, we study how to find a solution which is optimal irrespective of the missing preferences. In the process of finding such a solution, we may elicit preferences from the user if necessary. However, our goal is to ask the user as little as possible. We define a combined solving and preference elicitation scheme with a large number of different instantiations, each corresponding to a concrete algorithm which we compare experimentally. We compute both the number of elicited preferences and the "user effort", which may be larger, as it contains all the preference values the user has to compute to be able to respond to the elicitation requests. While the number of elicited preferences is important when the concern is to communicate as little information as possible, the user effort measures also the hidden work the user has to do to be able to communicate the elicited preferences. Our experimental results show that some of our algorithms are very good at finding a necessarily optimal solution while asking the user for only a very small fraction of the missing preferences. The user effort is also very small for the best algorithms. Finally, we test these algorithms on hard constraint problems with possibly missing constraints, where the aim is to find feasible solutions irrespective of the missing constraints., Principles and Practice of Constraint Programming, 14th International Conference, CP 2008, Sydney, Australia, September 14-18, 2008. Proceedings

We introduce the weighted CFG constraint and propose a propagation algorithm that enforces domain consistency in O(n3|G|) time. We show that this algorithm can be decomposed into a set of primitive arithmetic constraints without hindering propagation.

We present an online method for estimating the cost of solving SAT problems. Modern SAT solvers present several challenges to estimate search cost including non-chronological backtracking, learning and restarts. Our method uses a linear model trained on data gathered at the start of search. We show the effectiveness of this method using random and structured problems. We demonstrate that predictions made in early restarts can be used to improve later predictions. We also show that we can use such cost estimations to select a solver from a portfolio.

We present an algorithm for compressing table constraints representing allowed or disallowed tuples. This type of constraint is used for example in configuration problems, where the satisfying tuples are read from a database. The arity of these constraints may be large. A generic GAC algorithm for such a constraint requires time exponential in the arity of the constraint to maintain GAC, but Bessiere and Regin showed in [1] that for the case of allowed tuples, GAC can be enforced in time proportional to the number of allowed tuples, using the algorithm GAC-Schema. We introduce a more compact representation for a set of tuples, which allows a potentially exponential reduction in the space needed to represent the satisfying tuples and exponential reduction in the time needed to enforce GAC. We show that this representation can be constructed from a decision tree that represents the original tuples and demonstrate that it does in practice produce a significantly shorter description of the constraint. We also show that this representation can be efficiently used in existing algorithms and can be used to improve GAC-Schema further. Finally, we show that this method can be used to improve the complexity of enforcing GAC on a table constraint defined in terms of forbidden tuples.

A common type of symmetry is when both variables and values partition into interchangeable sets. Polynomial methods have been introduced to eliminate all symmetric solutions introduced by such interchangeability. Unfortunately, whilst eliminating all symmetric solutions is tractable in this case, pruning all symmetric values is NP-hard. We introduce a new global constraint called SIGLEX and its GAC propagator for pruning some (but not necessarily all) symmetric values. We also investigate how different postings of the SIGLEX constraints affect the pruning performance during constraint solving. Finally, we test these static symmetry breaking constraints experimentally for the first time.

The SEQUENCE constraint is useful in modelling car sequencing, rostering, scheduling and related problems. We introduce half a dozen new encodings of the SEQUENCE constraint, some of which do not hinder propagation. We prove that, down a branch of a search tree, domain consistency can be enforced on the SEQUENCE constraint in just O(n2 log n) time. This improves upon the previous bound of O(n3) for each call down the tree. We also consider a generalization of the SEQUENCE constraint - the Multiple SEQUENCE constraint. Our experiments suggest that, on very large and tight problems, domain consistency algorithms are best. However, on smaller or looser problems, much simpler encodings are better, even though these encodings hinder propagation. When there are multiple SEQUENCE constraints, a more expensive propagator shows promise.

Symmetry is an important factor in solving many constraint satisfaction problems. One common type of symmetry is when we have symmetric values. In a recent series of papers, we have studied methods to break value symmetries (Walsh 2006a; 2007). Our results identify computational limits on eliminating value symmetry. For instance, we prove that pruning all symmetric values is NP-hard in general. Nevertheless, experiments show that much value symmetry can be broken in practice. These results may be useful to researchers in planning, scheduling and other areas as value symmetry occurs in many different domains.

A wide range of constraints can be specified using automata or formal languages. The GRAMMAR constraint restricts the values taken by a sequence of variables to be a string from a given context-free language. Based on an AND/OR decomposition, we show that this constraint can be converted into clauses in conjunctive normal form without hindering propagation. Using this decomposition, we can propagate the GRAMMAR constraint in O(n3) time. The decomposition also provides an efficient incremental propagator. Down a branch of the search tree of length k, we can enforce GAC k times in the same O(n3) time. On specialized languages, running time can be even better. For example, propagation of the decomposition requires just O(n|δ|) time for regular languages where |δ| is the size of the transition table of the automaton recognizing the regular language. Experiments on a shift scheduling problem with a constraint solver and a state of the art SAT solver show that we can solve problems using this decomposition that defeat existing constraint solvers.

We describe some new propagators for breaking symmetries in constraint satisfaction problems. We also introduce symmetry breaking constraints to deal with symmetries acting simultaneously on variables and values, conditional symmetries, as well as symmeties acting on set and other types of variables.

Global constraints are an important tool in the constraint toolkit. Unfortunately, whilst it is usually easy to specify when a global constraint holds, it is often difficult to build a good propagator. One promising direction is to specify global constraints via grammars or automata. For example, the Regular constraint [1] permits us to specify a wide range of global constraints by means of a DFA accepting a regular language, and to propagate this constraint specification efficiently and effectively. More precisely, the Regular constraint ensures that the values taken by a sequence of variables form a string accepted by the DFA. In this paper, we consider how to propagate such grammar constraints and a number of extensions.

We describe how the propagator for the All-Different constraint can be generalized to prune variables whose domains are not just simple finite domains. We show, for example, how it can be used to propagate set variables, multiset variables and variables which represent tuples of values. We also describe how the propagator for the global cardinality constraint (which is a generalization of the All-Different constraint) can be generalized in a similar way. Experiments show that such propagators can be beneficial in practice, especially when the domains are large.

The G12 project recently started by National ICT Australia (NICTA)is an ambitious project to develop a software platform for solving large scale industrial combinatorial optimisation problems. The core design involves three languages: Zinc, Cadmium and Mercury (Group 12 of the periodic table). Zinc is a declarative modelling language for expressing problems, independent of any solving methodology. Cadmium is a mapping language for mapping Zinc models to underlying solvers and/or search strategies, including hybrid approaches. Finally, existing Mercury will be extended as a language for building extensible and hybridizable solvers. The same Zinc model, used with different Cadmium mappings, will allow us to experiment with different complete, local, or hybrid search approaches for the same problem. This talk will explain the G12 global design, the final G12 objectives, and our progress so far.

Super solutions are a mechanism to provide robustness to constraint programs. We introduce a new algorithm that exploits the similarity between a super solution and its repairs in order to do inference during search. It improves on previous methods since it is more space efficient and also faster in practice.

To use constraint technology to solve a problem, the solutions to the problem must first be characterised, or modelled, by a set of constraints that they must satisfy. A significant part of the modelling process can be characterised as refinement, the process of generating a concrete model from an abstract specification of the problem. Expert modellers also identify and perform transformations that can dramatically reduce the effort needed to solve the problem by systematic search. Through a case study of modelling a simplified version of the SONET fibre-optic communication problem, this paper examines the processes of refinement and transformation, and especially the interaction between the two.

We describe how the propagator for the ALL-DIFFERENT constraint can be generalized to prune variables whose domains are not just simple finite integer domains. We show, for example, how it can be used to propagate set, multiset and tuple variables.

To improve solution robustness, we introduce the concept of super solutions to constraint programming. An (a,b)-super solution is one in which if a variables lose their values, the solution can be repaired by assigning these variables with a new values and at most b other variables. Super solutions are a generalization of supermodels in propositional satisfiability. We focus in this paper on (1,0)-super solutions, where if one variable loses its value, we can find another solution by re-assigning this variable with a new value. To find super solutions, we explore methods based both on reformulation and on search. Our reformulation methods transform the constraint satisfaction problem so that the only solutions are super solutions. Our search methods are based on a notion of super consistency. Experiments show that super MAC, a novel search-based method shows considerable promise. When super solutions do not exist, we show how to find the most robust solution. Finally, we extend our approach from robust solutions of constraint satisfaction problems to constraint optimization problems.

short paper; International audience; Constraint propagation is one of the techniques central to the success of constraint programming. Fast algorithms are used to prune the search space either before or during backtracking search. Propagating global constraints is intractable in general. In this paper, we characterize a number of important questions related to constraint propagation. For example, we consider the two questions: "Is this problem generalized arc-consistent?" and "What are the maximal generalized arc-consistent domains?". We identify dependencies between the tractability and intractability of these questions for finite domain variables. Finally, we prove intractability for a range of global constraints.

Great progress has been made on DPLL based SAT solvers operating on CNF encoded SAT theories. However, for most problems CNF is not a very natural representation. Typically these problems are more easily expressed using unrestricted propositional formulae and hence must be converted to CNF before modern SAT solvers can be applied. This conversion entails a considerable loss of information about the problem's structure. In this work we demonstrate that conversion to CNF is both unnecessary and undesirable. In particular, we demonstrate that a SAT solver which operates directly on a propositional formula can achieve the same efficiency as a highly optimized modern CNF solver. Furthermore, since the original formula remains intact, such a solver can exploit the original problem structure to improve over CNF solvers. We present empirical evidence showing that exploiting the original structure can yield considerable benefits. An extended abstract on this topic was presented at the SAT-2004 conference.

Constraint models contain a number of common patterns. For example, many constraint models involve an array of decision variables with symmetric rows and/or columns. By documenting such constraint patterns, we can share modelling expertise. Constraint solvers can also be extended to exploit such patterns. For example, we can develop specialized methods like the global lexicographical ordering constraint for breaking such row and column symmetry.

We study from a formal perspective the consistency and propagation of constraints involving multiset variables. That is, variables whose values are multisets. These help us model problems more naturally and can, for example, prevent introducing unnecessary symmetry into a model. We identify a number of different representations for multiset variables and compare them. We then propose a definition of local consistency for constraints involving multiset, set and integer variables. This definition is a generalization of the notion of bounds consistency for integer variables. We show how this local consistency property can be enforced by means of some simple inference rules which tighten bounds on the variables. We also study a number of global constraints on set and multiset variables. Surprisingly, unlike finite domain variables, the decomposition of global constraints over set or multiset variables often does not hinder constraint propagation.

The Bounded Model Checking approach to the LTL model checking problem, based on an encoding to Boolean satisfiability, has seen a growth in popularity due to recent improvements in SAT technology. The currently available encodings have certain shortcomings, particularly in the size of the clause forms that it generates. We address this by making use of the established correspondence between temporal logic expressions and the fixpoints of predicate transformers as used in symbolic model checking. We demonstrate how an encoding based on fixpoints can result in improved performance in the SAT checker.

We identify an important class of symmetries in constraint programming, arising from matrices of decision variables where rows and columns can be swapped. Whilst lexicographically ordering the rows (columns) breaks all the row (column) symmetries, lexicographically ordering both the rows and the columns fails to break all the compositions of the row and column symmetries. Nevertheless, our experimental results show that this is effective at dealing with these compositions of symmetries. We extend these results to cope with symmetries in any number of dimensions, with partial symmetries, and with symmetric values. Finally, we identify special cases where all compositions of the row and column symmetries can be eliminated by the addition of only a linear number of symmetry-breaking constraints.

Davis-Putnam (DP) [3] was the first practical complete algorithm for solving propositional satisfiability (SAT) problems. DP uses resolution to determine whether a SAT problem instance is satisfiable. However, resolution is generally impractical, as it can use exponential space and time. The most important refinement to DP was DLL [2], which replaced the resolution in DP with backtracking search. Backtracking search still uses exponential time in the worst case, but only needs linear space. As time is more readily available than space, the change to search was a big improvement.

We propose some global constraints for lexicographic orderings on vectors of variables. These constraints are very useful for breaking a certain kind of symmetry arising in matrices of decision variables. We show that decomposing such constraints carries a penalty either in the amount or the cost of constraint propagation. We therefore present a global consistency algorithm which enforces a lexicographic ordering between two vectors of n variables in O(nb) time, where b is the cost of adjusting the bounds of a variable. The algorithm can be modified very slightly to enforce a strict lexicographic ordering. Our experimental results on a number of domains (balanced incomplete block design, social golfer, and sports tournament scheduling) confirm the efficiency and value of these new global constraints.

There are many problems that can be modelled as injection problems. These problems can be scheduling problems, combinatorial graph problems, cryptarithmetic puzzles, etc. Injection problems can be modelled as constraint satisfaction problems. The straightforward formulation would be to have as many variables as the elements of the source set that range over the target set, which captures a total function. To enforce that the function is injective, we would need to state an alldifferent constraint among all the variables. Dual variables can also be used along with the primal ones and linked through channeling constraints. We propose three different ways of achieveing this, as well as we add some implied constraints. The proposed models of injection problems are compared using the constraint tightness parameterized by the level of local consistency being enforced [2]. We proved that, with respect to arc-consistency a single primal alldifferent constraint is tighter than channeling constraints together with the implied or the dual not-equals constraints, but that the channeling constraints alone are as tight as the primal not-equals constraints. Both these gaps can lead to an exponential reduction in search cost when MAC or MGAC are used. The theoretical results showed that occurs constraints on dual variables are redundant, so we can safely discard them. The asymptotic analysis added details to the theoretical results. We conclude that it is safe to discard some of the models because they achieve less pruning than other models at the same cost. However, we keep a model employing primal and dual variables even though it achieves the same amount of pruning as a primal model at a higher cost because it might allow the development of cheap value ordering heuristics. Experimental results on a sport scheduling problem confirmed that MGAC on channeling and implied constraints outperformed MAC on primal not-equals constraints, and could be competitive with maintaining GAC on a primal alldifferent constraint.

When writing a constraint program, we have to decide what to make the decision variable, and how to represent the constraints on these variables. In many cases, there is considerable choice for the decision variables. For example, with permutation problems, we can choose between a primal and a dual representation. In the dual representation, dual variables stand for the primal values, whilst dual values stand for the primal variables. By means of channelling constraints, a combined model can have both primal and dual variables. In this paper, we perform an extensive theoretical and empirical study of these different models. Our results will aid constraint programmers to choose a model for a permutation problem. They also illustrate a general methodology for comparing different constraint models.