1: %% Searched string: {}

2: \typeout{}

3: \typeout{Compilability of Abduction}

4: \typeout{}

5: 

6: \documentclass[12pt]{article}

7: 

8: \usepackage{latexsym}

9: % \usepackage{proof}

10: 

11: %%%%%%%%%%%%% macros %%%%%%%%%%%%%%

12: %%%%%%%%%%%%%%%%%%%%%%%%%% Miscellaneous

13: 

14: \long\def\nop#1{}

15: \long\def\nota#1{\marginpar{\tiny #1}}

16: 

17: \def\comment{\edef\cps{\the\parskip} \parskip=0.5cm \begingroup \tt}

18: \def\endcomment{\endgroup \vskip 0.5cm \parskip=\cps}

19: \def\separator{\vskip 1cm\hrule\vskip 1cm}

20: 

21: \hyphenation{Ca-do-li Do-ni-ni Li-be-ra-to-re}

22: 

23: 

24: % se \shortcite non e' definito, lo definisce come \cite

25: 

26: \expandafter\ifx\csname shortcite\endcsname\relax

27: \let\shortcite=\cite

28: \fi

29: 

30: 

31: % framebox

32: 

33: \newbox\current

34: 

35: \long\def\plframebox#1{

36: \setbox\current\vbox{#1}		% set box

37: 

38: \vbox to \ht\current {\hrule\vss

39: \hbox to \wd\current {%

40: \vrule \hss\box\current\hss \vrule}

41: \vss\hrule }

42: }

43: 

44: % \hrule width\wd\current

45: % \vrule height\ht\current

46: 

47: 

48: % mangia i par

49: 

50: \long\def\eatpar#1{%

51: \ifx#1\par                      % se il token e' \par

52: \let\nextmove=\eatpar           % rimetti \eatpar in coda

53: \else

54: \let\nextmove=#1%               altrimenti, rimetti il token in coda

55: \fi

56: \noexpand\nextmove%             il token o \eatpar viene rimesso in coda

57: }

58: 

59: 

60: % modifica i margini

61: 

62: \def\modifymargins#1#2{

63: \newdimen\addtoh

64: \newdimen\addtow

65: \addtoh=#1

66: \addtow=#2

67: 

68: \advance\topmargin by -\addtoh

69: \multiply\addtoh by 2

70: \advance\textheight by \addtoh

71: 

72: \advance\oddsidemargin by -\addtow

73: \advance\evensidemargin by -\addtow

74: \multiply\addtow by 2

75: \advance\textwidth by \addtow

76: }

77: 

78: 

79: % tilde per gli indirizzi www

80: 

81: \begingroup

