Any normal logic program with constraints can be translated into a boolean formula using Clark's completion. The resulting formula be rewritten to be in Conjunctive Normal Form (CNF) so it can easily be processed by a SAT-solver. In case the logic program is tight, the models of the SAT encoding coincide with the answer sets of the logic program.



Clark's Completion for a normal logic program with integrity constraints
I assume that the reader is familiar with normal logic programs with integrity constraints in lparse syntax. I use these symbol & to denote the boolean logic AND, the symbol | to denote boolean logic OR, the symbol - to denote boolean NEGATION (NOT the negation as failure operator not) and the smbol = to denote boolean logic EQUIVALENCE. The symbol T denotes boolean TRUE, F boolean FALSE.

To form Clark's completion for a logic program do the following:

  1. Replace all rules with the same head

    head :- a, b, c, not d, not e, ....
    head :- f, g, h, not i, not j, ....
    head.
    ...

    by the logic formulas

    head = (a & b & c & -d & -e & ...) | ( f & g & h & -i & -j & ...) | T | ...
  2. Replace all integrity constraints like

    :- a, b, not c, not d, ...

    by the logic formula

    F = a & b & -c & -d & ...
  3. Combine all the formulas created using the boolean logic connective AND.

What happened is we made each head of a rule logically equal to the disjunction of its bodies. The notion of the logic equivalence (=) in Clark's Completion is this:

  • if at least one of its bodies is true, so must be the head (a rule could be applied),
  • if the head is true, then at least one body must be true (find the rule(s) that made the head true),
  • if all the bodies are false, so must be the head (no rule derives the head),
  • if the head is false, all of its bodies must be false as well (all rules must be cancelled).

Because the the translation of a logic program as given above is quite cumbersome to read, we use a different one that is a little bit easier on the eyes. Here it goes:

  1. Replace all rules with the same head

    head :- a, b, c, not d, not e, ...
    head :- f, g, h, not i, not j, ...
    head.
    ...

    by the logic formulas

    body1 = a & b & c & -d & -e & ...
    body2 = f & g & h & -i & -j & ...
    body3 = T.
    head = body1 | body2 | body3 | ...
  2. Replace all integrity constraints like

    :- a, b, not c, not d, ...

    by the logic formula

    F = a & b & -c & -d & ...
  3. Combine all the formulas created using the boolean logic connective AND.

Basically what we've done is we abbreviated the body literals of a rule using a new atom.

Rewriting Clark's Completion to Conjunctive Normal Form (CNF)
Because SAT-Solvers usually read in a formula in Conjunctive Normal Form (CNF), we need to rewrite the completion to CNF. A formula in CNF looks like this:

(a | b | ...) & (c | -d) & (-a | -c | ...) & ...

The disjunction (|) of the literals in the braces are called clauses. CNF is really nothing else but a conjunction (&) of clauses. When done translating a logic program into a boolean formula using any of the translation schemes described earlier, the final formula looks like this:

A & B & C & ....

where each of the A, B, C, ... is a subformula which we may need to rewrite to CNF.

If the subformula is T, it can safely be dropped because it has no effect on the overall satisfiability of the formula because X connected to true using boolean AND yields X.

If the subformula is an equivalence h = a & b & -c & ... then rewrite it into two implications connected with AND connective. The symbol -> denotes the boolean implication.

(h -> a & b & -c & ...) &
(a & b & -c & ... -> h)

The two implications are then rewritten using the standard rewrite rule for implications into disjunctions: a -> b is logically equivalent to -a | b.

(-h | (a & b & -c & ...)) &
(-(a & b & -c & ...) | h)

The resulting formulas can be simplified to yield

((-h | a) & (-h | b) & (-h | -c) & (-h | ...)) &
(-a | -b | c | -(...) | h)

This in turn yields

(-h | a) & (-h | b) & (-h | -c) & (-h | ...) & (-a | -b | c | -(...) | h)

Now we have successfully rewritten an equivalence into CNF. Note, if the equivalence is F = a & b & -c & ... then the resulting formula can be simplified to

-a | -b | c | -(...)

Last but not least if the subformula is h = a | b | -c | ... rewriting to CNF works analogous. First, replace the logic equivalence by two implications connected with AND.

(h -> a | b | -c | ...) &
((a | b | -c | ...) -> h)

Now rewrite the implications into disjunctions.

(-h | (a & b & -c & ...)) &
(-(a | b | -c | ...) | h)

Simplify the disjunctions.

((-h | a) & (-h | b) & (-h | -c) & (-h | ...)) &
((-a | h) & (-b | h) & (c | h) & (-(...) | h))

Which yields CNF.

(-h | a) & (-h | b) & (-h | -c) & (-h | ...) & (-a | h) & (-b | h) & (c | h) & (-(...) | h)

 

Tightness of a normal logic program
A model for the SAT encoding obtained by applying Clark's Completion for a logic program does not necessarily represent an answer set of the program. This is because the positive dependency graph of the logic program may contain cycles. If the positive dependency graph is a directed acyclic graph (DAG), the logic program is called tight. In this case the models of the completion of the logic program represent answer sets.

The positive dependency graph of a logic program be obtained by dropping all negative literals from all rules and then constructing the dependency graph for each atom in the logic program. If this graph is a DAG, the logic program is tight.