[mod.ai] TMS Query Response

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