Constraint satisfaction problem

Last updated

Constraint satisfaction problems (CSPs) are mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem as a homogeneous collection of finite constraints over variables, which is solved by constraint satisfaction methods. CSPs are the subject of research in both artificial intelligence and operations research, since the regularity in their formulation provides a common basis to analyze and solve problems of many seemingly unrelated families. CSPs often exhibit high complexity, requiring a combination of heuristics and combinatorial search methods to be solved in a reasonable time. Constraint programming (CP) is the field of research that specifically focuses on tackling these kinds of problems. [1] [2] Additionally, the Boolean satisfiability problem (SAT), satisfiability modulo theories (SMT), mixed integer programming (MIP) and answer set programming (ASP) are all fields of research focusing on the resolution of particular forms of the constraint satisfaction problem.

Contents

Examples of problems that can be modeled as a constraint satisfaction problem include:

These are often provided with tutorials of CP, ASP, Boolean SAT and SMT solvers. In the general case, constraint problems can be much harder, and may not be expressible in some of these simpler systems. "Real life" examples include automated planning, [6] [7] lexical disambiguation, [8] [9] musicology, [10] product configuration [11] and resource allocation. [12]

The existence of a solution to a CSP can be viewed as a decision problem. This can be decided by finding a solution, or failing to find a solution after exhaustive search (stochastic algorithms typically never reach an exhaustive conclusion, while directed searches often do, on sufficiently small problems). In some cases the CSP might be known to have solutions beforehand, through some other mathematical inference process.

Formal definition

Formally, a constraint satisfaction problem is defined as a triple , where [13]

Each variable can take on the values in the nonempty domain . Every constraint is in turn a pair , where is a subset of variables and is a -ary relation on the corresponding subset of domains . An evaluation of the variables is a function from a subset of variables to a particular set of values in the corresponding subset of domains. An evaluation satisfies a constraint if the values assigned to the variables satisfy the relation .

An evaluation is consistent if it does not violate any of the constraints. An evaluation is complete if it includes all variables. An evaluation is a solution if it is consistent and complete; such an evaluation is said to solve the constraint satisfaction problem.

Solution

Constraint satisfaction problems on finite domains are typically solved using a form of search. The most used techniques are variants of backtracking, constraint propagation, and local search. These techniques are also often combined, as in the VLNS method, and current research involves other technologies such as linear programming. [14]

Backtracking is a recursive algorithm. It maintains a partial assignment of the variables. Initially, all variables are unassigned. At each step, a variable is chosen, and all possible values are assigned to it in turn. For each value, the consistency of the partial assignment with the constraints is checked; in case of consistency, a recursive call is performed. When all values have been tried, the algorithm backtracks. In this basic backtracking algorithm, consistency is defined as the satisfaction of all constraints whose variables are all assigned. Several variants of backtracking exist. Backmarking improves the efficiency of checking consistency. Backjumping allows saving part of the search by backtracking "more than one variable" in some cases. Constraint learning infers and saves new constraints that can be later used to avoid part of the search. Look-ahead is also often used in backtracking to attempt to foresee the effects of choosing a variable or a value, thus sometimes determining in advance when a subproblem is satisfiable or unsatisfiable.

Constraint propagation techniques are methods used to modify a constraint satisfaction problem. More precisely, they are methods that enforce a form of local consistency, which are conditions related to the consistency of a group of variables and/or constraints. Constraint propagation has various uses. First, it turns a problem into one that is equivalent but is usually simpler to solve. Second, it may prove satisfiability or unsatisfiability of problems. This is not guaranteed to happen in general; however, it always happens for some forms of constraint propagation and/or for certain kinds of problems. The most known and used forms of local consistency are arc consistency, hyper-arc consistency, and path consistency. The most popular constraint propagation method is the AC-3 algorithm, which enforces arc consistency.

Local search methods are incomplete satisfiability algorithms. They may find a solution of a problem, but they may fail even if the problem is satisfiable. They work by iteratively improving a complete assignment over the variables. At each step, a small number of variables are changed in value, with the overall aim of increasing the number of constraints satisfied by this assignment. The min-conflicts algorithm is a local search algorithm specific for CSPs and is based on that principle. In practice, local search appears to work well when these changes are also affected by random choices. An integration of search with local search has been developed, leading to hybrid algorithms.

Theoretical aspects

Decision problems

