Constraint logic programming: Difference between revisions

Revision as of 12:22, 8 March 2006

Revision as of 15:53, 8 March 2006

Line 1:

'''Constraint logic programming''' is a variant of [[logic programming]] including 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>A(X,Y) :- X+Y>0, B(X), C(Y)</code>. In this clause, <code>X+Y>0</code> is a constraint; <code>A(X,Y)</code>, <code>B(X)</code>, and <code>C(Y)</code> are literals like in regular logic programming. Intuitively, this clause tells one condition under which the statement <code>A(X,Y)</code> holds: this is the case if <code>X+Y</code> is greater than zero and both <code>B(X)</code> and <code>C(Y)</code> are true.

An example of a clause including a constraint is <code>A(X,Y) :- X+Y>0, B(X), C(Y)</code>. In this clause, <code>X+Y>0</code> is a constraint; <code>A(X,Y)</code>, <code>B(X)</code>, and <code>C(Y)</code> are literals like in regular logic programming. Intuitively, this clause tells one condition under which the statement <code>A(X,Y)</code> holds: this is the case if <code>X+Y</code> is greater than zero and both <code>B(X)</code> and <code>C(Y)</code> are true.

Like in regular logic programming, programs are queried about the provability of a goal. A proof for a goal is composed of clauses whose constraints are satisfied and whose literals can in turn be proved using other clauses. Execution is done 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 ''constraint store''. If this set is found out to be unsatisfiable, the interpreter [[Backtracking|backtrack]]s, trying to use other clauses for proving the goal. In practice, satisfiability of the constraint store is checked using a form of [[local consistency]], which does not always detect inconsistency. A complete check for satisfiability can be explicitely forced by using a specific literal.

Line 7 ⟶ 5:

==Overview==

Formally, constraint logic programs are like regular logic programs, but the body of clause can contain: constraints and labeling literals (described below), in addition to the regular logic programming literals.

# logic programming literals (the regular literals of logic programming)

# constraints

# labeling literals

DuringThe evaluation,semantics of constraint logic programs can be defined in terms of a virtual interpreter that maintains a pair <math>\langle G,S \rangle</math> isduring maintainedexecution. The first element of this pair is thecalled current goal; the second element is thecalled constraint store. The ''current goal'' contains the literals the interpreter is trying to prove; constraints and equality of terms are considered literals, so they can be presentoccur in the goal; the ''constraint store'' contains all constraints the interpreter has assumed satisfiable so far.

Initially, the current goal is the goal and the constraint store is empty. The interpreter proceed by iteratively removing the first element from the current goal and analyzing it. This analysis may resultend up in a failure,[[Recursion|recursive whichcall]] producesor a backtracking.failure; Thisthe analysisinterpreter backtracks in the second case. It may also introducegenerate an addition of new literals into frontthe current goal and an addition of new constraint to the goalconstraint orstore. newThe constraintsinterpreter instops when the current goal is empty and the constraint store is satisfiable.

More precisely, eachEach step of the algorithm is as follows. The first literal of the goal is considered and removed from the current goal. 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 of the literal is chosen; the clause is rewritten by replacing its variables with new variables (what is important is that these new variables do not already occur in the goal); the body of the clause is then placed in front of the goal; equalitiesthe equality of argumentseach argument of the literal andwith the corresponding one of the rewritten clause head areis placed in 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 should backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, a form of local consistency is checked instead.

Line 23 ⟶ 17:

When the current goal is empty, a regular logic program interpreter would stop and output the current substitution. In the same conditions, a constraint logic program also stops, and its output may be the current domains as reduced via the local consistency conditions on the constraint store. Actual satisfiability and finding a solution is enforced via labeling literals. In particular, whenever the interpreter encounters the literal <math>labeling(variables)</math> during the evaluation of a clause, it runs a satisfiability checker on the current constraint store to try and find a satisfying assignment.

ConstraintThe logicconstraints programs usually containof constraints fromlogic aprogramming givenare language.typically Inof thethree simplest case, the only consideredclasses: constraints are equality ofover terms; this corresponds to regular logic programming. Two other languages are also used:, constraints over reals, and constraints over finite domains, thewhich latterare beingusually identifiedinterpreted withas sets of integers.

==Reference==