5.4.4.2 Top-Down Implementation

The top-down implementation is similar to the top-down definite clause interpreter described in Figure 5.4, except the top-level goal is to prove false, and the assumables encountered in a proof are not proved but collected.

non-deterministic procedure ConflictTD(KB,Assumables)
2:           Inputs
3:                     KB: a set Horn clauses
4:                     Assumables: a set of atoms that can be assumed Output
5:                     A conflict
6:           Local
7:                     G is a set of atoms (that implies false)
8:           G←{false}
9:           repeat
10:                     select an atom ai from G such that ai ∉Assumables
11:                     choose clause C in KB with ai as head
12:                     replace ai in G by the atoms in the body of C
13:           until G⊆Assumables
14:           return G
Figure 5.10: Top-down Horn clause interpreter to find conflicts

The algorithm is shown in Figure 5.10. Different choices can lead to different conflicts being found. If no choices are available, the algorithm fails.

Example 5.23: Consider the representation of the circuit in Example 5.20. The following is a sequence of the values of G for one sequence of selections and choices that leads to a conflict:
{false}
{dark_l1,lit_l1}
{lit_l1}
{light_l1,live_l1, ok_l1}
{live_l1, ok_l1}
{live_w0, ok_l1}
{live_w1, up_s2, ok_s2, ok_l1}
{live_w3, up_s1, ok_s1, up_s2, ok_s2, ok_l1}
{live_w5, ok_cb1, up_s1, ok_s1, up_s2, ok_s2, ok_l1}
{live_outside, ok_cb1, up_s1, ok_s1, up_s2, ok_s2, ok_l1}
{ok_cb1, up_s1, ok_s1, up_s2, ok_s2, ok_l1}
{ok_cb1, ok_s1, up_s2, ok_s2, ok_l1}
{ok_cb1, ok_s1, ok_s2, ok_l1}.

The set {ok_cb1, ok_s1, ok_s2, ok_l1} is returned as a conflict. Different choices of the clause to use can lead to another answer.