CSPs are also studied in computational complexity theory and finite model theory. An important dichotomy theorem states that for each set of relations, the set of all CSPs that can be represented using only relations chosen from that set is either in P or NP-complete. CSPs thus provide one of the largest known subsets of NP which avoids NP-intermediate problems, whose existence was demonstrated by Ladner's theorem under the assumption that P ≠ NP. Schaefer's dichotomy theorem handles the case when all the available relations are Boolean operators, that is, for domain size 2. Schaefer's dichotomy theorem was later generalized to a larger class of relations, [15] and a full dichotomy theorem was first conjectured as the Feder–Vardi conjecture [16] and finally proved independently by Andrei Bulatov [17] and Dmitriy Zhuk. [18]

Most classes of CSPs that are known to be tractable are those where the hypergraph of constraints has bounded treewidth (and there are no restrictions on the set of constraint relations), or where the constraints have arbitrary form but there exist essentially non-unary polymorphisms[ clarification needed ] of the set of constraint relations.

Every CSP can also be considered as a conjunctive query containment problem. [19]

Function problems

A similar situation exists between the functional classes FP and #P. By a generalization of Ladner's theorem, there are also problems in neither FP nor #P-complete as long as FP ≠ #P. As in the decision case, a problem in the #CSP is defined by a set of relations. Each problem takes a Boolean formula as input and the task is to compute the number of satisfying assignments. This can be further generalized by using larger domain sizes and attaching a weight to each satisfying assignment and computing the sum of these weights. It is known that any complex weighted #CSP problem is either in FP or #P-hard. [20]

Variants

The classic model of Constraint Satisfaction Problem defines a model of static, inflexible constraints. This rigid model is a shortcoming that makes it difficult to represent problems easily. [21] Several modifications of the basic CSP definition have been proposed to adapt the model to a wide variety of problems.

Dynamic CSPs

Dynamic CSPs [22] (DCSPs) are useful when the original formulation of a problem is altered in some way, typically because the set of constraints to consider evolves because of the environment. [23] DCSPs are viewed as a sequence of static CSPs, each one a transformation of the previous one in which variables and constraints can be added (restriction) or removed (relaxation). Information found in the initial formulations of the problem can be used to refine the next ones. The solving method can be classified according to the way in which information is transferred:

Flexible CSPs

Classic CSPs treat constraints as hard, meaning that they are imperative (each solution must satisfy all of them) and inflexible (in the sense that they must be completely satisfied or else they are completely violated). Flexible CSPs relax those assumptions, partially relaxing the constraints and allowing the solution to not comply with all of them. This is similar to preferences in preference-based planning. Some types of flexible CSPs include:

Decentralized CSPs

In DCSPs [24] each constraint variable is thought of as having a separate geographic location. Strong constraints are placed on information exchange between variables, requiring the use of fully distributed algorithms to solve the constraint satisfaction problem.

See also

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

Constraint programming (CP) is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state the constraints on the feasible solutions for a set of decision variables. Constraints differ from the common primitives of imperative programming languages in that they do not specify a step or sequence of steps to execute, but rather the properties of a solution to be found. In addition to constraints, users also need to specify a method to solve these constraints. This typically draws upon standard methods like chronological backtracking and constraint propagation, but may use customized code like a problem-specific branching heuristic.

Backtracking is a class of algorithms for finding solutions to some computational problems, notably constraint satisfaction problems, that incrementally builds candidates to the solutions, and abandons a candidate ("backtracks") as soon as it determines that the candidate cannot possibly be completed to a valid solution.

In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time.

In artificial intelligence and operations research, constraint satisfaction is the process of finding a solution through a set of constraints that impose conditions that the variables must satisfy. A solution is therefore an assignment of values to the variables that satisfies all constraints—that is, a point in the feasible region.

In computational complexity theory, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. It is a generalization of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.

In constraint satisfaction, local consistency conditions are properties of constraint satisfaction problems related to the consistency of subsets of variables or constraints. They can be used to reduce the search space and make the problem easier to solve. Various kinds of local consistency conditions are leveraged, including node consistency, arc consistency, and path consistency.

In backtracking algorithms, look ahead is the generic term for a subprocedure that attempts to foresee the effects of choosing a branching variable to evaluate one of its values. The two main aims of look-ahead are to choose a variable to evaluate next and to choose the order of values to assign to it.

<span class="mw-page-title-main">Local search (constraint satisfaction)</span>

In constraint satisfaction, local search is an incomplete method for finding a solution to a problem. It is based on iteratively improving an assignment of the variables until all constraints are satisfied. In particular, local search algorithms typically modify the value of a variable in an assignment at each step. The new assignment is close to the previous one in the space of assignment, hence the name local search.

In mathematical optimization, constrained optimization is the process of optimizing an objective function with respect to some variables in the presence of constraints on those variables. The objective function is either a cost function or energy function, which is to be minimized, or a reward function or utility function, which is to be maximized. Constraints can be either hard constraints, which set conditions for the variables that are required to be satisfied, or soft constraints, which have some variable values that are penalized in the objective function if, and based on the extent that, the conditions on the variables are not satisfied.

Within artificial intelligence and operations research for constraint satisfaction a hybrid algorithm solves a constraint satisfaction problem by the combination of two different methods, for example variable conditioning and constraint inference

Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is A(X,Y):-X+Y>0,B(X),C(Y). In this clause, X+Y>0 is a constraint; A(X,Y), B(X), and C(Y) are literals as in regular logic programming. This clause states one condition under which the statement A(X,Y) holds: X+Y is greater than zero and both B(X) and C(Y) are true.

The complexity of constraint satisfaction is the application of computational complexity theory to constraint satisfaction. It has mainly been studied for discriminating between tractable and intractable classes of constraint satisfaction problems on finite domains.

In computational complexity theory, a branch of computer science, Schaefer's dichotomy theorem, proved by Thomas Jerome Schaefer, states necessary and sufficient conditions under which a finite set S of relations over the Boolean domain yields polynomial-time or NP-complete problems when the relations of S are used to constrain some of the propositional variables. It is called a dichotomy theorem because the complexity of the problem defined by S is either in P or is NP-complete, as opposed to one of the classes of intermediate complexity that is known to exist by Ladner's theorem.

In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently.

In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.

In artificial intelligence and operations research, a Weighted Constraint Satisfaction Problem (WCSP) is a generalization of a constraint satisfaction problem (CSP) where some of the constraints can be violated and in which preferences among solutions can be expressed. This generalization makes it possible to represent more real-world problems, in particular those that are over-constrained, or those where we want to find a minimal-cost solution among multiple possible solutions.

In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to true. The internal workings of CDCL SAT solvers were inspired by DPLL solvers. The main difference between CDCL and DPLL is that CDCL's backjumping is non-chronological.

In computer science, an interchangeability algorithm is a technique used to more efficiently solve constraint satisfaction problems (CSP). A CSP is a mathematical problem in which objects, represented by variables, are subject to constraints on the values of those variables; the goal in a CSP is to assign values to the variables that are consistent with the constraints. If two variables A and B in a CSP may be swapped for each other without changing the nature of the problem or its solutions, then A and B are interchangeable variables. Interchangeable variables represent a symmetry of the CSP and by exploiting that symmetry, the search space for solutions to a CSP problem may be reduced. For example, if solutions with A=1 and B=2 have been tried, then by interchange symmetry, solutions with B=1 and A=2 need not be investigated.

In computational complexity theory, a branch of computer science, the Max/min CSP/Ones classification theorems state necessary and sufficient conditions that determine the complexity classes of problems about satisfying a subset S of boolean relations. They are similar to Schaefer's dichotomy theorem, which classifies the complexity of satisfying finite sets of relations; however, the Max/min CSP/Ones classification theorems give information about the complexity of approximating an optimal solution to a problem defined by S.

References

  1. Lecoutre, Christophe (2013). Constraint Networks: Techniques and Algorithms. Wiley. p. 26. ISBN   978-1-118-61791-5.
  2. "Constraints – incl. option to publish open access". springer.com. Retrieved 2019-10-03.
  3. Chandra, Satish, et al. "Type inference for static compilation of JavaScript." ACM SIGPLAN Notices 51.10 (2016): 410-429.
  4. Jim, Trevor, and Jens Palsberg. "Type inference in systems of recursive types with subtyping." Available on authors' web page (1999).
  5. Farhi, Edward and Harrow, Aram. "Quantum Supremacy through the Quantum Approximate Optimization Algorithm." arXiv:1602.07674
  6. Malik Ghallab; Dana Nau; Paolo Traverso (21 May 2004). Automated Planning: Theory and Practice. Elsevier. pp. 1–. ISBN   978-0-08-049051-9.
  7. Dynamic Flexible Constraint Satisfaction and Its Application to AI Planning, Archived 2009-02-06 at the Wayback Machine Ian Miguel – slides.
  8. Demetriou, George C. "Lexical disambiguation using constraint handling in Prolog (CHIP)." Proceedings of the sixth conference on European chapter of the Association for Computational Linguistics. Association for Computational Linguistics, 1993.
  9. MacDonald, Maryellen C., and Mark S. Seidenberg. "Constraint satisfaction accounts of lexical and sentence comprehension." Handbook of Psycholinguistics (Second Edition). 2006. 581–611.
  10. Mauricio Toro, Carlos Agon, Camilo Rueda, Gerard Assayag. "GELISP: A FRAMEWORK TO REPRESENT MUSICAL CONSTRAINT SATISFACTION PROBLEMS AND SEARCH STRATEGIES." Journal of Theoretical and Applied Information Technology 86 (2). 2016. 327–331.
  11. Applying constraint satisfaction approach to solve product configuration problems with cardinality-based configuration rules, Dong Yang & Ming Dong, Journal of Intelligent Manufacturing volume 24, pages99–111 (2013)
  12. Modi, Pragnesh Jay, et al. "A dynamic distributed constraint satisfaction approach to resource allocation." International Conference on Principles and Practice of Constraint Programming. Springer, Berlin, Heidelberg, 2001.
  13. Stuart Jonathan Russell; Peter Norvig (2010). Artificial Intelligence: A Modern Approach. Prentice Hall. p. Chapter 6. ISBN   9780136042594.
  14. Milano, Michela; Van Hentenryck, Pascal, eds. (2011). Hybrid optimization : the ten years of CPAIOR. International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimisation Problems. New York: Springer. ISBN   9781441916440. OCLC   695387020.
  15. Bodirsky, Manuel; Pinsker, Michael (2011). "Schaefer's theorem for graphs". Proceedings of the 43rd Annual Symposium on Theory of Computing (STOC '11). Association for Computing Machinery. pp. 655–664. arXiv: 1011.2894 . Bibcode:2010arXiv1011.2894B. doi:10.1145/1993636.1993724. ISBN   978-1-4503-0691-1. S2CID   47097319.
  16. Feder, Tomás; Vardi, Moshe Y. (1998). "The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory". SIAM Journal on Computing. 28 (1): 57–104. doi:10.1137/S0097539794266766. ISSN   0097-5397.
  17. Bulatov, Andrei (2017). "A Dichotomy Theorem for Nonuniform CSPs". Proceedings of the 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017. IEEE Computer Society. pp. 319–330. doi:10.1109/FOCS.2017.37.
  18. Zhuk, Dmitriy (2020). "A Proof of the CSP Dichotomy Conjecture". Journal of the ACM. 67 (5): 1–78. arXiv: 1704.01914 . doi:10.1145/3402029.
  19. Kolaitis, Phokion G.; Vardi, Moshe Y. (2000). "Conjunctive-Query Containment and Constraint Satisfaction". Journal of Computer and System Sciences . 61 (2): 302–332. doi: 10.1006/jcss.2000.1713 .
  20. Cai, Jin-Yi; Chen, Xi (2012). "Complexity of counting CSP with complex weights". Proceedings of the Forty-Fourth Annual ACM Symposium on Theory of Computing (STOC '12) . pp. 909–920. arXiv: 1111.2384 . doi:10.1145/2213977.2214059. ISBN   978-1-4503-1245-5. S2CID   53245129.
  21. Miguel, Ian (July 2001). Dynamic Flexible Constraint Satisfaction and its Application to AI Planning (Ph.D. thesis). University of Edinburgh School of Informatics. CiteSeerX   10.1.1.9.6733 . hdl:1842/326.
  22. Dechter, R. and Dechter, A., Belief Maintenance in Dynamic Constraint Networks Archived 2012-11-17 at the Wayback Machine In Proc. of AAAI-88, 37–42.
  23. Solution reuse in dynamic constraint satisfaction problems, Thomas Schiex
  24. Duffy, K.R.; Leith, D.J. (August 2013), "Decentralized Constraint Satisfaction", IEEE/ACM Transactions on Networking, 21(4), vol. 21, pp. 1298–1308, arXiv: 1103.3240 , doi:10.1109/TNET.2012.2222923, S2CID   11504393

Further reading