82: \catcode`\~=11

83: \gdef\centertilde#1{\lower #1pt\hbox{~}}

84: \endgroup

85: 

86: 

87: % ora corrente

88: 

89: \newcount\currenttime

90: \newcount\hour

91: \newcount\minute

92: 

93: \def\printtime{%

94: \currenttime=\time

95: \hour=\currenttime

96: \divide\hour by 60

97: \minute=-\hour

98: \multiply\minute by 60

99: \advance\minute by \currenttime

100: \the\hour:\ifnum\minute<10 0\fi\the\minute

101: }

102: 

103: 

104: % mette l'ora nella data che appare sotto il titolo

105: 

106: \begingroup

107: \makeatletter

108: \global\let\@@date=\@date

109: \gdef\@date{\@@date\ --- \printtime}

110: \endgroup

111: 

112: 

113: % oggi

114: 

115: \def\oggi{\number\day\space 

116: \ifcase\month\or

117: Gennaio\or Febbraio\or Marzo\or Aprile\or Maggio\or Giugno\or

118: Luglio\or Agosto\or Settembre\or Ottobre\or Novembre\or Dicembre\fi

119: \space \number\year}

120: 

121: 

122: % riga vuota

123: 

124: \def\riga{\vskip 1\baselineskip \noindent}

125: 

126: \newcounter{rmexample}

127: 

128: \newenvironment{rmexample}

129: {\addtocounter{rmexample}{1}

130: \medskip

131: \noindent{\bf Example~\thermexample}:}{\ifhmode\nobreak{\raisebox{-.2ex}{$\Diamond$}}\par\fi\smallskip}

132: 

133: \def\proof{\noindent {\sl Proof.\ \ }}

134: \def\proofsketch{{\sl Proof (sketch).\ \ }}

135: \def\proofof#1{{\sl Proof of #1.}}

136: 

137: \def\qed{\hfill{\boxit{}}

138:   \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}

139: \def\qedn#1{\hfill{\boxit{}$_#1$}

140:   \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}

141: \long\def\boxit#1{\vbox{\hrule\hbox{\vrule\kern3pt

142:                   \vbox{\kern3pt#1\kern3pt}\kern3pt\vrule}\hrule}}

143: 

144: \def\ovl#1{\overline{#1}}

145: 

146: 

147: %%%%%%%%%%%%%%%%%%%%%%%%%% General Math

148: 

149: \def\calA{{\cal A}} \def\B{{\cal B}} \def\D{{\cal D}}

150: \def\E{{\cal E}} \def\F{{\cal F}} \def\G{{\cal G}} \def\H{{\cal H}}

151: \def\I{{\cal I}} \def\J{{\cal J}} \def\K{{\cal K}} \def\L{{\cal L}}

152: \def\M{{\cal M}} \def\N{{\cal N}} \def\O{{\cal O}} \def\calP{{\cal P}}

153: \def\Q{{\cal Q}} \def\R{{\cal R}} \def\calS{{\cal S}} \def\T{{\cal T}}

154: \def\U{{\cal U}} \def\V{{\cal V}} \def\W{{\cal W}} \def\X{{\cal X}}

155: \def\Y{{\cal Y}} \def\Z{{\cal Z}}

156: 

157: %%%%%%%%%%%%%%%%%%%%%%%%%% Abbreviations

158: 

159: \def\eset{\emptyset}

160: \def\col{\colon}

161: \def\ol#1{\overline{#1}}                % overline

162: \def\ul#1{\underline{#1}}               % underline

163: \def\uls#1{\underline{\raisebox{0pt}[0pt][0.45ex]{}#1}} % underline with space

164: \def\iff{if and only if}

165: \def\kb{k.b.}

166: \def\ie{i.e.}

167: \def\eg{e.g.}

168: \def\wrt{w.r.t.}

169: \def\aka{a.k.a.}

170: %\def\wlog{w.l.o.g.}

171: 

172: %%%%%%%%%%%%%%%%%%%%%%%%%% Relations

173: 

174: \def\incl{\subseteq}

175: \def\imp{\Rightarrow}

176: \def\imply{\rightarrow}

177: \def\deq{\doteq}

178: \def\defas{\doteq}                      % defined as

179: \def\dleq{\dot{\leq}}                   % dotted less equal

180: \def\finimpl{\models_{fin}}             % finitely implies

181: \def\subsumed{\sqsubseteq}              % subsumed by

182: 

183: %%%%%%%%%%%%%%%%%%%%%%%%%% Minimal Sets

184: 

185: \def\setdiff{\Delta}

186: \def\mindiff{\delta}    %  proposta; si accettano simboli migliori

187: \def\minTdiff{\mu}      %  idem

188: \def\minset{min_\subseteq}  %% come Eiter, Gottlob 92

189: \def\M{{\cal M}}

190: \def\F{{\cal F}}

191: \def\form{form}

192: \def\card#1{card(#1) }

193: 

194: %%%%%%%%%%%%%%%%%%%%%%%%%% Spaces

195: 

196: \def\asp{\makebox[3pt]{}}       % arrow space, put before and after arrows

197: \def\osp{\hskip1pt}             % operator space, put before and after ops

198: \def\asps#1{{\asp#1\asp}}

199: \def\osps#1{{\osp{#1}\osp}}

200: \def\qland{\;\;\land\;\;}

201: 

202: \def\con{\asp\asp\&\asp}

203: % Incompatibile con LaTex2e

204: % \def\sbox{\vbox{\hrule

205: %                \hbox{\vrule\hskip4pt\vbox{\vskip4pt}\vrule}

206: %                \hrule}}

207: 

208: \def\per{\mbox{\bf .}}                  % period

209: 

210: \def\cld{,\ldots,}                      % ,...,

211: \def\ld#1{#1 \ldots #1}                 % #1 ... #1

212: \def\cd#1{#1 \cdots #1}                 % #1 ... #1

213: \def\lds#1{\, #1 \; \ldots \; #1 \,}    % _#1_..._#1_

214: \def\cds#1{\, #1 \; \cdots \; #1 \,}    % _#1_..._#1_

215: \def\dd#1#2{#1_1,\ldots,#1_{#2}}        % da da, makes x1,...,xn

216: 

217: %%%%%%%%%%%%%%%%%%%%%%%%%% Delimiters

218: 

219: \def\quotes#1{{\lq\lq#1\rq\rq}}         % quote

220: \def\braces#1{$\{$ #1 $\}}              % braces

221: \def\set#1{\{#1\}}                      % set

222: \def\Set#1{\left\{ #1 \right\}}

223: \def\bigset#1{ \Bigl\{ #1 \Bigr\} }

224: \def\bigmid{\ \Big|\ }                  % mid

225: \def\card#1{|{#1}|}                     % cardinality of a set

226: \def\Card#1{\left| #1 \right|}

227: \def\cards#1{\sharp #1}

228: \def\sub#1{[#1]}                        % [ #1 ]

229: \def\tup#1{\langle #1 \rangle}          % tuple < #1 >

230: \def\Tup#1{\left\langle #1 \right\rangle}

231: \def\l{\langle}

232: \def\r{\rangle}

233: \newcommand{\pair}[2]{\langle #1, #2 \rangle}

234: 

235: \def\If{\lq\lq$\Leftarrow$\rq\rq\ \ }           % 1st direction of iff-proof

236: \def\OnlyIf{\lq\lq$\Rightarrow$\rq\rq\ \ }      % 2nd direction of iff-proof

237: 

238: %%%%%%%%%%%%%%%%%%%%%%%%%% Constraints

239: 

240: \def\relc#1#2#3{#1#2#3}

241: %\def\inc#1#2{#1 \!:#2}

242: \def\inc#1#2{#1\col#2}

243: 

244: %%%%%%%%%%%%%%%%%%%%%%%%%% General Commands

245: 

246: 

247: 

248: %%%%%%%%%%%%%%%%%%%%%%%%%% Programs

249: 

250: \def\pwhile{{\tt while ~}}

251: \def\pfor{{\tt for ~}}

252: \def\pforeach{{\tt foreach ~}}

253: \def\pto{{\tt ~ to ~}}

254: \def\pdo{{\tt ~ do ~ }}

255: 

256: \def\pif{{\tt if ~ }}

257: \def\pthen{{\tt ~ then ~ }}

258: \def\pelse{{\tt ~ else ~ }}

259: \def\por{{\tt ~ or ~ }}

260: \def\pand{{\tt ~ and ~ }}

261: 

262: \def\pbegin{{\tt begin}}

263: \def\pend{{\tt end}}

264: 

265: \def\pret{{\tt return ~}}

266: \def\ptrue{{\tt true}}

267: \def\pfalse{{\tt false}}

268: 

269: \def\pind{~~~}

270: 

271: %%%%%%%%%%%%%%%%%%%%%%%%%% Interpretation

272: 

273: \def\mod{M\!od}

274: \def\form{F\!orm}

275: \def\var{V\!ar}

276: \def\diff{Di\!f\!f}

277: \def\dist{\mbox{{\sc dist}}}

278: 

279: %%%%%%%%%%%%%%%%%%%%%%%%%% Concept forming operators

280: 

281: \def\OR{\sqcup}

282: \def\NOT{\neg}

283: \def\ALL#1#2{\forall #1 \per #2}

284: \def\SOME#1#2{\exists #1 \per #2}

285: \def\SOMET#1{\exists #1}

286: \def\ALLRC{\ALL R C}

287: \def\SOMERC{\SOME R C}

288: \def\SOMERT{\SOMET R}

289: \def\ATLEAST#1#2{(\geq #1 \, #2)}

290: \def\ATMOST#1#2{(\leq #1 \, #2)}

291: \def\EXACTLY#1#2{(= #1 \, #2)}

292: \def\INV#1{#1^{-1}}

293: 

294: \def\Atmost#1#2{A_{(\leq #1 \, #2)}}

295: \def\Atleast#1#2{A_{(\geq #1 \, #2)}}

296: 

297: %%%%%%%%%%%%%%%%%%%%%%%%%% PDL forming operators

298: 

299: \def\true{{\sf true}}

300: \def\false{{\sf false}}

301: \def\Not{\neg}

302: \def\Or{\vee}

303: \def\Implies{\rightarrow}

304: \def\Diam#1#2{\langle #1 \rangle #2}

305: \def\DiamT#1{\langle #1 \rangle \true}

306: \def\Boxx#1#2{[#1]#2}

307: \def\Inv#1{#1^{-}}

308: \def\Star#1{#1^{\ast}}

309: \def\Comp{;}

310: \def\Choice{\cup}

311: 

312: \def\AllR{\Star{(\cup_i R_i)}}

313: 

314: %%%%%%%%%%%%%%%%%%%%%%%%%% Complexity Classes

315: 

316: \def\C{{\rm C}}

317: \def\nc{{\rm NC}}

318: \def\p{{\rm P}}

319: \def\np{{\rm NP}}

320: \def\conp{{\rm coNP}}

321: \def\Dp{${\rm D}^p$}

322: \def\S#1{\mbox{$\Sigma^p_{#1}$}}

323: \def\P#1{$\Pi^p_{#1}$}

324: \def\D#1{\mbox{$\Delta^p_{#1}$}}

325: \def\Dlog#1{\mbox{$\Delta^p_{#1}[\log n]$}}

326: \def\PH{{\rm PH}}

327: \def\poly{{\rm poly}}

328: \def\pp{{\rm PP}}

329: \def\copp{{\rm co\pp}}

330: \def\nppp{$\np^\pp$}

331: 

332: \def\FC{\mbox{\rm FC}}

333: \def\leqFC{\leq^{\rm FC}}

334: 

335: \def\pspace{{\rm PSPACE}}

336: \def\logspace{{\rm LOGSPACE}}

337: \def\exptime{\mbox{\rm EXPTIME}}

338: 

339: %%%%%%%%%%%%%%%%%%%%%%%%%% Compilability Classes

340: 

341: \def\c{$\leadsto$}

342: 

343: \def\cC{\c{\rm C}}

344: \def\cp{\c{\rm P}}

345: \def\cnp{{\rm compNP}}

346: \def\cconp{{\rm compcoNP}}

347: \def\cDp{${\rm compD}^p$}

348: \def\cS#1{comp$\Sigma^p_#1$}

349: \def\cP#1{comp$\Pi^p_#1$}

350: \def\cD#1{comp$\Delta^p_#1$}

351: \def\cDlog#1{comp$\Delta^p_#1[\log n]$}

352: 

353: \def\cpspace{{\rm compPSPACE}}

354: \def\clogspace{{\rm compLOGSPACE}}

355: 

356: \def\nuc#1{\mbox{$\parallel\!\leadsto$#1}}

357: 

358: \def\nucC{\nuc{\rm C}}

359: \def\nucp{\nuc{\rm P}}

360: \def\nucnp{\nuc{\rm NP}}

361: \def\nucconp{\nuc{\rm coNP}}

362: \def\nucS#1{\nuc{$\Sigma^p_{#1}$}}

363: \def\nucP#1{\nuc{$\Pi^p_{#1}$}}

364: \def\nucD#1{\nuc{\D{#1}}}

365: \def\nucDp{\nuc\Dp}

366: \def\nucDlog#1{{\rm nucomp}\Dlog{#1}}

367: 

368: \def\comp{\leq_{comp}}

369: \def\nucomp{\leq_{nucomp}}

370: 

371: \def\ep#1{*#1}

372: 

373: %%%%%%%%%%%%%%%%%%%%%%%%%% FPT Classes

374: 

375: \def\fpt{\mbox{\rm FPT}}

376: \def\ufpt{\mbox{\rm uFPT}}

377: \def\sufpt{\mbox{\rm suFPT}}

378: \def\nufpt{\mbox{\rm nuFPT}}

379: 

380: %%%%%%%%%%%%%%%%%%%%%%%%%% Succinctness Classes	

381: 

382: \def\mC{{\rm model-C}}

383: \def\tC{{\rm thm-C}}

384: 

385: \def\mC{{\rm model-C}}                 % Model checking e' C

386: \def\mP{{\rm model-P}}                 % Model checking e' P

387: \def\mNP{{\rm model-NP}}               % Model checking e' NP

388: \def\mcoNP{{\rm model-coNP}}           % Model checking e' coNP

389: \def\mS#1{{\rm model-}$\Sigma^p_{#1}$}

390: \def\mPi#1{{\rm model-}$\Pi^p_{#1}$}

391: 

392: \def\tC{{\rm thm-C}}                 % Inference e' C

393: \def\tP{{\rm thm-P}}                 % Inference e' P

394: \def\tNP{{\rm thm-NP}}               % Inference e' NP

395: \def\tcoNP{{\rm thm-coNP}}           % Inference e' coNP

396: \def\tS#1{{\rm thm-}$\Sigma^p_{#1}$}

397: \def\tPi#1{{\rm thm-}$\Pi^p_{#1}$}

398: 

399: 

400: \def\diventa{\mapsto} 

401: 

402: 

403: %%%%%%%%%%%%%%%%%%%%%%%%%% Problems

404: 

405: \def\profont{\sf}

406: 

407: \def\sat{{\profont sat}}

408: \def\unsat{{\profont unsat}}

409: \def\qbf{{\rm QBF}}

410: \def\maxlexmod{{\profont maxlexmod}}

411: \def\minlexmod{{\profont minlexmod}}

412: \def\infncirc{{\profont infncirc}}

413: \def\critsat{{\profont critsat}}

414: \def\threesat{{\profont 3sat}}

415: \def\threeunsat{{\profont 3unsat}}

416: \def\threecolor{{\profont 3colorability}}

417: \def\clique{{\profont clique}}

418: \def\vc{{\profont vc}}

419: \def\gi{{\profont gi}}

420: \def\sgi{{\profont sgi}}

421: \def\hc{{\profont hc}}

422: \def\shc{{\profont shc}}

423: \def\md{{\profont md}}

424: \def\cq{{\profont cq}}

425: \def\rp{{\profont rp}}

426: \def\nf{{\profont nf}}

427: \def\st{{\profont st}}

428: \def\ec{{\profont ec}}

429: \def\x3c{{\profont x3c}}

430: \def\threecnf{{\profont 3cnf}}

431: \def\ci{{\profont ci}}

432: \def\mmc{{\profont mmc}}

433: \def\finf{{\profont fi}}

434: \def\epssat{$\epsilon$\threesat}

435: \def\diagn{{\profont diagn}}

436: \def\strips{{\profont STRIPS}}

437: \def\ibr{{\profont ibr}}

438: \def\mbt{{\profont mbt}}

439: \def\irr{{\profont irr}}

440: 

441: 

442: %%%%%%%%%%%%%%%%%%%%%%%%%% Theorems

443: 

444: \def\possnewtheorem#1#2{

445: \expandafter\ifx\csname #1\endcsname\relax

446: \newtheorem{#1}{#2}

447: \fi

448: }

449: 

450: \def\possnewtheoremthree#1[#2]#3{

451: \expandafter\ifx\csname #1\endcsname\relax

452: \newtheorem{#1}[#2]{#3}

453: \fi

454: }

455: 

456: \possnewtheorem{theorem}{Theorem}

457: \possnewtheorem{corollary}{Corollary}

458: \possnewtheorem{lemma}{Lemma}

459: \possnewtheoremthree{proposition}[theorem]{Proposition}

460: \possnewtheorem{definition}{Definition}

461: \possnewtheorem{question}{Question}

462: \possnewtheorem{example}{Example}

463: \possnewtheorem{property}{Property}

464: \possnewtheorem{assumption}{Assumption}

465: \possnewtheorem{conjecture}{Conjecture}

466: \newenvironment{theorem*}[1]{{\noindent \bf Theorem~#1}\begin{it}}{\end{it}\

467: 

468: }

469: 

470: %%%%%%%%%%%%%%%%%%%%%%%%%% Revision & Update

471: 

472: \def\agm#1{{\sc agm#1}}

473: \def\km#1{{\sc km#1}}

474: \def\leh#1{{\sc leh#1}}

475: 

476: \def\ginsberg{*_G}

477: \def\fuv{*_{FUV}}

478: \def\satoh{*_S}

479: \def\dalal{*_D}

480: \def\winslett{*_W}

481: \def\borgida{*_B}

482: \def\forbus{*_F}

483: \def\ssu{*_{SSU}}

484: \def\weber{*_{W\!eb}}

485: \def\hegner{*_{H}}

486: \def\widtio{*_{Wit}}

487: \def\revesz{*_{R}}

488: \def\up{*_{UP}}

489: \def\fm{*_{FM}}

490: 

491: \let\texcirc=\circ

492: \def\circ{C\!I\!RC}

493: \def\ncirc{\mbox{{\sc ncirc}}}

494: \newcommand{\deftheory}[2]{\langle #1, #2 \rangle}

495: % Comando per un default PF normale

496: \def\defaultone#1{\frac{~:#1}{#1}}

497: % Comando per un default normale

498: \def\defaulttwo#1#2{\frac{#1:#2}{#2}}

499: % Comando per un default qualsiasi

500: \def\defaultthree#1#2#3{\frac{#1:#2}{#3}}

501: \def\anr{*_{ANR}}

502: \def\nat{*_{NR}}

503: \def\ocf{{\sc ocf}}

504: \def\cond{*_{CT}}

505: \def\adj{*_{AT}}

506: \def\rr#1{*_{RR(#1)}}

507: \def\pr#1{*_{PR(#1)}}

508: 

509: \def\ranking#1{\kappa_{[T;P_1,\ldots,P_{#1}]}}

510: 

511: %%%%%%%%%%%%%%%%%%%%%%%%%% RAA

512: 

513: \def\A{$\cal{A}$}

514: 

515: \def\init#1{~{\sf initially}~#1}

516: \def\after#1#2{#1~{\sf after}~#2}

517: \def\causes#1#2{#1~{\sf causes}~#2}

518: \def\causesif#1#2#3{#1~{\sf causes}~#2~{\sf if}~#3}

519: 

520: %%%%%%%%%%%%%%%%%%%%%%%%%%

521: 

522: %\def\SetFigFont#1#2#3{}

523: 

524: 

525: 

526: \let\shortcite=\cite

527: 

528: \title{Compilability of Abduction}

529: \author{Paolo Liberatore\\

530: \normalsize Dipartimento di Informatica e Sistemistica\\

531: \normalsize Universit\`a di Roma ``La Sapienza''\\

532: \normalsize Via Salaria 113, 00198 Roma - Italy\\

533: \normalsize Email: {\tt paolo@liberatore.org}

534: \and Marco Schaerf\\

535: \normalsize Dipartimento di Informatica e Sistemistica\\

536: \normalsize Universit\`a di Roma ``La Sapienza''\\

537: \normalsize Via Salaria 113, 00198 Roma - Italy\\

538: \normalsize Email: {\tt schaerf@dis.uniroma1.it}

539: }

540: 

541: \date{}

542: 

543: % \modifymargins{50pt}{50pt}

544: 

545: % \def\comment#1{\vskip\baselineskip

546: % {\bf\tt #1}

547: % \vskip\baselineskip}

548: 

549: \begin{document}

550: 

551: \maketitle

552: 

553: %%%%%%%%%%%%% abst %%%%%%%%%%%%%%

554: \begin{abstract}

555: 

556: Abduction is one of the most important forms of reasoning; it has

557: been successfully applied to several practical problems such as

558: diagnosis. In this paper we investigate whether the computational

559: complexity of abduction can be reduced by an appropriate use of

560: preprocessing. This is motivated by the fact that

561: part of the data of the problem (namely, the set of all possible

562: assumptions and the theory relating assumptions and manifestations)

563: are often known before the rest of the problem. In this paper,

564: we show some complexity results about abduction when compilation

565: is allowed.

566: 

567: \end{abstract}

568: 

569: 

570: \newpage

571: 

572: \tableofcontents

573: 

574: \let\sectionnewpage=\newleaf

575: \let\subsectionnewpage=\relax

576: 

577: %%%%%%%%%%%%% intr %%%%%%%%%%%%%%

578: \section{Introduction}

579: 

580: Deduction, induction, and abduction~\shortcite{peir-55} are the

581: three basic reasoning mechanisms. Deduction allows drawing

582: conclusions from known facts using some piece of knowledge, so

583: that ``battery is down'' allows concluding ``car will not start''

584: thanks to the knowledge of the rule ``if the battery is down,

585: the car will not start''. Induction derives rules from the

586: facts: from the fact that the battery is down and that the

587: car is not starting up, we may conclude the rule relating these

588: two facts. Abduction is the inverse of deduction

589: (to some extent \cite{cial-96}): from the

590: fact that the car is not starting up, we conclude that the

591: battery is down. Clearly, this is not the only possible

592: explanation of a car not starting up. Therefore, we may get

593: more than one explanation. This is an important difference

594: between abduction and deduction, making the former, in

595: general, more complex.

596: 

597: While deduction formalizes the process of drawing conclusions,

598: abduction formalizes the diagnostic process, which attempts to

599: invert the cause-effect relation by inferring the causes from

600: its observable effects. The example of the car shows such

601: an application: complete knowledge about car would allow

602: finding (\ie, abducing) the possible reasons of why the car

603: is not starting up. The following example shows how abduction

604: can be applied to formalize a diagnostic scenario.

605: 

606: \begin{example}

607: 

608: While writing a paper with some authors located in another

609: country, you get a set of macros that are used in a nice

610: figure they drew. However, when compiling the .tex file, an

611: incomprehensible error message results. Four explanations

612: are possible:

613: 

614: \begin{description}

615: 

616: \item[$a$]: the macro has been used with the wrong arguments;

617: 

618: \item[$p$]: the package $X$ is required;

619: 

620: \item[$t$]: the macro is incompatible with package $X$;

621: 

622: \item[$v$]: the wrong version of TeX has been used.

623: 

624: \end{description}

625: 

626: This scenario can be formalized in logical terms by 

627: introducing a variable $f$ to denote the presence of

628: compile errors: since each of the facts above causes

629: $f$, we know $a \rightarrow f$, $p \rightarrow f$, etc.

630: Moreover, we know that a package cannot at the same

631: time be required and incompatible with the macros.

632: The following theory $T$ formalize our knowledge.

633: 

634: \[

635: T = \{ a \imply f, p \imply f, t \imply f,

636: v \imply f, \neg (p \wedge t) \}

637: \]

638: 

639: This theory relates the observed effect (the compile

640: error) with its possible causes (we used the wrong

641: version of TeX, etc.) Therefore, it can be used to

642: find the possible causes: namely, an explanation is

643: a set of facts that logically imply the observed

644: effect. Formally, an explanation is a set of variable

645: that allow deriving the observed effects from the

646: theory $T$. However, to make sense an explanation

647: has to be consistent with our knowledge, that is,

648: with the theory $T$.

649: 

650: \end{example}

651: 

652: This example shows that a given problem of abduction may

653: have one, none, or even many possible solutions (explanations).

654: Moreover, a consistent and an implication checks are required

655: just to verify an explanation. These facts intuitively explain

656: why abduction is to be expected to be harder than deduction.

657: This observation has indeed been confirmed by theoretical

658: results. Selman and Levesque~\cite{selm-leve-90}

659: and Bylander {\em et al.}~\shortcite{byla-etal-89}

660: proved the first results about fragments of abductive reasoning,

661: Eiter and Gottlob~\shortcite{eite-gott-95-a} presented

662: an extensive analysis, and Eiter and Makino have shown

663: the complexity of computing all abductive explanations

664: \cite{eite-maki-02}. All these results proved that abduction

665: is, in general, harder than deduction. The analysis has also shown

666: that several problems are of interest in abduction. Not only the

667: problem of finding an explanation is relevant, but also the

668: problems of checking an explanation, or whether a fact is

669: in all, or some, of the explanations are.

670: 

671: A common fact about deduction and abduction is that the

672: knowledge relating facts may be known in advance, while

673: the particular observation may change from time to time.

674: In the example of the car, the fact that the dead battery

675: makes the car not to start is always known, while the

676: fact that the battery is dead may or may not be true. The

677: possible causes of TeX errors are known before a specific

678: error message comes out, etc.

679: 

680: We can therefore assign two different statuses to the knowledge

681: base and to the single facts: while the knowledge base is

682: {\em fixed}, the single facts are {\em varying}. In the

683: example above, $T$ will always reflect the state of the

684: word, while $f$ is only true when the TeX complains

685: about something.

686: 

687: This difference has computational consequences. While

688: the example we have shown here does not present any problem

689: of efficiency, larger and more complex abduction

690: problems result from the formalization of real-world domains.

691: The difference of status of $T$ and the observations

692: can then be exploited. Indeed, since $T$ is always the

693: same, we can perform a preprocessing step on it alone,

694: even before the status of the observations are known.

695: Clearly, we cannot explain an observation we do not

696: know. However, this preprocessing step can be used to

697: perform some computation that would otherwise be done

698: on $T$ alone. As a result, finding a solution might

699: take less time when the observation finally get known.

700: 

701: The idea of using a preprocessing step for speeding-up

702: the solving of abduction problems is not new. For instance,

703: Console, Portinale, and Dupr\`e~\shortcite{cons-port-dupr-96}

704: have shown how compiled knowledge can be used in the process

705: of abductive diagnosis.

706: 

707: Preprocessing part of the input data has also been used in

708: many other areas of computer science, as there are many

709: problems with a similar fixed-varying part pattern. However,

710: the first formalization of intractability with preprocessing

711: is relatively recent \cite{cado-etal-02}. In this paper,

712: we characterize the complexity of the problems about

713: abductions from this point of view.

714: 

715: 

716: 

717: %%%%%%%%%%%%% prel %%%%%%%%%%%%%%

718: \section{Preliminaries}

719: 

720: The problem of abduction is formalized by a knowledge

721: base, a set of observations, and a set of possible

722: facts that can explain the observations. In this paper,

723: we are only concerned about propositional logic.

724: Therefore, the knowledge is formalized by a propositional

725: theory $T$. We usually denote by $M$ the set of

726: observations.

727: 

728: The theory is $T$ must necessarily contain all variables

729: of $M$, otherwise there would be no way of explaining

730: the observations. In general, the theory $T$ contains other

731: variables as well, describing facts we do not know whether

732: they are true or not. Some of these facts can be taken

733: as part of a possible explanation, while others are can

734: not. Intuitively, when we are trying to establish the

735: causes of an observation, we want the {\em first cause},

736: and not something that is only a consequence of it.

737: In the example of the car, the fact that there is no

738: voltage in the starting engine explains the fact that

739: the car is not starting up, but it is not an acceptable

740: explanation, as it does not tell where the real problem

741: is (the battery). Therefore, the abduction problem is

742: not defined only in terms of the theory and the

743: observation, but also of the set of possible facts

744: (variable) we would accept as first causes of the

745: observation.

746: 

747: Formally, an instance of abduction is a triple

748: $\l H, M, T \r$. The observations are formalized as $M$,

749: which is a set of variables. $T$ is a propositional

750: theory formalizing our knowledge of the domain. Finally,

751: $H$ is a set of variables; these variables are the ones

752: formalizing facts that we regards as possible first

753: causes.

754: 

755: Abduction is the process of explaining the observation.

756: Its outcome will therefore be a set of facts from which

757: all observations can be inferred. Since we can only 

758: use variables of $H$ to form explanations, these will

759: be subsets $H' \subseteq H$. Moreover, an explanation

760: can only be accepted if it is consistent with our

761: knowledge. This leads to the following definition of

762: the possible solutions (explanations) of a given

763: abduction problem  $\l H, M, T \r$.

764: 

765: \[

766: SOL( H, M, T ) =

767: \{ H' \subseteq H  ~|~	H' \cup T \mbox{ is consistent and }

768: 			H' \cup T \models M \}

769: \]

770: 

771: We apply this definition to the running example of the

772: TeX file.

773: 

774: \begin{example}

775: 

776: The propositional theory of the example shown in the

777: introduction is $T = \{ a \imply f, p \imply f, t \imply f,

778: v \imply f, \neg (p \wedge t) \}$. The observation is

779: the variable formalizing the presence of compiler errors,

780: that is, $M=\{f\}$. Of the variables of $T$, all but

781: $T$ can be taken as possible first causes of the problem,

782: that is, $H=\{a, p, t, v\}$.

783: 

784: Abduction amounts to finding a set of literals that

785: explain the observation $f$. Formally, this is captured

786: by the constraint $H' \cup T \models M$. Note that

787: $H' = \{f\}$ satisfies this formula; this is not

788: an acceptable explanation: ``the reason of why the file

789: does not compile is that it does not compile'' is a

790: tautology, not an explanation. This problem is avoided

791: by enforcing $H' \subseteq H$.

792: 

793: All non-empty subsets of $H$ implies, together with $T$,

794: the observation $M$. However, the subsets containing

795: both $p$ and $t$ are inconsistent with $T$. Therefore,

796: the set of solution of the problem is given by:

797: 

798: \[

799: SOL( H, M, T ) =

800: \{ H' \subseteq H ~|~ H \not= \emptyset ,~ \{t,p\} \not\subseteq H' \}

801: \]

802: 

803: This is simply the formal result of our current definition.

804: However, some explanations in this set are not really reasonable:

805: for example, the explanation is $\{a, t, v\}$ seems overly pessimistic:

806: the macro has been called in the wrong way {\em and} a package

807: is required {\em and} we used the wrong compiler version.

808: 

809: \end{example}

810: 

811: The set $SOL( H, M, T )$ contains all explanations we

812: consider possible. However, some explanations may be

813: more likely than others. For example, explanations

814: requiring a large number of assumptions are often

815: less likely than explanations with less assumptions.

816: 

817: Likeliness of explanations is formalized by an

818: an ordering $\preceq$ over the subsets of $H$.

819: Given a specific $\preceq$, the set of minimal

820: solutions is defined as follows.\eatpar

821: 

822: \[

823: SOL_\preceq( H, M, T ) = \min( SOL(H, M, T), \preceq )

824: \]

825: 

826: The ordering $\preceq$ is used to formalize the

827: relative plausibility explanations: $H' \prec H''$

828: means that $H'$ is considered more likely to

829: be the ``real'' cause of the manifestations

830: than $H''$. The ordering $\preceq$ represents the

831: concept of ``at least as likely as'', thus

832: $H' \cong H''$ holds if $H'$ and $H''$ are equally

833: likely. The definition of $SOL_\preceq$ formalizes

834: the principle of choosing only the explanations we

835: consider more likely.

836: 

837: An implicit assumption of this definitions is that

838: the ordering $\preceq$ does not depend on the set of 

839: manifestations. We also assume that $\preceq$ is a

840: ``well-founded'' ordering, that is, any non-empty

841: set of explanations has at least one $\preceq$-minimal

842: element. Therefore, if the set $SOL( H, M, T )$ is

843: not empty, then $\min(SOL( H, M, T ),\preceq)$ is not

844: empty as well.

845: 

846: In this paper we take into account several plausibility

847: ordering. The absence of a preference among the explanations

848: can be formalized as the ordering $\preceq$ that is equal

849: to the universal relation, that is, $H' \preceq H''$ for

850: any pair of sets of variables $H'$ and $H''$.

851: 

852: Besides this no-information ordering, the two simplest

853: and most natural orderings are $\subseteq$-preference,

854: where an explanation $H_1$ is more likely of $H_2$ if

855: $H_1 \subseteq H_2$, and $\leq$-preference, where $H_1$

856: is preferred to $H_2$ if it contains less hypothesis,

857: that is, $|H_1| \leq |H_2|$.

858: 

859: Both these orderings are based on the principle of making

860: as few hypotheses as possible, and by assuming that all

861: hypotheses are equally likely. Two other orderings follows

862: from assuming that the hypotheses are not equally likely:

863: the $\subseteq$-prioritization and the $\leq$-prioritization.

864: 

865: In particular, we assume that the hypotheses are partitioned

866: into equivalence classes of equal likeliness.

867: Let $\l H_1,\ldots,H_m \r$ be such a partition. By definition,

868: it holds $H_1 \cup \cdots \cup H_m = H$ and

869: $H_i \cap H_j = \emptyset$ for each $i

870: \not= j$. The instances of the problem of abduction can thus be

871: written as $\l \l H_1,\ldots,H_m \r, M, T \r$.  The set of all

872: assumptions $H$ is implicitly defined as the union of the classes

873: $H_i$. We assume

874: that the hypotheses in $H_1$ are the most likely, while those

875: in $H_m$ are the least likely.

876: 

877: The $\subseteq$-prioritization and $\leq$-prioritization compare

878: explanations on the basis of their relative plausibility.

879: Namely, the explanations that use hypothesis in lower classes

880: are more likely than explanations using hypothesis in higher classes.

881: This idea, when combined with subset containment, defines the

882: $\subseteq$-prioritization. When it is combined with the

883: cardinality-based ordering, it defines the $\leq$-prioritization.

884: Formal definition is below.

885: 

886: Penalization is the last form of preference we consider. The

887: idea is to assign weights to assumptions to formalize their

888: likeliness. Explanations with the least total weight are

889: preferred. Weights encodes the likeliness of assumptions:

890: the most high the weight of an assumption, the

891: unlikely it is to be true. To use penalization, the instance

892: of the problem must include, besides $H$, $M$, and $T$,

893: an $n$-tuple of weights $W=\l w_1,\ldots,w_n \r$, where each

894: $w_i$ is an integer number (the weight) associated to a

895: variable $h_i \in H$.  The instance can thus be written

896: $\l W, H, M, T \r$.

897: 

898: The considered orderings are formally defined as follows:

899: 

900: \begin{description}

901: 

902: \item[$\subseteq$-preference] $H' \preceq H''$ if and only if

903: $H' \subseteq H''$;

904: 

905: \item[$\leq$-preference] $H' \preceq H''$ if and only if $|H'| \leq |H''|$;

906: 

907: \item[$\subseteq$-prioritization] $H' \preceq H''$ if and only if $H'=H''$

908: or there exists $i$ such that $H' \cap H_m = H'' \cap H_m$, $\ldots$, 

909: $H' \cap H_i = H'' \cap H_i$, $H' \cap H_{i-1} \subset H'' \cap H_{i-1}$;

910: 

911: \item[$\leq$-prioritization] $H' \preceq H''$ if and only if either $|H' \cap

912: H_i| =|H'' \cap H_i|$ for each $i$, or there exists $i$ such that $|H' \cap

913: H_m| = |H'' \cap H_m|$, $\ldots$, $|H' \cap H_i| = |H'' \cap H_i|$, $|H' \cap

914: H_{i-1}| \leq |H'' \cap H_{i-1}|$;

915: 

916: \item[penalization] $H' \preceq H''$ if and only if

917: $\sum_{h_i \in H'} w_i \leq \sum_{h_j \in H''} w_j$.

918: 

919: \end{description}

920: 

921: Let us consider the use of these orderings on

922: the running example.

923: 

924: \begin{example}

925: 

926: The use of $\subseteq$-preference or $\leq$-preference

927: reduces the set of possible explanations of the example

928: of the TeX file. Namely, $\leq$-preference let 

929: minimal-size explanations only to be solutions of the

930: problem. The only such explanations are

931: $\{a\}$, $\{p\}$, $\{t\}$, and $\{v\}$. The explanation

932: $\{a, t, v\}$, being not minimal, is not a solution

933: of the problem any more. The use of preference therefore

934: avoids having as solutions some sets that contains too

935: many hypotheses. Since $\subseteq$-preference only

936: selects explanations that are not contained in other

937: ones, the only solutions it produces are 

938: $\{a\}$, $\{p\}$, $\{t\}$, and $\{v\}$. In this case,

939: the two kinds of the preference generate the same

940: solutions, but this is not always the case.

941: 

942: Prioritization allows for a further refinement of the

943: set of solutions by exploiting the plausibility ordering

944: over the hypotheses. For example, we may assume that

945: the fact that package $X$ is required and that we used

946: the wrong version of the compiler are the two most

947: likely hypotheses. Formally, they will be part of the

948: first set of assumptions $H_1$, while the other assumptions

949: will therefore go in $H_2$. Formally, the problem instance

950: is now $\l \l H_1,H_2 \r, M, T \r$. Both

951: $\subseteq$-prioritization and $\leq$-prioritization

952: produce $\{p\}$ and $\{v\}$ as the only minimal

953: explanations. This is because all other explanations

954: either have a bigger intersection with $H_2$, or an

955: equal intersection with $H_2$ but a bigger intersection

956: with $H_1$.

957: 

958: Finally, penalization requires a weight (an integer

959: number) for each hypothesis. Let us for example use

960: the set of weights $\l 4, 2, 4, 1\r$ associated with

961: the set of hypotheses $\l a, p, t, v\}$. Since larger

962: weights correspond to less likely hypotheses, we are

963: assuming that our first and third hypotheses ($a$ and

964: $t$) are the least likely, while $p$ is more likely

965: and $v$ is the most likely. From definition, the

966: explanation $\{v\}$ is the one having the least weight,

967: and is therefore the only solution of the problem.

968: 

969: \end{example}

970: 

971: \iffalse

972: 

973: In the sequel, we assume that the set of all possible manifestations is

974: identical to the set of all variables.  In some cases, it is useful to assume

975: that this set is disjoint to the set of hypothesis. In such cases, a very

976: simple reduction can be used: we create a copy of each variable $a$, and then

977: we add $a \equiv a'$ to the theory. This way, we can use the original variables

978: in $H$ for the hypothesis and the variables $a'$ for the possible

979: manifestations.  Moreover, without loss of generality,

980: 

981: In this paper, we assume that $T$ is a 3CNF formula

982: (this assumption does not cause a loss of generality

983: unless we want to assume that $H \cup M = \var(T)$.)

984: We also assume that the variables of $T$ are the

985: assumptions $h_1,\ldots,h_m$, plus another disjoint set of variables we denote

986: as $x_1,\ldots,x_n$. 

987: 

988: \fi

989: 

990: The basic problem of abduction is that of finding

991: one or more explanations. However, we have already

992: remarked that none may exist. Therefore, the first

993: problem we consider is the existence one: given

994: an instance of abduction, does an explanation

995: exist? Another related problem is that of verifying,

996: once a set of hypotheses has been found, whether

997: it is really an explanation or not.

998: 

999: Other problems are related to the structure of

1000: the explanations. Namely, hypotheses that are in

1001: {\em all} explanations may considered as ``sure''

1002: conclusions of the abductive process. On the other

1003: hand, hypotheses that are part of some explanations

1004: can be regarded as ``possible'' conclusions.

1005: 

1006: The formal definition of these questions as

1007: decision problems is as follows.

1008: 

1009: \begin{description}

1010:   

1011: \item[Existence:] is there an explanation of the observed

1012:   manifestations? That is, $SOL(H,M,T) \not= \emptyset$?

1013: 

1014: \item[Verification:] given a set $H' \subseteq H$, is $H'$ a minimal

1015:   solution? That is, $H' \in SOL_{\preceq} (H, M, T)$?

1016: 

1017: \item[Relevance:] given a variable $h \in H$, is there a minimal solution

1018: containing~$h$? That is, $\exists H' \subseteq H$ such that $H' \in

1019: SOL_{\preceq} (H, M, T)$ and $h \in H'$?

1020: 

1021: \item[Necessity:] is $h \in H$ in all, and at least one, minimal

1022:   solution?  That is, $SOL(H, M, T) \neq \emptyset$ and $\forall H'

1023:   \subseteq H$ we have that $H' \in SOL_{\preceq} (H, M, T)$ implies

1024:   $h \in H'$?

1025:   

1026: \item[Dispensability:] is $h \in H$ such that either there is no

1027:   solution or there exists one who does not contain $h$? That is,

1028:   $SOL(H, M, T) = \emptyset$ or $\exists H' \subseteq H$ such that $H'

1029:   \in SOL_{\preceq} (H, M, T)$ and $h \not \in H'$?

1030: 

1031: \end{description}

1032: 

1033: Dispensability is the converse of the problem of necessity,

1034: since an hypothesis $h$ is dispensable if and only if it

1035: is not necessary. The problem of dispensability is not of

1036: much interest by itself, but is sometimes useful for

1037: simplifying the proofs.

1038: 

1039: Clearly, the ordering does not matter for the problem of existence,

1040: since we consider only well-founded orderings: therefore,

1041: an explanation exists if and only if a minimal explanation

1042: exists. For the other problems, the ordering must be taken

1043: into account. Different orderings may lead to different

1044: computational properties.

1045: 

1046: In this paper, we assume that $T$ is a 3CNF formula:

1047: this assumption does not cause a loss of generality

1048: unless we want to assume that $H \cup M = \var(T)$.

1049: 

1050: 

1051: 

1052: %%%%%%%%%%%%% comp %%%%%%%%%%%%%%

1053: \section{Complexity and Compilability}

1054: \label{compilability}

1055: 

1056: The basic complexity classes of the polynomial hierarchy

1057: \cite{stoc-76,gare-john-79}, such as \p, \np, \conp, etc.,

1058: are assumed known to the reader. We denote by \C, $\C'$,

1059: etc.\  arbitrary classes of the polynomial hierarchy.

1060: The {\em length} of a string $x \in \Sigma^*$ is denoted

1061: by $||x||$.

1062: 

1063: We summarize some definitions and results proposed to

1064: formalize the on-line complexity of problems \cite{cado-etal-02}.

1065: In computational complexity, problems whose solution

1066: can only be yes or no are the most commonly analyzed. Such

1067: problems are called {\em decision problems}. Any such

1068: problem can be formalized as set of strings, those

1069: whose solution is yes. For example, the problem of

1070: propositional satisfiability (deciding whether a formula

1071: is satisfiable or not) is characterized by the set of

1072: the strings that represent exactly all satisfiable

1073: formulae.

1074: 

1075: The strings that compose the set associated to a problem

1076: represent the possible problem instances that produce a

1077: positive solution. Problems like abduction, however,

1078: have instances that can be naturally broken into two

1079: parts: one part is known in advance ($T$ and $H$)

1080: and one part is only known at run-time ($M$). Therefore,

1081: the instances of such problems are better encoded as

1082: {\em pairs of strings}. Therefore, a problem like abduction

1083: is formalized by a set of pairs of strings, rather than

1084: a set of strings. We define a {\em language of pairs} $S$

1085: as a subset of $\Sigma^* \times \Sigma^*$. 

1086: 

1087: The difference between the first and second element of

1088: a pair is that some preprocessing time can be spent on

1089: the first string alone. This is done to the aim of solving

1090: the problem faster when the second string comes to be

1091: known. While our final aim is to reduce the running time

1092: of this second phase, some constraints have to be put on

1093: the preprocessing phase. Namely, we impose its result

1094: to be of polynomial size. {\em Poly-size} function are

1095: introduced to this purpose: a function $f$ from strings

1096: to strings is called {\em poly-size} if there exists a

1097: polynomial $p$ such that, for all strings $x$, it holds

1098: $||f(x)|| \leq p(||x||)$. An exception to this definition

1099: is when $x$ represents a natural number: in this case,

1100: we impose $||f(x)|| \leq p(x)$. Any polynomial function is

1101: polysize, but not viceversa. Indeed, a function $g$ is

1102: {\em poly-time} if there exists a polynomial $q$ such that,

1103: for all $x$, $g(x)$ can be computed in time less than or

1104: equal to $q(||x||)$. Clearly, the running time also bounds

1105: the size of the output string; on the other hand, even

1106: a function requiring exponential running time can produce

1107: a very short output. The definitions of polysize and polytime

1108: function extend to binary functions as usual.

1109: 

1110: Using the above definitions, we introduce a new hierarchy

1111: of classes of languages of pairs, the {\em non-uniform

1112: compilability classes} \cite{cado-etal-02}, denoted by

1113: \nucC, where C is a generic uniform complexity class, such

1114: as P, \np, \conp, or \S 2.

1115: 

1116: \begin{definition}[\nucC\  classes, \cite{cado-etal-02}]

1117: 

1118: A language of pairs $S \subseteq \Sigma^* \times \Sigma^*$

1119: belongs to \nucC\  iff there exists a binary poly-size

1120: function $f$ and a language of pairs $S' \in \C$ such that,

1121: for all $\pair x y \in S$, it holds:\eatpar

1122: 

1123: \[

1124: \pair x y \in S

1125: \mbox{~~ iff ~~}

1126: \pair {f(x,||y||)} y \in S'

1127: \]

1128: 

1129: \end{definition}

1130: 

1131: Clearly, any problem whose time complexity is in \C\

1132: is also in \nucC: just take $f(x,||y||)=x$ and $S'=S$.

1133: Some problems in \C\ however belongs to $\nucC'$ with

1134: $\C' \subset C$; for example, some problem in \np\

1135: are in \nucP. These are in fact the problems we are

1136: most interested, as the preprocessing phase, running

1137: on $x$ only, will produce $f(x)$, which allows solving

1138: the problem in polynomial time. This is important if

1139: these problems cannot be solved in polynomial time

1140: without the preprocessing phase (\eg, they are

1141: \np-complete).

1142: 

1143: The class \nucC\ generalizes the non-uniform class

1144: \C/\poly\ --- i.e., \C/\poly\ $\subset$ \nucC\ ---

1145: by allowing for a fixed part $x$. We extend the

1146: definition of polynomial reduction to a concept

1147: that can be used with these classes.

1148: 

1149: \begin{definition}[Non-uniform comp-reduction]

1150: \label{non-uniform-reduction}

1151: 

1152: A non-uniform comp-reduction is a triple of functions

1153: $\l f_1, f_2, g \r$, where $g$ is polytime and $f_1$

1154: and $f_2$ are polysize. Given two problems $A$ and $B$,

1155: $A$ is {\em non-uniformly comp-reducible\/} to $B$

1156: (denoted by $A \nucomp B$) iff there exists a non-uniform

1157: comp-reduction $\l f_1, f_2, g \r$ such that, for every

1158: pair ${\pair x y }$ it holds that ${\pair x y } \in A$ if

1159: and only if

1160: ${\pair {f_1(x,||y||)} {g(f_2(x,||y||),y)} } \in B$.

1161: 

1162: \end{definition}

1163: 

1164: These reductions allows for a concept of {\em hardness}

1165: and {\em completeness} for the classes \nucC.

1166: 

1167: \begin{definition}[\nucC-completeness]

1168: 

1169: Let $S$ be a language of pairs and {\rm C} a complexity

1170: class. $S$ is \nucC{\em -hard} iff for all problems

1171: $A \in \nucC$ we have that $A \nucomp S$. Moreover,

1172: $S$ is \nucC-complete if $S$ is in \nucC\  and

1173: is \nucC-hard.

1174: 

1175: \end{definition}

1176: 

1177: The hierarchy formed by the compilability classes is

1178: proper if and only if the polynomial hierarchy is proper

1179: \cite{cado-etal-02,karp-lipt-80,yap-83} --- a fact widely

1180: conjectured to be true.

1181: 

1182: Informally, \nucnp-hard problems are ``not compilable to P''.

1183: Indeed, if such compilation were possible, then it would be

1184: possible to define $f$ as the function that takes the fixed

1185: part of the problem and gives the result of compilation

1186: (ignoring the size of the input), and $S'$ as the language

1187: representing the on-line processing. This would implies that a

1188: \nucnp-hard problem is in \nucp, and this implies the collapse

1189: of the polynomial hierarchy.  In general, a problem that is

1190: \nucC-complete for a class \C\  can be regarded as the

1191: ``toughest'' problem in \C, in the assumption that preprocessing

1192: the fixed part is possible.

1193: 

1194: While \nucC-completeness is adequate to show the compilability

1195: level of a given reasoning problem, proving it requires finding

1196: a nucomp reduction. We show a technique that let us reuse,

1197: with simple modifications, the polytime reductions that were

1198: used to prove the usual (uniform) hardness of the problem.

1199: Namely, we present sufficient conditions allowing for a

1200: polynomial reduction to imply the existence of a nucomp

1201: reduction \cite{libe-01-jacm}.

1202: 

1203: Let us assume that we know a polynomial reduction from

1204: the problem $A$ to the problem $B$, and we want to prove

1205: the nucomp-hardness of $B$. Some conditions on $A$ should

1206: hold, as well as a condition over the reduction.

1207: If all these conditions are verified, then

1208: there exists a nucomp reduction from $*A$ to $B$.

1209: 

1210: \begin{definition}[Classification Function]

1211: 

1212: A {\em classification function} for a problem $A$ is a

1213: polynomial function $Class$ from instances of $A$ to

1214: nonnegative integers, such that $Class(y) \leq ||y||$.

1215: 

1216: \end{definition}

1217: 

1218: \begin{definition}[Representative Function]

1219: 

1220: A {\rm representative function} for a problem $A$ is a

1221: polynomial function $Repr$ from nonnegative integers to

1222: instances of $A$, such that $Class( Repr( n) )=n$, and

1223: that $||Repr(n)||$ is bounded by some polynomial in $n$.

1224: 

1225: \end{definition}

1226: 

1227: \begin{definition}[Extension Function]

1228: 

1229: An {\em extension function} for a problem $A$ is a polynomial function from

1230: instances of $A$ and nonnegative integers to instances of $A$ such that, for

1231: any $y$ and $n \geq Class(y)$, the instance $y' = Exte(y,n)$ satisfies the

1232: following conditions:\eatpar

1233: 

1234: \begin{enumerate}

1235: \itemsep=0pt

1236: \item $y \in A$ if and only if $y' \in A$;

1237: \item $Class(y')=n$.

1238: \end{enumerate}

1239: 

1240: \end{definition}

1241: 

1242: Let us give some intuitions about these functions.

1243: Usually, an instance of a problem is composed of a

1244: set of objects combined in some way. For problems on

1245: boolean formulas, we have a set of variables combined

1246: to form a formula.  For graph problems, we have a set

1247: of nodes, and the graph is indeed a set of edges,

1248: which are pairs of nodes.

1249: The classification function gives the number of objects in an

1250: instance. The representative function thus gives an instance with the given

1251: number of objects. This instance should be in some way ``symmetric'', in the

1252: sense that its elements should be interchangeable (this is because the

1253: representative function must be determined only from the number of objects.)

1254: Possible results of the representative function can be

1255: the set of all clauses of three literals over a given

1256: alphabet, the complete graph over a set of nodes, the graph with no edges,

1257: etc.

1258: 

1259: Let for example $A$ be the problem of propositional satisfiability. We can take

1260: $Class(F)$ as the number of variables in the formula $F$, while $Repr(n)$ can

1261: be the set of all clauses of three literals over an alphabet of $n$ variables.

1262: Finally, a possible extension function is obtained by adding tautological

1263: clauses to an instance.

1264: 

1265: Note that these functions are related to the problem $A$ only, and do not

1266: involve the specific problem $B$ we want to prove hard, neither the specific

1267: reduction used. We now define a condition over the polytime

1268: reduction from $A$ to $B$. Since $B$ is a problem of pairs,

1269: we can define a reduction from $A$ to $B$ as a pair of

1270: polynomial functions $\l r,h \r$ such that $x \in A$

1271: if and only if $\l r(x),h(x) \r \in B$.

1272: 

1273: \begin{definition}[Representative Equivalence]

1274: 

1275: Given a problem $A$ (having the above three functions), a problem of pairs

1276: $B$, and a polynomial reduction $\langle r,h \rangle$ from $A$ to $B$, the

1277: condition of representative equivalence holds if, for any instance $y$ of $A$,

1278: it holds:\eatpar

1279: 

1280: \[

1281: \l r(y),h(y) \r \in B \mbox{ ~~ iff ~~ } \l r(Repr(Class(y)),h(y) \r \in B

1282: \]

1283: 

1284: \end{definition}

1285: 

1286: The condition of representative equivalence can be

1287: proved to imply that the problem $B$ is \nucC-hard,

1288: if $A$ is \C-hard \cite{libe-01-jacm}.

1289: 

1290: 

1291: 

1292: 

1293: %%% Local Variables: 

1294: %%% mode: latex

1295: %%% TeX-master: "main"

1296: %%% End: 

1297: 

1298: %%%%%%%%%%%%% noorder %%%%%%%%%%%%%%

1299: \section{Compilability of Abduction: No Ordering}

1300: 

1301: In this section we analyze the problems of existence

1302: of explanation, explanation verification, relevance,

1303: and necessity, for the basic case in which no ordering

1304: is defined. Formally, we want to determine whether

1305: the complexity of the problems related to

1306: $SOL(H, M, T)$ decrease thanks to the preprocessing

1307: step on $H$ and $T$.

1308: 

1309: We first give an high-level explanation of the method

1310: we use to prove the incompilability of the considered

1311: problems. We begin by applying the method to the problem

1312: of existence of explanations, and then we used it for

1313: verification, relevance and necessity.

1314: 

1315: %%%%%%%%%%%%% method %%%%%%%%%%%%%%

1316: \subsection{The Method}

1317: 

1318: The problem of deciding whether there exists an explanation for

1319: a set of manifestations is \S{2}-hard \cite{eite-gott-95-a}.

1320: Therefore, there exists a polynomial reduction from another

1321: \S{2}-hard problem to this one. In order to prove it is also

1322: \nucS{2}-hard we can show that the other problem has the

1323: three functions, and the reduction satisfies the condition

1324: of representative equivalence. Unfortunately, this is not

1325: the case. As a result, we have to look for another reduction.

1326: 

1327: Such a reduction should be as simple as possible. In

1328: general, the more similar two problems are, the easier

1329: it is to find a reduction. What is the \S{2}-hard problem

1330: that is the most similar to the problem of existence of

1331: explanation? Clearly, the problem itself is the most similar

1332: to itself.

1333: 

1334: The theorem of representative equivalence is indeed about

1335: a reduction between two problems $A$ and $B$, but it does

1336: not forbid using the same problem: it only tells that, if

1337: we have a reduction from {\em an arbitrary} \S{2}-hard

1338: problem $A$ to $B$, satisfying representative equivalence,

1339: then $B$ is \nucS{2}-hard. Nothing prevent us from choosing

1340: $A=B$. This technique can be formalized as follows:\eatpar

1341: 

1342: \begin{itemize}

1343: 

1344: \item show that there exists a classification, representative,

1345: and extension functions for the problem $B$;

1346: 

1347: \item show that there exists a reduction from $B$ to $B$

1348: satisfying representative equivalence.

1349: 

1350: \end{itemize}

1351: 

1352: The most obvious reduction from a problem to itself is the identity.

1353: In our case, however, identity does not satisfy the condition of

1354: representative equivalence. As a result, we have to look for

1355: another reduction.

1356: 

1357: Before showing the technical details of the reductions used,

1358: we point out an important feature of this technique. Since

1359: the condition of representative equivalence tells that $B$

1360: is \nucC-hard if $A$ is \C-hard, using $A=B$ we prove

1361: that $B$ is \nucC-hard whenever $B$ is \C-hard. This result

1362: holds even if a precise complexity characterization of $B$

1363: is not known. For example, if we only know that $B$ is in

1364: \S{2}, but do not have any hardness result, we can still

1365: conclude that $B$ is \nucnp-hard if it is \np-hard, it

1366: is \nucconp-hard if it is \conp-hard, it is \nucS{2}-hard

1367: if it is \S{2}-hard, etc.

1368: 

1369: In order to simplify the following proofs, we denote with

1370: $\Pi(X)$ the set of all distinct clauses of length 3 on a

1371: given alphabet $X = \{x_1, \ldots, x_n\}$. Since the theory

1372: $T$ is in 3CNF by assumption, we have that $T \subseteq \Pi(V)$,

1373: where $V$ is the set of variables appearing in $T$.

1374: 

1375: 

1376: 

1377: %%%%%%%%%%%%% existence %%%%%%%%%%%%%%

1378: \subsection{Existence of Solutions}

1379: 

1380: In order to define a reduction from the problem of

1381: existence of solutions to itself, we first consider

1382: the function $f$ from abduction instances to

1383: abduction instances defined as follows:

1384: 

1385: \begin{eqnarray*}

1386: f( \l H,M,T \r ) 

1387: &=&

1388: \l H',M',T' \r

1389: \\

1390: &&

1391: \mbox{where:}

1392: \\

1393: &&

1394: \begin{array}{rcl}

1395: H' &=&

1396: H \cup C \cup D \\

1397: M' &=&

1398: M \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \} \\

1399: T' &=&

1400: \{ \neg c_i \vee \neg d_i ~|~ \gamma_i \in \Pi(H \cup X)\}

1401: \cup \{ c_i \rightarrow \gamma_i ~|~ \gamma_i \in \Pi(H \cup X) \}

1402: \end{array}

1403: \end{eqnarray*}

1404: 

1405: In these formulae, $X$ denotes the alphabet of $T$, while

1406: $C$ and $D$ are sets of new variables in one-to-one correspondence

1407: with the clauses in $\Pi(H \cup X)$. Note that, by definition,

1408: $T$ is a subset of $\Pi(H \cup X)$. The following lemma

1409: relates the solutions of $\l H,M,T \r$ with the solutions

1410: of $\l H',M',T' \r$.

1411: 

1412: \begin{lemma}

1413: \label{basic}

1414: 

1415: Let $f$ be the function defined above. For any $H$, $M$, $T$,

1416: it holds:\eatpar

1417: 

1418: \[

1419: SOL(f(\l H,M,T \r)) =

1420: \{ S \cup \{ c_i ~|~ \gamma_i \in T \} \cup

1421: \{ d_i ~|~ \gamma_i \not\in T \}

1422: ~|~ S \in SOL(\l H,M,T \r) \}

1423: \]

1424: 

1425: \end{lemma}

1426: 

1427: \proof We divide the proof in three parts. In the first

1428: part, we prove that any solution of $f(\l H,M,T \r)$

1429: contains exactly the literals $c_i$ and $d_i$ that are in $M'$.

1430: In the second part, we prove that, if $S'$ is a solution

1431: of $f(\l H,M,T \r)$, then $S' \backslash (C \cup D)$ is

1432: a solution of $\l H,M,T \r$; the third part is the proof

1433: of the converse.

1434: 

1435: \begin{enumerate}

1436: 

1437: \item We prove that

1438: $S' \cap (C \cup D) =

1439: \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}$.

1440: Let $R= \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}$.

1441: Since $R \subseteq M'$, we have that $S' \cup T' \models R$.

1442: If $c_i \in R$, then $S' \cup T' \models c_i$.

1443: Since $T'$ does not contain any positive occurrence of $c_i$,

1444: the theory $S' \cup T'$ can imply $c_i$ only if $c_i \in S'$.

1445: The same holds for any $d_i \in R$. This proves that

1446: $S' \cap (C \cup D) \supseteq R$. Since $R$ contains

1447: either $c_i$ or $d_i$ for any $i$, the same holds for $S'$.

1448: No other variable in $C \cup D$ can be in $S'$, otherwise

1449: $S'$ would be inconsistent with $T'$, which contains

1450: the clauses $\neg c_i \vee \neg d_i$.

1451: 

1452: \item Let $S'$ be an element of $SOL(\l H',M',T' \r)$. We prove that $S = S'

1453: \backslash (C \cup D) \in SOL(\l H,M,T \r)$. The point proved above shows that,

1454: for each $i$, $S'$ contains either $c_i$ or $d_i$, depending on whether

1455: $\gamma_i \in T$. As a result:\eatpar

1456: 

1457: \begin{eqnarray*}

1458: S' \cup T'

1459: &\equiv&

1460: S \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}

1461: \cup \{ \neg c_i \vee \neg d_i \} \cup \{ c_i \rightarrow \gamma_i \}

1462: \\

1463: &\equiv&

1464: S \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}

1465: \cup T

1466: \end{eqnarray*}

1467: 

1468: As a result, $S \cup T$ is consistent because the above formula is. Moreover,

1469: since the above formula implies $M$, and each variable in $C \cup D$ appears

1470: only once, it also holds $S \cup T \models M$. As a result, $S$ is a solution

1471: of $\l H,M,T \r$.

1472: 

1473: \item Let $S \in SOL(\l H,M,T \r)$, and let

1474: $S' = S \cup \{ c_i ~|~ \gamma_i \in T \} \cup

1475: \{ d_i ~|~ \gamma_i \not\in T \}$.

1476: Since $S' \cup T'$ is equivalent to

1477: $S \cup T \cup \{ c_i ~|~ \gamma_i \in T \} \cup

1478: \{ d_i ~|~ \gamma_i \not\in T \}$, then $S'$ 

1479: is a solution of $\l H',M',T' \r$.

1480: 

1481: \end{enumerate}

1482: 

1483: The claim is thus proved.~\qed

1484: 

1485: This lemma shows that any abduction instance can be

1486: converted into another one in which the set $H$ and

1487: the theory $T$ only depends on the number of variables

1488: of the original instance. This reduction can be used

1489: to build a reduction satisfying the condition of

1490: representative equivalence.

1491: 

1492: \begin{lemma}

1493: \label{add-assumptions}

1494: 

1495: Let $c$ be a positive integer number, and let $g_c$

1496: be the following function:\eatpar

1497: 

1498: \[

1499: g_c(\l H,M,T \r) = \l H \cup \{ h_{|H|+1}, \ldots , h_c \}, M,

1500: T \cup \{ x_{r+1} \vee \neg x_{r+1}, \ldots , x_c \vee \neg x_c \} \r

1501: \]

1502: 

1503: \noindent where $r = |Var(T) \backslash H|$. It holds

1504: 

1505: \[

1506: SOL(g_c(\l H,M,T \r)) =

1507: \{ S \cup H' ~|~ S \in SOL(\l H,M,T \r) \mbox{ and }

1508: H' \subseteq \{ h_{|H|+1}, \ldots , h_c \} \}

1509: \]

1510: 

1511: \end{lemma}

1512: 

1513: \proof The instance $g_c(\l H,M,T \r)$ only differs

1514: from $\l H,M,T \r$ because of the new assumptions

1515: $h_{|H|+1}, \ldots , h_c$, which are not even mentioned

1516: in $T$, and new tautological clauses to $T$. Therefore,

1517: any explanation of $\l H,M,T \r$ is also an explanation

1518: of $g_c(\l H,M,T \r)$. The only difference between these

1519: two problems is that assumptions in $h_{|H|+1}, \ldots , h_c$

1520: can be freely added to any explanations.~\qed

1521: 

1522: We now define the classification, representative, and extension functions for

1523: the basic problems of abduction. First, the classification function is given by

1524: the maximum between the number of variables in $H$ and the number of variables

1525: in $T$ but not in $H$:\eatpar

1526: 

1527: \[

1528: Class(\l H,M,T \r) = \max( |H|, |Var(T) \backslash H|)

1529: \]

1530: 

1531: The representative instance of the class $c$ is given by an instance with $c$

1532: possible assumptions, $c$ other variables, and $T$ composed by all possible

1533: clauses of three literals over these variables:\eatpar

1534: 

1535: \[

1536: Repr(c) = \l \{h_1, \ldots, h_c\}, \emptyset,

1537: 	\Pi(\{h_1, \ldots, h_c\} \cup \{x_1, \ldots, x_c\}) \r

1538: \]

1539: 

1540: The extension function is also easy to give. For example, we may add to $T$ a

1541: set of tautologies with new variables.\eatpar

1542: 

1543: \[

1544: Ext(\l H,M,T \r,m) =

1545: \l H, M, T \cup \{x_{r+1} \vee \neg x_{r+1}, \ldots, x_m \vee \neg x_m\} \r

1546: \mbox{ where } r=|Var(T) \backslash H|

1547: \]

1548: 

1549: These three functions are valid classification, representative,

1550: and extension functions for the problem of existence of explanation;

1551: they are also valid for the problems of relevance and necessity.

1552: 

1553: \

1554: 

1555: We are now able to show a reduction satisfying the condition

1556: of representative equivalence. Let $i$ be the reduction

1557: defined as follows.

1558: 

1559: \[

1560: i(\l H,M,T \r) = f( g_{Class(\l H,M,T \r)} ( \l H,M,T \r) )

1561: \]

1562: 

1563: The following theorem is a consequence of the fact that

1564: $i$ satisfies the condition of representative equivalence.

1565: 

1566: \begin{theorem}

1567: 

1568: The problem of establishing the existence of solution of an abductive

1569: problem is \nucS{2}-hard.

1570: 

1571: \end{theorem}

1572: 

1573: \proof

1574: By the above two lemmas, $i(\l H,M,T \r)$ has solutions

1575: if and only if $\l H,M,T \r$ has solution. Therefore,

1576: $i$ is a valid reduction from the problem of solution

1577: existence to itself. The fixed part of $i(\l H,M,T \r)$

1578: only depends on the class of the instance $\l H,M,T \r$. As a

1579: result, this reduction satisfies the condition of

1580: representative equivalence. Since the problem of

1581: existence of solutions is \S{2}-hard \cite{eite-gott-95-a},

1582: it is also \nucS{2}-hard.~\qed

1583: 

1584: 

1585: 

1586: 

1587: %%%%%%%%%%%%% veri-noor %%%%%%%%%%%%%%

1588: \subsection{Verification}

1589: 

1590: We consider the problem of verifying whether a set of

1591: assumptions is a possible explanation, still in the

1592: case of no ordering. An instance of the problem is

1593: composed of a triple $\l H,M,T \r$ and a specific subset

1594: $H_a \subseteq H$ we want to check being an explanation.

1595: Formally, this problem amounts to checking whether

1596: $H_a \cup T$ is consistent and $H_a \cup T \models M$.

1597: The varying part is composed of $H_a$ and $M$. Formally,

1598: an instance of the verification problem is a 4-tuple

1599: $\l H,H_a,M,T \r$, where $H_a \subseteq H$.

1600: 

1601: The first step of the proof is that of finding the

1602: three functions (classification, representative,

1603: and extension). The functions of the last proof

1604: only require minor changes to be used now.\eatpar

1605: 

1606: \begin{eqnarray*}

1607: Class(\l H,H_a,M,T \r) &=& \max( |H|, \var(T) \backslash H ) \\

1608: Repr(c) &=& \l \{ h_1, \ldots, h_c \}, \emptyset, \emptyset,

1609: 	    \Pi( \{ h_1, \ldots, h_c \} \cup \{ x_1, \ldots, x_c \} \r \\

1610: Exte(\l H,H_a,M,T \r) &=& 

1611: 	\l H,H_a,M,T \cup \{ x_{r+1} \vee \neg x_{r+1}, \ldots ,

1612:                             x_c \vee \neg x_c \r \} \r \\

1613: && \mbox{where } r=| \var(T) \backslash H |

1614: \end{eqnarray*}

1615: 

1616: We define two functions $f'$ and $g_c'$ to be similar to

1617: the functions $f$ and $g_c$ of the last section, except

1618: for the addition of a candidate explanation $H_a$.\eatpar

1619: 

1620: \begin{eqnarray*}

1621: f'(\l H,H_a,M,T \r)

1622: &=&

1623: \l H',H_a \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \},

1624: M',T' \r \\

1625: &&

1626: \mbox{ where } \l H',M',T' \r = f(\l H,M,T \r)

1627: \\

1628: g_c'(\l H,H_a,M,T \r)

1629: &=&

1630: \l H',H_a,M',T' \r

1631: \\

1632: &&

1633: \mbox{ where } \l H',M',T' \r = g_c(\l H,M,T \r)

1634: \end{eqnarray*}

1635: 

1636: These functions can be composed to generate a function

1637: that satisfies representative equivalence. This way,

1638: we prove the nucomp-hardness of the problem of

1639: verification.

1640: 

1641: \begin{theorem}

1642: 

1643: The problem of verification with no ordering is \nucDp-complete.

1644: 

1645: \end{theorem}

1646: 

1647: \proof

1648: By Lemma~\ref{basic} and Lemma~\ref{add-assumptions}, $H_a \subseteq H$ is a

1649: solution of $g_c(\l H,M,T \r)$ if and only if it is a solution of $\l H,M,T

1650: \r$, and that $H_a \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i

1651: \not\in T \}$ is a solution of $f(\l H,M,T \r)$ if and only if $H_a$ is a

1652: solution of $\l H,M,T \r$.

1653: 

1654: As a result, both $f'$ and $g_c'$ are reductions from the problem of

1655: verification to itself. Moreover, their composition $i'$ satisfies

1656: representative equivalence, since the fixed part of $i'(\l H,H_a,M,T \r)$

1657: only depends on the class of the instance $\l H,H_a,M,T \r$. We can then

1658: conclude that the problem of verification is hard for the

1659: compilability class that corresponds to the complexity class

1660: it is hard for.~\qed

1661: 

1662: 

1663: 

1664: 

1665: %%%%%%%%%%%%% rele-noor %%%%%%%%%%%%%%

1666: \subsection{Relevance, Dispensability, and Necessity}

1667: 

1668: We make the following simplifying assumption: given an

1669: instance of abduction $\l H,M,T \r$, where $H = \{h_1,\ldots,h_m\}$,

1670: the problem is to decide whether the first assumption $h_1$ is

1671: relevant/dispensable/necessary. Clearly, the complexity of these

1672: problems is the same, as we can always rename the variables

1673: appropriately.

1674: 

1675: \begin{theorem}

1676: 

1677: The problems of relevance and dispensability with no ordering

1678: is \nucS{2}-hard, while necessity is \nucP{2}-hard.

1679: 

1680: \end{theorem}

1681: 

1682: \proof

1683: By Lemma~\ref{basic} and Lemma~\ref{add-assumptions}, 

1684: $i(\l H,M,T \r)$ is a reduction from the problem

1685: of relevance to the problem of relevance. Indeed, for

1686: any $H_a \subseteq H$, the set

1687: $H_a \cup \{ c_i ~|~ \gamma_i \in T \} \cup

1688: \{ d_i ~|~ \gamma_i \not\in T \}$ is a solution

1689: of $f(g_c(\l H,M,T \r))$ if and only if $H_a$ is a

1690: solution of $\l H,M,T \r$. As a result, $h_1$ is

1691: relevant/dispensable/necessary for $\l H,M,T \r$ if and

1692: only if it is so for $f(g_c(\l H,M,T \r))$.

1693: 

1694: The function $i$ satisfies representative equivalence, since the fixed part of

1695: $i(\l H,M,T \r)$ only depends on the class of $\l H,M,T \r$. What is left to

1696: prove is the existence of the three functions. We can use the same three ones

1697: used for the problem of existence of solutions.~\qed

1698: 

1699: 

1700: 

1701: 

1702: 

1703: 

1704: 

1705: %%%%%%%%%%%%% noclass %%%%%%%%%%%%%%

1706: \section{Compilability of Abduction: Preferences}

1707: 

1708: In this section, we consider the problems of verification,

1709: relevance, and necessity when the ordering used is either

1710: $\leq$ or $\subseteq$. These orderings have in common the

1711: fact that the instance of an abduction problem is simply

1712: a triple $\l H,M,T \r$, whereas the orderings of the next

1713: section employee classes of priority or weights that are

1714: part of the instances. The problem of existence is the same  

1715: as with no ordering, as these orderings are well founded.

1716: 

1717: 

1718: %%%%%%%%%%%%% meth-nocl %%%%%%%%%%%%%%

1719: \subsection{Some General Results}

1720: 

1721: We give some general results about the problem of abduction in the case in

1722: which an ordering on explanation is given. In order to keep results as general

1723: as possible, we consider an arbitrary ordering $\preceq$ satisfying

1724: the following natural conditions.

1725: 

1726: \begin{description}

1727: 

1728: \item[Meaningful.] The ordering $\preceq$ is meaningful if, for any variable

1729: $h$ and any pair of sets $H'$ and $H''$ such that $h \not\in H' \cup H''$

1730: it holds:\eatpar

1731: 

1732: \[

1733: H' \cup \{h\} \preceq H'' \cup \{h\} ~~ \mbox{ iff } ~~ H' \preceq H''

1734: \]

1735: 

1736: Intuitively, a meaningful ordering compares two explanations

1737: $H'$ and $H''$ only on the variables they differ.

1738: 

1739: \item[Irredundant] The ordering $\preceq$ is irredundant if, for any pair

1740: of sets $H'$ and $H''$ it holds:\eatpar

1741: 

1742: \[

1743: H' \subset H'' ~~ \Rightarrow ~~ H' \prec H''

1744: \]

1745: 

1746: Irredundancy formalizes the natural assumption that

1747: hypotheses that are not necessary should be removed.

1748: 

1749: \end{description}

1750: 

1751: We determine the compilability of abduction with preference

1752: in the same way we did in the case of no ordering: we show

1753: that the function $i$ is a polynomial reduction from the

1754: problems of abduction to themselves, and that it satisfies

1755: the condition of representative equivalence.

1756: To this aim, we need the analogous of Lemma~\ref{basic} and

1757: Lemma~\ref{add-assumptions}.

1758: 

1759: 

1760: \begin{lemma}

1761: \label{basic-order}

1762: 

1763: If $\preceq$ is a meaningful ordering, it holds:\eatpar

1764: 

1765: \[

1766: SOL_\preceq(f(\l H,M,T \r)) =

1767: \{ S \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}

1768: ~|~ S \in SOL_\preceq(\l H,M,T \r) \}

1769: \]

1770: 

1771: \end{lemma}

1772: 

1773: \proof We use the result of Lemma~\ref{basic}. Namely, since all solutions

1774: of $f(\l H,M,T \r)$ coincide on $C \cup D$, these variables are irrelevant

1775: thanks to the fact that $\preceq$ is meaningful.

1776: 

1777: Formally, we have:\eatpar

1778: 

1779: \begin{eqnarray*}

1780: \lefteqn{S \in SOL_\preceq(f(\l H,M,T \r))} \\

1781: & \Leftrightarrow &

1782: S \in SOL(f(\l H,M,T \r)) \mbox{ and }

1783: \not\exists S' \in SOL(f(\l H,M,T \r)) ~.~ S' \preceq S

1784: \\

1785: & \Leftrightarrow &

1786: S = S_1 \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \},

1787: \\

1788: &&

1789: S_1 \in SOL(H,M,T) \mbox{ and }

1790: \\

1791: &&

1792: \not\exists S'_1 \in SOL(\l H,M,T \r) \mbox{ such that }

1793: \\

1794: && ~~~

1795: S'_1 \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}

1796: \prec S_1 \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}

1797: \\

1798: & \Leftrightarrow &

1799: S = S_1 \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}, ~~

1800: S_1 \in SOL(H,M,T) \mbox{ and }

1801: \\

1802: &&

1803: \not\exists S'_1 \in SOL(\l H,M,T \r) ~.~

1804: S'_1 \prec S_1

1805: \\

1806: & \Leftrightarrow &

1807: S = S_1 \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \}

1808: \mbox{ and }

1809: S_1 \in SOL_\preceq(\l H,M,T \r)

1810: \end{eqnarray*}

1811: 

1812: This proves the claim.~\qed

1813: 

1814: 

1815: We can also prove the analogous of Lemma~\ref{add-assumptions}.

1816: 

1817: \begin{lemma}

1818: \label{add-assumptions-order}

1819: 

1820: Let $c$ be a positive integer number and let $g_c$ be the following

1821: function:\eatpar

1822: 

1823: \[

1824: g_c(\l H,M,T \r) = \l H \cup \{ h_{|H|+1}, \ldots , h_c \}, M,

1825: T \cup \{ x_{r+1} \vee \neg x_{r+1}, \ldots , x_c \vee \neg x_c \} \r

1826: \]

1827: 

1828: \noindent where $r = |Var(T) \backslash H|$.

1829: If $\preceq$ is an irredundant ordering, it holds:\eatpar

1830: 

1831: \[

1832: SOL_\preceq(g_c(\l H,M,T \r)) = SOL_\preceq(\l H,M,T \r)

1833: \]

1834: 

1835: \end{lemma}

1836: 

1837: \proof Similar to the proof of Lemma~\ref{add-assumptions},

1838: but now the hypotheses in $\{ h_{|H|+1}, \ldots , h_c \}$

1839: are all irrelevant; therefore, they are not part of any

1840: minimal explanation.~\qed

1841: 

1842: These lemmas can be used to prove incompilability of abduction

1843: when an irredundant and meaningful ordering is used.

1844: 

1845: 

1846: %%%%%%%%%%%%% veri-nocl %%%%%%%%%%%%%%

1847: \subsection{Verification}

1848: 

1849: We consider the problem of verifying whether a set of

1850: assumptions is a minimal explanation according to the

1851: orderings $\leq$ and $\subseteq$. More generally, we

1852: prove the following theorem for any meaningful and

1853: irredundant ordering.

1854: 

1855: \begin{theorem}

1856: \label{veri-nocl}

1857: 

1858: If $\preceq$ is a meaningful and irredundant ordering, verifying whether a

1859: set of assumptions is a minimal explanation is \nucC-hard for any class \C\

1860: for which the problem is \C-hard.

1861: 

1862: \end{theorem}

1863: 

1864: \proof The same classification, representative, and extension

1865: functions used for the case of no ordering can be used for

1866: this case as well.

1867: 

1868: Let now consider the functions $f'$ and $g_c'$. From

1869: Lemma~\ref{basic-order} and Lemma~\ref{add-assumptions-order}

1870: it follows that they are reductions from the problem of

1871: verification to itself. Moreover, their composition $i'$

1872: satisfies representative equivalence.~\qed

1873: 

1874: 

1875: 

1876: %%%%%%%%%%%%% rele-nocl %%%%%%%%%%%%%%

1877: \subsection{Relevance, Dispensability, and Necessity}

1878: 

1879: We make the following simplifying assumption: given an

1880: instance of abduction $\l H,M,T \r$, where

1881: $H = \{h_1,\ldots,h_m\}$, the problem is to decide whether

1882: the first assumption $h_1$ is relevant/dispensable/necessary.

1883: There is no loss of generality in making this assumption.

1884: as we can always rename the variables appropriately.

1885: 

1886: \begin{theorem}

1887: \label{rele-nocl}

1888: 

1889: If $\preceq$ is a meaningful and irredundant ordering, then

1890: the problems of relevance/dispensability/necessity are

1891: \nucC-hard for any class \C\  of the polynomial hierarchy

1892: for which they are \C-hard.

1893: 

1894: \end{theorem}

1895: 

1896: \proof

1897: From Lemma~\ref{basic-order} and Lemma~\ref{add-assumptions-order},

1898: it follows that the reduction $i$ is a reduction from the problems of

1899: relevance/dispensability/necessity to themselves, if $\preceq$ is meaningful

1900: and irredundant, and it also satisfies representative equivalence.~\qed

1901: 

1902: Since $\subseteq$ and $\leq$ are meaningful irredundant orderings,

1903: their complexity implies their compilability characterization.

1904: 

1905: \begin{corollary}

1906: 

1907: Relevance and dispensability using $\subseteq$ are \nucS{2}-hard,

1908: while using $\leq$ they are \nucDlog{3}-hard. Necessity is

1909: \nucP{2}-hard and \nucDlog{3}-hard, using $\subseteq$ and $\leq$,

1910: respectively.

1911: 

1912: \end{corollary}

1913: 

1914: 

1915: 

1916: 

1917: 

1918: %%%%%%%%%%%%% prio %%%%%%%%%%%%%%

1919: \section{Compilability of Abduction: Prioritization and Penalization}

1920: 

1921: We consider the cases in which the ordering over the explanations is defined in

1922: terms of a prioritization. The instances of the problem are different from

1923: those of the previous section, since $H$ is replaced by a partition of

1924: assumptions $\l H_1,\ldots,H_m \r$.

1925: 

1926: In the cases of $\leq$-prioritization and $\subseteq$-prioritization,

1927: the induced ordering $\preceq$ is meaningful and irredundant. However,

1928: the results on meaningful irredundant ordering cannot be directly

1929: applied because, in Theorem~\ref{veri-nocl} and Theorem~\ref{rele-nocl},

1930: we assumed that the instances have the form $\l H,M,T \r$, while now

1931: they have the form $\l \l H_1,\ldots,H_m \r,M,T \r$.

1932: Therefore, we have to find new classification, representative,

1933: and extension functions.

1934: 

1935: We first consider the problem of verification, and prove 

1936: its nucomp-hardness. Then, we move to the problems of

1937: relevance, dispensability, and necessity. As for the

1938: case of $\leq$-preference and $\subseteq$-preference,

1939: we employee a sort of normal form, in which the assumption

1940: we check is the first one.

1941: 

1942: 

1943: \subsection{Verification}

1944: 

1945: First of all, we show the classification, representative,

1946: and extension functions for the problem of verification.

1947: The instances of the problem include a ``candidate

1948: explanation'' $H_a$. 

1949: 

1950: \begin{eqnarray*}

1951: \lefteqn{Class(\l \l H_1,\ldots,H_m \r,H_a,M,T \r)}

1952: \\

1953: &=&

1954: \max( m, |H_1|, \ldots, |H_m|, |\var(T) \backslash \cup H_i| )

1955: \\

1956: \lefteqn{Repr(c)}

1957: \\

1958: &=&

1959: \l \l \{ h^1_1,\ldots,h^1_c \} , \ldots , \{ h^c_1,\ldots,h^c_c \} \r,

1960: \emptyset, \emptyset,

1961: \Pi( \{ h^1_1,\ldots,h^1_c \} \cup \cdots \cup \{ h^c_1,\ldots,h^c_c \} \cup

1962:      \{ x_1,\ldots,x_c \} ) \r

1963: \\

1964: \lefteqn{Exte(\l \l H_1,\ldots,H_m \r,H_a,M,T \r,m)}

1965: \\

1966: &=&

1967: \l \l H_1,\ldots,H_c \r, H_a, M,

1968: T \cup \{ x_{r+1} \vee \neg x_{r+1}, \ldots, x_m \vee \neg x_m \} \r

1969: \\

1970: && \mbox{ where } r = | \var(T) \backslash \cup H_i |

1971: \end{eqnarray*}

1972: 

1973: These functions can be easily proved to be valid

1974: classification, representative, and extension functions.

1975: What is missing is a reduction from the problem of

1976: verification to itself satisfying the condition of

1977: representative equivalence.

1978: 

1979: To this extent, we use two functions $f''$ and $g_c''$

1980: that are similar to $f$ and $g_c$, respectively. In

1981: particular, $f(\l \l H_1,\ldots,H_m \r,H_a,M,T \r) =

1982: \l  \l H_1',\ldots,H_m' \r, H_a', M', T' \r$, where:\eatpar

1983: 

1984: \begin{eqnarray*}

1985: H_1' &=& H_1 \cup C \cup D \\

1986: H_2' &=& H_2 \\

1987: & \vdots & \\

1988: H_m' &=& H_m \\

1989: H_a' &=& H_a \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \} \\

1990: M' &=& M \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \} \\

1991: T' &=& \{ \neg c_i \vee \neg d_i ~|~ \gamma_i \in \Pi( \var(T) \cup \bigcup H_i ) \} \cup

1992:        \{ c_i \rightarrow \gamma_i ~| ~ \gamma_i \in \Pi( \var(T) \cup \bigcup H_i ) \}

1993: \end{eqnarray*}

1994: 

1995: Besides the partition of the assumptions, this is exactly the function used

1996: in Lemma~\ref{basic}. As a result, we have that:\eatpar

1997: 

1998: \[

1999: SOL(\l \l H_1',\ldots,H_m' \r, M', T' \r) =

2000: \{ S \cup \{ c_i ~|~ \gamma_i \in T \} \cup \{ d_i ~|~ \gamma_i \not\in T \} ~|~

2001: S \in SOL (\l \l H_1,\ldots,H_m \r, M, T \r ) \}

2002: \]

2003: 

2004: Since $\preceq$ is a meaningful irredundant ordering, the

2005: same property holds replacing $SOL$ with $SOL_\preceq$.

2006: The last step is to define a function $g_c''$ similar to

2007: $g_c$. This is done as follows.\eatpar

2008: 

2009: \begin{eqnarray*}

2010: \lefteqn{g_c''(\l \l H_1,\ldots,H_m \r, H_a, M, T \r) =} \\

2011: &&

2012: \l \l H_1 \cup \{ h^1_{|H_1|+1}, \ldots, h^1_c \} ,

2013:       \ldots,

2014:       H_m \cup \{ h^m_{|H_m|+1}, \ldots, h^m_c \} ,

2015:       \ldots,

2016:       \{ h^c_1,\ldots,h^c_c \} \r,

2017:    H_a, \\

2018: && M,

2019:    T \cup \{ x_{r+1} \vee \neg x_{r+1}, \ldots, x_c \vee \neg x_c \} \r \\

2020: && \mbox{ where } r = | \var(T) \backslash \bigcup H_i |

2021: \end{eqnarray*}

2022:    

2023: In words, each $H_i$ is extended with new assumptions to make

2024: it contain exactly $c$ assumptions. Some new classes of assumptions

2025: $H_i$ are added, in such a way the resulting instance contains

2026: exactly $c$ classes of assumptions. Finally, $T$ is extended

2027: with tautologies over new variables, in such a way the variables of the

2028: new theory that are not assumptions are exactly $c$.

2029: 

2030: The resulting instance is defined in such a way all its

2031: relevant numbers (number of classes of assumptions, number of

2032: assumptions in each class, number of other variables in the theory)

2033: coincide. The analogous of Lemma~\ref{add-assumptions-order} holds:

2034: the solutions of $\l \l H_1,\ldots,H_m \r, H_a, M, T \r$ and the

2035: solutions of $g_c''(\l \l H_1,\ldots,H_m \r, H_a, M, T \r)$ coincide.

2036: This is due to the fact that $g_c''$ only introduces new variables

2037: that are irrelevant to the minimal solutions.

2038: 

2039: \begin{theorem}

2040: 

2041: The problem of verification for any prioritization based on a meaningful and

2042: irredundant ordering is \nucC-hard for any class \C\  for which it is \C-hard.

2043: 

2044: \end{theorem}

2045: 

2046: \proof

2047: The composition of $i''$ of $f''$ and $g_c''$ is a reduction

2048: satisfying representative equivalence.

2049: 

2050: \[

2051: i''(\l \l H_1,\ldots,H_m \r, H_a, M, T \r) =

2052: f( g''_{Class(\l \l H_1,\ldots,H_m \r, H_a, M, T \r)} 

2053: (\l \l H_1,\ldots,H_m \r, H_a, M, T \r) )

2054: \]

2055: 

2056: The fact that is a reduction from the problem of verification to itself easily

2057: follows from the fact that both $f''$ and $g_c''$ are. Moreover, the result of

2058: $f( g''_{Class(\l \l H_1,\ldots,H_m \r, H_a, M, T \r)} (\l \l H_1,\ldots,H_m

2059: \r, H_a, M, T \r) )$ is an instance in which the number of classes of

2060: assumption, of variables in each class, and the number of other variables, all

2061: coincide with the class of the original instance. The function $f''$ produces

2062: an instance in which everything but $M$ and $H_a$ depends only on these

2063: numbers. As a result , the function $i$ produces an instance in which

2064: everything but $M$ and $H_a$ depends on the class of the original instance

2065: only. As a result, this function $i''$ is a reduction from the problem of

2066: verification to itself, satisfying representative equivalence, which implies

2067: the incompilability of the problem.~\qed

2068: 

2069: 

2070: 

2071: \subsection{Relevance and Necessity}

2072: 

2073: We restrict the problems to the case the assumption we

2074: want to check for relevance/dispensability/necessity

2075: is the first variable of $H_1$. The problems have the

2076: same complexity of the general ones (in which the assumption

2077: can be an arbitrary one.) This, however, cannot be proved

2078: with a simple renaming of the variables, as we did for

2079: the case of preference.

2080: 

2081: \begin{theorem}

2082: \label{first-of-first}

2083: 

2084: Let $\preceq$ be a meaningful and irredundant ordering.

2085: It holds:\eatpar

2086: 

2087: \begin{eqnarray*}

2088: & h^i_j \mbox{ is relevant/necessary for }

2089: \l \l H_1,\ldots,H_m \r, M, T \r & \\

2090: & \mbox{ iff } & \\

2091: & t \mbox{ is relevant/necessary for } \\

2092: &

2093: \l \l \{t, s\}, H_1,\ldots,H_m \r, M \cup \{u,v\}, T \cup

2094: \{ h^i_j \rightarrow u, t \rightarrow v,

2095: s \rightarrow u, s \rightarrow v \} \r &

2096: \end{eqnarray*}

2097: 

2098: \end{theorem}

2099: 

2100: \proof We first give an informal sketch of the proof.

2101: The set of solutions (with no ordering) of

2102: the first and the second instances only differ because

2103: the explanations for the second instances must contain

2104: either $s$ or both $h^i_j$ and $t$.

2105: 

2106: The explanations of the second instances are first compared

2107: on the assumptions in $H_1,\ldots,H_m$, and then on

2108: $\{s,t\}$. Therefore, the ordering for the second instance

2109: is a refinement of the ordering of the first one. Namely,

2110: a minimal solution of the second instances is either a

2111: minimal solution of the first one plus $s$, or a minimal

2112: solution of the first one plus $t$. However, the latter is

2113: a solution only if it contains $h^i_j$. Therefore, the

2114: presence of a solution containing $h^i_j$ in the first

2115: instance is equivalent to the presence of a solution for

2116: the second instance containing $t$.

2117: 

2118: The formal proof is as follows. Let $\l H,M,T \r$ be the

2119: first instance and $\l H',M',T \r$ be the second one.

2120: 

2121: \begin{enumerate}

2122: 

2123: \item $S' \in SOL(H',M',T')$ implies

2124: $S' \backslash \{s,t\} \in SOL(H,M,T)$.

2125: 

2126: This can be proved as follows. First, since $S' \cup T'$ is

2127: consistent, it follows that $S' \cup T$ is consistent as well

2128: (because $T \subseteq T'$), which also implies that

2129: $(S' \backslash \{s,t\}) \cup T$ is consistent.

2130: 

2131: Let us now prove that $(S' \backslash \{s,t\}) \cup T \models M$. By

2132: assumption, we have $S' \cup T' \models M'$. The following

2133: chain of implications leads to the claim.

2134: 

2135: \begin{eqnarray*}

2136: & S' \cup T' \models M \cup \{u, v\} & \\

2137: & \Downarrow & \\

2138: & S' \cup T' \models M & \\

2139: & \Downarrow & \\

2140: & S' \cup T' \cup \neg M \mbox{ is inconsistent} & \\

2141: & \Downarrow & \\

2142: & (S' \backslash \{s,t\}) \cup T \cup (S' \cap \{s,t\}) \cup

2143: \{ h^i_j \rightarrow u, t \rightarrow u, t \rightarrow v, s \rightarrow v \}

2144: \cup \neg M 

2145: \mbox{ is inconsistent} & \\

2146: & \mbox{ since $u$ and $v$ appears only positively, set $u=y=\true$ } & \\

2147: & \Downarrow & \\

2148: & (S' \backslash \{s,t\}) \cup T \cup (S' \cap \{s,t\}) \cup 

2149: \neg M \mbox{ is inconsistent} & \\

2150: & \mbox{ $s$ and $t$ appears (at most) once: they can be removed } & \\

2151: & \Downarrow & \\

2152: & (S' \backslash \{s,t\}) \cup T \cup \neg M \mbox{ is inconsistent} & \\

2153: & \Downarrow & \\

2154: & (S' \backslash \{s,t\}) \cup T \models M &

2155: \end{eqnarray*}

2156: 

2157: \item $S' \in SOL_\preceq(H',M',T')$ implies

2158: $S' \backslash \{s,t\} \in SOL_\preceq(H,M,T)$.

2159: 

2160: Proved by reductio ad absurdum. Assume that

2161: $S' \in SOL_\preceq(H',M',T')$, but that

2162: $S' \backslash \{s,t\} \not\in SOL_\preceq(H,M,T)$.

2163: As proved above, $S' \backslash \{s,t\} \in SOL(H,M,T)$.

2164: As a result, it is not minimal: there exists

2165: another $S'' \in SOL(H,M,T)$ such that

2166: $S''$ is better than $S' \backslash \{s,t\}$.

2167: As proved above, $S'' \cup \{s,t\} \in SOL_\preceq(H',M',T')$.

2168: Moreover, $S'' \cup \{s,t\}$ is better than $S'$, because

2169: $s$ and $t$ are in the lowest class of the prioritization.

2170: 

2171: \item If $h^i_j \in S$, then $S \in SOL_\preceq(H,M,T)$ if and only if

2172: $S \cup \{t\} \in SOL_\preceq(H',M',T')$.

2173: 

2174: By the point 1 and 2 above, if $S \cup \{t\}$ is a minimal solution of the

2175: second instance, then $S$ is a minimal solution of the first one. We prove the

2176: converse.

2177: 

2178: First of all, $S \cup \{t\}$ is solution of the second instance. What is left

2179: to prove is its minimality. This is also easy: removing $t$ leads to a set

2180: of assumptions which does not explain $v$. If removing some variable from $S$

2181: leads to another solution, then $S$ is not minimal.

2182: 

2183: \item If $h^i_j \not\in S$, then $S \in SOL_\preceq(H,M,T)$ if and only if

2184: $S \cup \{s\} \in SOL_\preceq(H',M',T')$.

2185: 

2186: The ``if'' direction is easy. Let us assume that $S$ is a minimal solution of

2187: the first instance. Then $S \cup \{s\}$ is a solution of the second one. Let us

2188: prove that it is minimal. We cannot remove variables from $S$, otherwise $S$

2189: would be not minimal. As a result, the only other possible explanations that

2190: can be preferred are $S \cup \{t\}$ and $S \cup \emptyset$. None of them is a

2191: solution, because they do not imply $u$.

2192: 

2193: \end{enumerate}

2194: 

2195: It is now possible to prove the claim. If there exists a minimal solution

2196: of the first instance containing $h^i_j$, then there exists a minimal solution

2197: of the second one containing $t$. On the other hand, if no minimal solution

2198: contains $h^i_j$, then all corresponding minimal solutions of the second

2199: instances contains $s$, which means that $t$ is in none of them.

2200: Therefore, relevance and necessity of $h^i_j$ on the first

2201: instance are equivalent to relevance and necessity, respectively,

2202: of $t$ in the second instance.~\qed

2203: 

2204: As a result of this theorem, we can assume that relevance or dispensability are

2205: evaluated w.r.t.\  the first variable in $H_1$. In order to prove that these

2206: problems are not compilable, we give a classification, representative, and

2207: extension function.\eatpar

2208: 

2209: \begin{eqnarray*}

2210: && Class( \l \l H_1,\ldots,H_m \r, M, T \r )

2211: =

2212: \max( m, |H_1|, \ldots, |H_m|, |Var(T) \backslash (H_1 \cup \cdots \cup H_m)| )

2213: \\

2214: && Repr(c)

2215: =

2216: \l \l \{h^1_1,\ldots,h^1_c\},\ldots,\{h^c_1,\ldots,h^c_c\} \r, \emptyset, \\

2217: && ~~~~~~~~~~~~~

2218: \Pi( \{h^1_1,\ldots,h^1_c\} \cup \cdots \cup \{h^c_1,\ldots,h^c_c\} \cup

2219: \{x_1,\ldots,x_c\}) \r

2220: \\

2221: &&Ext( \l \l H_1,\ldots,H_m \r, M, T \r, m )

2222: = \l \l H_1,\ldots,H_m \r, M,

2223: T \cup \{ x_{r+1} \vee \neg x_{r+1}, \ldots, x_m \vee\neg x_m \} \r \\

2224: && ~~~~~~~~~~~~~

2225: \mbox{ where } r = |Var(T) \backslash (H_1 \cup \cdots \cup H_m)|

2226: \end{eqnarray*}

2227: 

2228: Given these three functions, all is needed is a reduction from the problem of

2229: relevance to itself satisfying representative equivalence. The function $i''$

2230: cannot be used only because the instance it deals with contains the set of

2231: assumptions $H_a$. However, removing this part of the instance both from its

2232: argument and its result, we obtain a reduction with the right

2233: properties. We can thus conclude that the problems of relevance,

2234: dispensability, and necessity are incompilable.

2235: 

2236: \begin{theorem}

2237: 

2238: Let $\preceq$ be a meaningful and irredundant ordering. The problems of

2239: relevance, dispensability, and necessity for the problem of prioritized

2240: abduction are \nucC-hard for any class \C\  of the polynomial hierarchy for

2241: which these problems are \C-hard.

2242: 

2243: \end{theorem}

2244: 

2245: As a result, we easily obtain the compilability properties of the problem

2246: of prioritized abduction using the orderings $\subseteq$ and $\leq$.

2247: 

2248: \begin{theorem}

2249: 

2250: Relevance and dispensability are \nucS{3}-hard if $\subseteq$ is used,

2251: and \nucD{3}-hard if $\leq$ is used instead.

2252: 

2253: \end{theorem}

2254: 

2255: The compilability of relevance and dispensability in the case of penalization

2256: is an easy consequence of the last theorem, as relevance with $\leq$

2257: (prioritized) can be directly translated (using a nucomp reduction) to

2258: relevance with penalization.

2259: 

2260: \begin{corollary}

2261: 

2262: Relevance and dispensability are \nucD{3}-hard, in the case of penalization.

2263: 

2264: \end{corollary}

2265: 

2266: 

2267: 

2268: 

2269: \let\subsectionnewpage=\newpage

2270: 

2271: %%%%%%%%%%%%% horn %%%%%%%%%%%%%%

2272: \section{The Horn Case}

2273: 

2274: The Horn case can be dealt with using the same technique

2275: of the general case. Since, however, only Horn clauses

2276: are allowed, each time we use $\Pi(H \cup X)$, which

2277: contains all clauses of three literals over $H \cup X$,

2278: we have to replace it with the $\Pi_H(H \cup X)$ that

2279: contains all Horn clauses of three literals over the

2280: set $H \cup X$. The reductions we used employ clauses

2281: $\neg c_i \vee \neg d_i$ and $\neg c_i \vee \gamma_i$,

2282: which are Horn if $\gamma_i$ is Horn. The reduction

2283: used in Theorem~\ref{first-of-first} also involves Horn

2284: clauses only. Therefore, all results holding for the

2285: general case hold for the Horn case as well. Namely,

2286: all problems about Horn clauses are \nucC-hard for the

2287: same classes \C\  they are \C-hard.

2288: An important feature of reduction from the same problem

2289: is that it allows proving nucomp-hardness result even

2290: for a restriction of the problem, provided that these

2291: reduction do not transform an instance into a non-valid

2292: one (\eg, unless an Horn instance is mapped into a

2293: non-Horn one.)

2294: 

2295: The even more restricted case of definite Horn clauses,

2296: however, cannot be dealt with in the same manner. Indeed,

2297: the clauses $\neg c_i \vee \neg d_i$, are not definite.

2298: Some problems, however, becomes polynomial, in this case.

2299: Namely, all problems in the case of no order are polynomial,

2300: as well as necessity for $\subseteq$-preference. We only

2301: show that a reduction for the case of $\leq$-preference.

2302: As before, the problem is that of checking whether $h_1$

2303: is in an explanation of minimal size of $\l H,M,T \r$.

2304: Since $h_1$ is part of $H$, we regard $\l H,M,T \r$ as

2305: being the instance of the problem. The classification,

2306: representative, and extension functions are as usual

2307: (tautologies are definite Horn clauses.)

2308: 

2309: The reduction we use is based on the following function

2310: $f$, where $n = |H|$.

2311: 

2312: \begin{eqnarray*}

2313: f(\l H,M,N \r) &=&

2314: \l H',M',T' \r

2315: \\

2316: && \mbox{where} \\

2317: &&

2318: \begin{array}{rcl}

2319: H' &=&

2320: H \cup \{ c^j_i ~|~ \gamma_i \in \Pi_H(X \cup H), ~ 1 \leq j \leq n+1 \}

2321: \\

2322: M' &=&

2323: M \cup \{ c^j_i ~|~ \gamma_i \in T, ~ 1 \leq j \leq n+1 \}

2324: \\

2325: T' &=&

2326: \{ \gamma_i \vee \bigvee \{ \neg c^j_i ~|~  1 \leq j \leq n+1 \} ~|~

2327: \gamma_i \in \Pi_H(X \cup H) \}

2328: \end{array}

2329: \end{eqnarray*}

2330: 

2331: The idea is simply that of replicating each variable $c^j_i$

2332: for $n+1$ times. This way, if $S \subseteq H$, then a clause

2333: $\gamma_i$ holds in $S \cup T$ only if $S$ contains all

2334: clauses $c^j_i$.

2335: 

2336: The reduction is based on the following two facts:

2337: 

2338: \begin{enumerate}

2339: 

2340: \item definite Horn clauses are always consistent with

2341: sets of positive literals;

2342: 

2343: \item checking the existence of explanations is polynomial.

2344: 

2345: \end{enumerate}

2346: 

2347: Therefore, the instance $\l H,M,T \r$ can be solved by

2348: first checking whether it has explanations. If it has,

2349: we can reduce it to $\l H',M',T' \r$. Being both $T$ and

2350: $T'$ definite Horn theories, consistency is not an issue.

2351: In other words, $S \subseteq H$ is an explanation of the

2352: first instance if and only if $S \cup T \models M$, and

2353: the same for the second instance.

2354: 

2355: \begin{lemma}

2356: 

2357: For any $C' \subseteq C$ such that $|C'| \leq n$,

2358: it holds that $S$ is an explanation of $\l H,M,T \r$ if

2359: and only if $S \cup \{c^j_i ~|~ \gamma_i \in T \} \cup C'$

2360: is an explanation of $f(\l H,M,T \r)$.

2361: 

2362: \end{lemma}

2363: 

2364: \proof The definition of explanation for definite

2365: Horn clauses is: $S \subseteq H$ is an explanation

2366: if and only if $S \cup T \models M$. Consistency

2367: is not relevant, as any definite Horn theory is

2368: consistent with any set of positive literals.

2369: 

2370: Let us first assume that $S$ is an explanation

2371: of $\l H,M,T \r$, that is, $S \cup T \models M$.

2372: Since $\{c^j_i ~|~ \gamma_i \in T \} \cup T'$

2373: implies $\{c^j_i ~|~ \gamma_i \in T \} \cup T$,

2374: we conclude that $S \cup \{c^j_i ~|~ \gamma_i \in T \} \cup T$

2375: implies $M \cup \{c^j_i ~|~ \gamma_i \in T \}$.

2376: The set $S \cup \{c^j_i ~|~ \gamma_i \in T \}$

2377: is therefore an explanation because the latter

2378: set is indeed $M'$. The set $C'$ is not relevant

2379: to this part of the proof.

2380: 

2381: Let us now assume that

2382: $S' = S \cup \{c^j_i ~|~ \gamma_i \in T \} \cup C'$

2383: is an explanation of $f(\l H,M,T \r)$. Since $|C'| \leq n$,

2384: then $S'$ does not contain all $c^j_i$ for any $i$.

2385: Therefore, all clauses that are not in $T$ contains

2386: at least an unassigned $c^j_i$ in $S' \cup T'$.

2387: Therefore, these clauses are cannot be used to derive

2388: a single literal in $M'$. As a result,

2389: $S \cup \{c^j_i ~|~ \gamma_i \in T \} \cup T' \models M'$.

2390: This is equivalent to $S \cup T \models M$, that is,

2391: $S$ is an explanation of $\l H,M,T \r$.~\qed

2392: 

2393: This lemma can be used to relate the minimal

2394: explanations of the two instances.

2395: 

2396: \begin{lemma}

2397: 

2398: If $\l H,M,T \r$ has explanations, then

2399: $S$ is one of its minimal explanation if

2400: and only if

2401: $S \cup \{c^j_i ~|~ \gamma_i \in T \}$ is

2402: a minimal explanation of $f(\l H,M,T \r)$.

2403: 

2404: \end{lemma}

2405: 

2406: \proof The lemma above implies that $S$

2407: is an explanation if and only if 

2408: $S \cup \{c^j_i ~|~ \gamma_i \in T \}$ is

2409: an explanation, as this is the case of

2410: $C'=\emptyset$. Let us now prove that

2411: the minimality of these two explanations

2412: coincide.

2413: 

2414: Let us first assume that $S$ is a minimal

2415: explanation. We prove that

2416: $S'=S \cup \{c^j_i ~|~ \gamma_i \in T \}$

2417: is a minimal explanation of $\l H',M',T' \r$.

2418: By the lemma above, $S'$ is an explanation;

2419: we have therefore only left to prove that

2420: it is of minimal size. Assume that $S''$

2421: is another explanation of $\l H',M',T' \r$.

2422: By construction, $S''$ contains

2423: $\{c^j_i ~|~ \gamma_i \in T \}$. Therefore,

2424: $S''$ can be smaller than $S'$ only if

2425: $S'' \backslash \{c^j_i ~|~ \gamma_i \in T \}$

2426: is smaller than $S' \backslash \{c^j_i ~|~ \gamma_i \in T \}$.

2427: Since the latter coincide with $S' \cap H$,

2428: whose size is bounded by $n$, we have that

2429: $|S'' \backslash \{c^j_i ~|~ \gamma_i \in T \}| \leq n$.

2430: Therefore, $S''$ can be written as

2431: $S''=S''' \cup \{c^j_i ~|~ \gamma_i \in T \} \cup C'$

2432: with $|S''' \cup C'| < |S|$. The latter inequality

2433: implies $|C'| < n$: by the lemma above, $S'''$

2434: would be an explanation of $\l H,M,T \r$.

2435: Since $|S''' \cup C'| < |S|$, then $|S'''| < |S|$,

2436: that is, $S$ is not be minimal.

2437: 

2438: Let us now assume that

2439: $S'=S \cup \{c^j_i ~|~ \gamma_i \in T \}$

2440: is a minimal explanation of $\l H',M',T' \r$,

2441: and prove that $S$ is a minimal explanation

2442: of $\l H,M,T \r$. Assume, indeed, that

2443: $S''$ is a smaller explanation of $\l H,M,T \r$.

2444: By the lemma above, $S'' \cup \{c^j_i ~|~ \gamma_i \in T \}$

2445: would then be an explanation of $\l H',M',T' \r$

2446: smaller than $S'$.~\qed

2447: 

2448: The reduction can be defined as for the Horn

2449: case, by taking into account the fact that

2450: the original instance $\l H,M,T \r$ may not

2451: have any explanation. Such a reduction ratifies

2452: the condition of representative equivalence,

2453: thus proving that problems about $\leq$-preference

2454: are \nucC-hard whenever they are \C-hard. Similar

2455: reductions can be defined for the other orderings.

2456: 

2457: 

2458: 

2459: 

2460: 

2461: 

2462: 

2463: %%%%%%%%%%%%% concl %%%%%%%%%%%%%%

2464: \section{Conclusions}

2465: 

2466: In this paper, we have shown that logic-based

2467: abduction cannot be simplified by preprocessing

2468: the theory $T$ and the hypotheses $H$. In

2469: particular, this result holds for various kinds

2470: of explanation orderings, and also for the

2471: Horn restriction. These results have been proved

2472: using the technique of representative equivalence

2473: \cite{libe-01-jacm}; since reductions are from

2474: a problem to itself, they prove that a problem is

2475: ``compilability-hard'' for any class for which

2476: it is hard. In other words, we did not prove that

2477: a problem is hard for some class, but rather that

2478: it complexity decreases thanks to preprocessing.

2479: Using these ``self-reductions'' allows for proving

2480: such a result even if the complexity of the problem

2481: is not known. For example, we prove that a

2482: preprocessing step does not simplify the problem

2483: of finding a minimal explanation for any ordering

2484: that is both meaningful and irredundant. The

2485: complexity of this problem is not known for

2486: all such orderings; moreover, it depends on the

2487: ordering itself.

2488: 

2489: The technique we used to prove that ``preprocessing

2490: does not simplify abduction'', being based on

2491: complexity classes at last, should however not

2492: be considered as implying that preprocessing is

2493: not useful for speeding up solving of abduction

2494: problems. Indeed, as for any result based on the

2495: theory of \np-completeness, this conclusion

2496: only holds as a worst-case result. In other words,

2497: it does not tell that no instance can ever by

2498: made simpler by preprocessing, but simply that any

2499: preprocessing procedure necessarily has some hard

2500: instances that are not simplified. In a sense,

2501: our result is more positive than it appears, as it

2502: tells that a worst-case exponential on-line

2503: algorithm is reasonable, given than no

2504: worst-case polynomial one exists.

2505: 

2506: Compilability results based on hardness and reductions

2507: have consequences similar to complexity results based

2508: on the theory of \np-completeness: they tell that,

2509: since no worst-case polynomial algorithm can solve

2510: the problem, alternative directions have to be considered.

2511: Approximation is one example: the preprocessing phase

2512: may result in some data structure that allows a

2513: better (or faster) approximation of the best

2514: abductive explanations. Another possible direction

2515: is that of incomplete compilation, in which the

2516: preprocessing phase produces a result that is only

2517: useful in some cases, but not always. Another common

2518: solution to hard-to-compile problems is that of

2519: generating a worst-case exponential preprocessing

2520: result. This approach is especially useful if part

2521: of the result can be used, as we can then try to

2522: generate it and use only the part we can store. All

2523: these alternative approaches, however, only make

2524: sense when the impossibility of preprocessing the

2525: problem into a polynomial problem has been proved.

2526: This is the practical impact of our hardness results.

2527: 

2528: Finally, compilability has been proved to be related

2529: to expressibility of logical formalisms, that is, their

2530: ability of representing information in little space

2531: \cite{cado-etal-00}. Logical-based abduction formalisms

2532: could then be characterized by the set of abductive

2533: problems they are able to express. Compilation  classes

2534: (and not complexity ones) have been proved useful to

2535: this aim.

2536: 

2537: 

2538: 

2539: 

2540: \let\sectionnewpage=\newpage

2541: 

2542: \bibliographystyle{alpha}

2543: \begin{thebibliography}{BATJ89}

2544: 

2545: \bibitem[BATJ89]{byla-etal-89}

2546: T.~Bylander, D.~Allemang, M.~C. Tanner, and J.~R. Josephson.

2547: \newblock Some results concerning the computational complexity of abduction.

2548: \newblock In {\em Proceedings of the First International Conference on the

2549:   Principles of Knowledge Representation and Reasoning (KR'89)}, pages 44--54,

2550:   1989.

2551: 

2552: \bibitem[CDLS00]{cado-etal-00}

2553: M.~Cadoli, F.~M. Donini, P.~Liberatore, and M.~Schaerf.

2554: \newblock Space efficiency of propositional knowledge representation

2555:   formalisms.

2556: \newblock {\em Journal of Artificial Intelligence Research}, 13:1--31, 2000.

2557: 

2558: \bibitem[CDLS02]{cado-etal-02}

2559: M.~Cadoli, F.~M. Donini, P.~Liberatore, and M.~Schaerf.

2560: \newblock Preprocessing of intractable problems.

2561: \newblock {\em Information and Computation}, 176(2):89--120, 2002.

2562: 

2563: \bibitem[CPT96]{cons-port-dupr-96}

2564: L.~Console, L.~Portinale, and D.~{Theseider Dupr\'{e}}.

2565: \newblock Using compiled knowledge to guide and focus abductive diagnosis.

2566: \newblock {\em {IEEE} Transactions on Knowledge and Data Engineering},

2567:   8(5):690--706, 1996.

2568: 

2569: \bibitem[EG95]{eite-gott-95-a}

2570: T.~Eiter and G.~Gottlob.

2571: \newblock The complexity of logic-based abduction.

2572: \newblock {\em Journal of the {ACM}}, 42(1):3--42, 1995.

2573: 

2574: \bibitem[EM02]{eite-maki-02}

2575: T.~Eiter and K.~Makino.

2576: \newblock On computing all abductive explanations.

2577: \newblock In {\em Proceedings of the Eighteenth National Conference on

2578:   Artificial Intelligence (AAAI~2002)}, pages 62--67, 2002.

2579: 

2580: \bibitem[GJ79]{gare-john-79}

2581: M.~R. Garey and D.~S. Johnson.

2582: \newblock {\em Computers and Intractability: {A} Guide to the Theory of

2583:   {NP}-Completeness}.

2584: \newblock W.H. Freeman and Company, San Francisco, Ca, 1979.

2585: 

2586: \bibitem[KL80]{karp-lipt-80}

2587: R.~M. Karp and R.~J. Lipton.

2588: \newblock Some connections between non-uniform and uniform complexity classes.

2589: \newblock In {\em Proceedings of the Twelfth ACM Symposium on Theory of

2590:   Computing (STOC'80)}, pages 302--309, 1980.

2591: 

2592: \bibitem[Lib01]{libe-01-jacm}

2593: P.~Liberatore.

2594: \newblock Monotonic reductions, representative equivalence, and compilation of

2595:   intractable problems.

2596: \newblock {\em Journal of the {ACM}}, 48(6):1091--1125, 2001.

2597: 

2598: \bibitem[MF96]{cial-96}

2599: M.~Cialdea Mayer and F.Pirri.

2600: \newblock Abduction is not deduction-in-reverse.

2601: \newblock {\em {J}ournal of the {IGPL}}, 4(1):86--104, 1996.

2602: 

2603: \bibitem[Pei55]{peir-55}

2604: C.~S. Peirce.

2605: \newblock Abduction and induction.

2606: \newblock In J.~Buchler, editor, {\em Philosophical Writings of Peirce},

2607:   chapter~11. Dover, New York, 1955.

2608: 

2609: \bibitem[SL90]{selm-leve-90}

2610: B.~Selman and H.~J. Levesque.

2611: \newblock Abductive and default reasoning: {A} computational core.

2612: \newblock In {\em Proceedings of the Eighth National Conference on Artificial

2613:   Intelligence (AAAI'90)}, pages 343--348, 1990.

2614: 

2615: \bibitem[Sto76]{stoc-76}

2616: L.~J. Stockmeyer.

2617: \newblock The polynomial-time hierarchy.

2618: \newblock {\em Theoretical Computer Science}, 3:1--22, 1976.

2619: 

2620: \bibitem[Yap83]{yap-83}

2621: C.~K. Yap.

2622: \newblock Some consequences of non-uniform conditions on uniform classes.

2623: \newblock {\em Theoretical Computer Science}, 26:287--300, 1983.

2624: 

2625: \end{thebibliography}

2626: 

2627: \end{document}

2628: 

2629: