Constraint logic programming: Difference between revisions

Revision as of 16:23, 9 November 2022

Revision as of 16:44, 14 October 2023

Line 4:

'''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 {{code|2=prolog|A(X,Y) :- X+Y>0, B(X), C(Y)}}. In this clause, {{code|2=prolog|X+Y>0}} is a constraint; <code>A(X,Y)</code>, <code>B(X)</code>, and <code>C(Y)</code> are [[Literal (mathematical logic)|literals]] as in regular logic programming. This clause states one condition under which the statement <code>A(X,Y)</code> holds: <code>X+Y</code> is greater than zero and both <code>B(X)</code> and <code>C(Y)</code> are true.

As in regular logic programming, programs are queried about the provability of a goal, which itself may contain constraints in addition to literals. A proof for a goal is composed of clauses whose bodies are satisfiable constraints and literals that can in turn be proved using other clauses. Execution is performed by an interpreter, which starts from the goal and [[Recursion|recursively]] scans the clauses trying to prove the goal. Constraints encountered during this scan are placed in a set called the '''constraint store'''. If this set is found out to be unsatisfiable, the interpreter [[Backtracking|backtracks]], trying to use other clauses for proving the goal. In practice, satisfiability of the constraint store may be checked using an incomplete algorithm, which does not always detect inconsistency.

==Overview==

Line 14:

A(X,Y):- X>0, B(X,Y).

</syntaxhighlight>

Like in regular logic programming, evaluating a goal such as <code>A(X,1)</code> requires evaluating the body of the last clause with <code>Y=1</code>. Like in regular logic programming, this in turn requires proving the goal <code>B(X,1)</code>. Contrary to regular logic programming, this also requires a constraint to be satisfied: <code>X>0</code>, the constraint in the body of the last clause. (inIn regular logic programming, X>0 cannot be proved unless X is bound to a fully [[ground term]] and execution of the program will fail if that is not the case).)

Whether a constraint is satisfied cannot always be determined when the constraint is encountered. In this case, for example, the value of <code>X</code> is not determined when the last clause is evaluated. As a result, the constraint <code>X>0</code> is notneither satisfied nor violated at this point. Rather than proceeding in the evaluation of <code>B(X,1)</code> and then checking whether the resulting value of <code>X</code> is positive afterwards, the interpreter stores the constraint <code>X>0</code> and then proceeds in the evaluation of <code>B(X,1)</code>; this way, the interpreter can detect violation of the constraint <code>X>0</code> during the evaluation of <code>B(X,1)</code>, and backtrack immediately if this is the case, rather than waiting for the evaluation of <code>B(X,1)</code> to conclude.

In general, the evaluation of a constraint logic program proceeds as does a regular logic program. However, constraints encountered during evaluation are placed in a set called a constraint store. As an example, the evaluation of the goal <code>A(X,1)</code> proceeds by evaluating the body of the first clause with <code>Y=1</code>; this evaluation adds <code>X>0</code> to the constraint store and requires the goal <code>B(X,1)</code> to be proven. While trying to prove this goal, the first clause is applied but its evaluation adds <code>X<0</code> to the constraint store. This addition makes the constraint store unsatisfiable. The interpreter then backtracks, removing the last addition from the constraint store. The evaluation of the second clause adds <code>X=1</code> and <code>Y>0</code> to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution <code>X=1, Y=1</code>.

Line 26:

Initially, the current goal is the goal and the constraint store is empty. The interpreter proceeds by removing the first element from the current goal and analyzing it. The details of this analysis are explained below, but in the end this analysis may produce a successful termination or a failure. This analysis may involve [[Recursion|recursive call]]s and addition of new literals to the current goal and new constraint to the constraint store. The interpreter backtracks if a failure is generated. A successful termination is generated when the current goal is empty and the constraint store is satisfiable.

The details of the analysis of a literal removed from the goal is as follows. After having removed this literal from the front of the goal, it is checked whether it is a constraint or a literal. If it is a constraint, it is added to the constraint store. If it is a literal, a clause whose head has the same predicate ofas the literal is chosen; the clause is rewritten by replacing its variables with new variables (variables not occurring in the goal): the result is called a ''fresh variant'' of the clause; the body of the fresh variant of the clause is then placed inat the front of the goal; the equality of each argument of the literal with the corresponding one of the fresh variant head is placed inat the front of the goal as well.

Some checks are done during these operations. In particular, the constraint store is checked for consistency every time a new constraint is added to it. In principle, whenever the constraint store is unsatisfiable the algorithm could backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, an incomplete satisfiability checker may be used instead. In practice, satisfiability is checked using methods that simplify the constraint store, that is, rewrite it into an equivalent but simpler-to-solve form. These methods can sometimes but not always prove unsatisfiability of an unsatisfiable constraint store.

Line 34:

Formally, the semantics of constraint logic programming is defined in terms of ''derivations''. A transition is a pair of pairs goal/store, noted <math>\langle G,S \rangle \rightarrow \langle G',S' \rangle</math>. Such a pair states the possibility of going from state <math>\langle G,S \rangle</math> to state <math>\langle G',S' \rangle</math>. Such a transition is possible in three possible cases:

* an element of {{mvar|G}} is a constraint {{mvar|C}}, and we have <math>G'=G \backslash \{C\}</math> and <math>S'=S \cup \{C\}</math>; in other words, a constraint can be moved from the goal to the constraint store

* an element of {{mvar|G}} is a literal <math>L(t_1,\ldots,t_n)</math>, there exists a clause that, rewritten using new variables, is <math>L(t_1',\ldots,t_n') \mathrel{{:}{-}} B</math>, the set <math>G'</math> is {{mvar|G}} with <math>L(t_1,\ldots,t_n)</math> replaced by <math>t_1=t_1',\ldots,t_n=t_n',B</math>, and <math>S'=S</math>; in other words, a literal can be replaced by the body of a fresh variant of a clause having the same predicate in the head, adding the body of the fresh variant and the above equalities of terms[[term (logic)|term]]s to the goal

* {{mvar|S}} and <math>S'</math> are equivalent according to the specific constraint semantics

Line 46:

The result of evaluating a goal against a constraint logic program is defined if the goal is proved. In this case, there exists a derivation from the initial pair to a pair where the goal is empty. The constraint store of this second pair is considered the result of the evaluation. This is because the constraint store contains all constraints assumed satisfiable to prove the goal. In other words, the goal is proved for all variable evaluations that satisfy these constraints.

The pairwise equality of termsthe arguments of two literals is often compactly denoted by <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math>: this is a shorthand for the constraints <math>t_1=t_1',\ldots,t_n=t_n'</math>. A common variant of the semantics for constraint logic programming adds <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> directly to the constraint store rather than to the goal.

==Terms and conditions==

Line 180:

==Applications==

Constraint logic programming has been applied to a number of fields, such as [[Automated planning and scheduling|automated scheduling]],<ref>Abdennadher, Slim, and Hans Schlenker. "[https://www.aaai.org/Papers/IAAI/1999/IAAI99-118.pdf?q=optimal-scheduling-using-constraint-logic-programming Nurse scheduling using constraint logic programming]." [[AAAI]]/IAAI. 1999.</ref> [[type inference]],<ref>Michaylov, Spiro, and [[Frank Pfenning]]. "[http://www.cs.cmu.edu/Groups/fox/people/fp/papers/ppcp93.pdf Higher-Order Logic Programming as Constraint Logic Programming]." PPCP. Vol. 93. 1993.</ref> [[civil engineering]], [[mechanical engineering]], [[digital circuit]] verification, [[air traffic control]], finance, and others.{{citation needed|date=September 2020}}

==History==

Constraint logic programming was introduced by Jaffar and Lassez in 1987.<ref>Jaffar, Joxan, and J-L. Lassez. "[https://dl.acm.org/citation.cfm?id=41635 Constraint logic programming]." Proceedings of the 14th [[ACM SIGACT-SIGPLAN-SIGACT symposiumSymposium on Principles of programmingProgramming languagesLanguages]]. ACM, 1987.</ref> They generalized the observation that the term equations and disequations of [[Prolog II]] were a specific form of constraints, and generalized this idea to arbitrary constraint languages. The first implementations of this concept were [[Prolog III]], [[CLP(R)]], and [[CHIP (programming language)|CHIP]].{{citation needed|date=August 2019}}

==See also==

*[[BPrologB-Prolog]]

*[[BNR Prolog]] (aka CLP(BNR))

*[[Constraint Handling Rules]]

Line 202:

| first=Rina

| last=Dechter

|authorlink = Rina Dechter

| title=Constraint processing

| publisher=Morgan Kaufmann

Line 242 ⟶ 243:

|author2=Michael J. Maher

| title=Constraint logic programming: a survey

| journal=[[Journal of Logic Programming]]

| volume=19/20

| pages=503–581