AI.PETRIE@MCC.COM (Charles Petrie) (09/29/86)
More detail on Don Rose's TMS query: Does anyone know whether the standard algorithms for belief revision (e.g. dependency-directed backtracking in TMS-like systems) are guaranteed to halt? That is, is it possible for certain belief networks to be arranged such that no set of mutually consistent beliefs can be found (without outside influence)? There are at least three distinct Doyle-style algorithms. Doyle's doesn't terminate on unsatisfiable cicularities. James Goodwin's algorithm does. This algorithm is proved correct in "An Improved Algorithm for Non-monotonic Dependency Net Update", LITH-MAT-R-82-23, Linkoping Institute of Technology. David Russinoff's algorithm not only halts given an unsatisfiable circularity, but is guaranteed to find a well-founded, consistent set of status assignments, even if there are odd loops, if such a set is possible. There are dependency nets for which Russinoff's algorithm will properly assign statuses and Goodwin's may not. An example and proof of correctness for this algorithm is given in "An Algorithm for Truth Maintenance", AI-068-85, Microelectronics and Computer Technology Corporation. Also, Doyle made the claim that an unsatisfiable circularity can be detected if a node is its own ancestor after finding a valid justification with a NIL status in the Outlist. Detection of unsatisfiable circularities turns out to be more difficult than this. This is noted in "A Diffusing Computation for Truth Maintenance" wherein I give a distributed computation for status assignment (published in the Proc. 1986 Internat. Conf. on Parallel Processing, IEEE) that halts on unsatisfiable circularities. The term "unsatisfiable circularity" was introduced by Doyle and refers to a dependency network that has no correct status labeling. The term "odd loop" was introduced by Charniak, Riesbeck, and McDermott in section 16.7 of "Artificial Intelligence Programming". An equivalent definition is given by Goodwin. In both, an odd loop refers to a particular circular path in a dependency net. As Goodwin notes, such odd loops are a necessary, but not sufficient, condition for an unsatisfiable circularity. All of the algorithms mentioned above are for finding a proper set of status assignments for a dependency network. A distinct issue is the avoidance of the creation of odd loops, which may introduce unsatisfiable circularities, by Doyle-style dependency-directed backtracking. Examples of creation of such odd loops and algorithms to avoid such are described in my technical reports on DDB. Michael Reinfrank's report on the KAPRI system also notes the possibility of odd loops created by DDB. (DDB references on request to avoid an even longer note.) Charles Petrie PETRIE@MCC -------
DAM@OZ.AI.MIT.EDU (David A. McAllester) (10/16/86)
I saw a recent message concerning the termination of belief revision in a Doyle-style TMS. Some time ago I proved that determining the existence of a fixed point for a set of Doyle justifications is NP-complete. It is possible to give a procedure that terminates but all such procedures will have exponential worst case behaviour. The proof is given below: *********************************************************** DEFINITIONS: A NM-JUSTIFICATION is an "implication" of the form: (IN-DEPENDENCIES, OUT-DEPENDENCIES) => N where IN-DEPENDENCIES and OUT-DEPENDENCIES are sets of nodes and N is the justified node. A labeling L marks every node as either "in" or "out". An nm-justification is said to be "active" under a labeling L if every out dependency in the justification is labeled "out" and every in dependency of the justification is labeled "in". Let J be a set of nm-justifications and L be a labeling. We say that a node n is JUSTIFIED under J and L if there is some justification for n which is active under the labeling L. A set J of nm-justifications will be called Doyle Satisfiable if there is a labeling L such that every justified node is "in" and every node which is not justified is "out". ******************* THEOREM: The problem of determining the Doyle satisfiability of a set J of nm-justifications is NP-complete. ******************* PROOF: PSAT can be reduced to Doyle satisfiability as follows: Let C be any set of propositional clauses (i.e. a problem in PSAT). For each atomic proposition symbol P appearing in C let P and nP be two nodes and construct the following justifications: ({}, {nP}) => P (i.e. if nP is "out" then P is justified) ({}, {P}) => nP (i.e. if P is "out" then nP is justified) We introduce an additional node F (for "false") and for each clause (L1 or L2 ... or LN) in C we construct the justification: ({nL1, nL2, ... nLn} {F}) => F where the node nLj is the node nP if Lj is the symbol P and nLj is the node P if Lj is the literal (NOT P). The set J of nm-justifications constructed in this way is Doyle-Satisfiable iff the original set C is propositionally satisfiable. To verify this last claim note that if L is a labeling which satisfies J then exactly one of P and nP is "in"; if P is "out" then nP must be "in" and vice versa, and if P is "in" then nP must be "out" and vice versa. Next note that if L is a labeling satisfying J then F must be "out"; if F were "in" then no justification for F would be active contradicting the requirement that F is not justified then F is not "in". Finally note that a labeling L satisfies J just in case none of the justifications for F are active, i.e. just in case the corrosponding truth assignment to the proposition symbols in C satisfies every clause. ************** David McAllester