Constraint logic programming: Difference between revisions

Revision as of 18:25, 9 March 2006

Revision as of 12:41, 10 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.

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 may be checked using an incomplete algorithm, which is one that does not always detect inconsistency.

==Overview==

Line 25:

===Tree terms===

InConstraint thelogic basicprogramming casewith oftree constraintterms reformulates regular logic programming, termswith substitutions stored as constraints in the constraint store. Terms are variables, constants, and functors applied to other terms. In this case, theThe only considered constraints are equalityequalities orand disequalitydisequalities between terms. Equality is particularly important, as constraints link <code>t1=t2</code> are often generated by the intepreter.

A constraint <code>t1=t2</code> can be simplified if both terms are functors applied to other terms. If the two functors are the same and the number of subterms is also the same, this constraint can be replaced with the pairwise equality of subterms. If the terms are composed of different functors or the same functor but on different number of terms, the constraint is unsatisfiable.

Line 50:

As for domains of reals, functors can be used with domains of integers. In this case, a term can be an expression over integers, a constant, or the application of a functor over other terms. A variable can take an arbitrary term as a value, if its ___domain has not been specified to be a set of integers or constants.

==The constraint store==

The constraint store contains the constraints that are currently assumed satisfiable. It can be considered what the current substitution is for regular logic programming. When only tree terms are allowed, the constraint store contains constraints in the form <code>t1=t2</code>; these constraints are simplified by unification, resulting in constraints of the form <code>variable=term</code>; such constraints are equivalent to a substitution.

However, the constraint store may also contain constraints in the form <code>t1!=t2</code>, if the difference <code>!=</code> between terms is allowed. When constraints over reals or finite domains are allowed, the constraint store may also contain ___domain-specific constraints like <code>X+2=Y/2</code>, etc.

The constraint store extends the concept of current substitution in two ways: first, it does not only contains the constraints derived from equating a literal with the head of a rewritten clause, but also the constraints of the body of clauses; second, it does not only contains constraints of the form <code>variable=value</code> but also constraints on reals or a finite ___domain, depending on the considered ___domain.

Domain-specific constraints may come to the constraint store both from the body of a clauses and from matching of a literals with a clause head: for example, if the interpreter rewrites the literal <code>A(X+2)</code> with a clause whose rewritten head is <code>A(Y/2)</code>, the constraint <code>X+2=Y/2</code> is added to the constraint store.

==Labeling==