Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.3 4.3bsd-beta 6/6/85; site ucbvax.BERKELEY.EDU
Path: utzoo!decvax!ucbvax!OZ.AI.MIT.EDU!DAM
From: DAM@OZ.AI.MIT.EDU (David A. McAllester)
Newsgroups: mod.ai
Subject: TMS Query Response
Message-ID: <861016092006.2.DAM@ROCKY-GRAZIANO.LCS.MIT.EDU>
Date: Thu, 16-Oct-86 09:20:00 EDT
Article-I.D.: ROCKY-GR.861016092006.2.DAM
Posted: Thu Oct 16 09:20:00 1986
Date-Received: Sun, 19-Oct-86 04:20:19 EDT
References: <AI.PETRIE@MCC.COM>
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The ARPA Internet
Lines: 79
Approved: ailist@sri-stripe.arpa


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