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
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
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}.
{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.