TY - JOUR

T1 - A dichotomy in the complexity of propositional circumscription

AU - Kirousis, Lefteris M.

AU - Kolaitis, Phokion G.

PY - 2001

Y1 - 2001

N2 - The inference problem for propositional circumscription is known to be highly intractable and, in fact, harder than the inference problem for classical propositional logic. More precisely, in its full generality this problem is II2P-complete, which means that it has the same inherent computational complexity as the satisfiability problem for quantified Boolean formulas with two alternations (universal-existential) of quantifiers. We use Schaefer's framework of generalized satisfiability problems to study the family of all restricted cases of the inference problem for propositional circumscription. Our main result yields a complete classification of the "truly hard" (II2P-complete) and the "easier" cases of this problem (reducible to the inference problem for classical propositional logic). Specifically, we establish a dichotomy theorem which asserts that each such restricted case either is II2P-complete or is in coNP. Morever, we provide efficiently checkable criteria that tell apart the "truly hard" cases from the "easier" ones.

AB - The inference problem for propositional circumscription is known to be highly intractable and, in fact, harder than the inference problem for classical propositional logic. More precisely, in its full generality this problem is II2P-complete, which means that it has the same inherent computational complexity as the satisfiability problem for quantified Boolean formulas with two alternations (universal-existential) of quantifiers. We use Schaefer's framework of generalized satisfiability problems to study the family of all restricted cases of the inference problem for propositional circumscription. Our main result yields a complete classification of the "truly hard" (II2P-complete) and the "easier" cases of this problem (reducible to the inference problem for classical propositional logic). Specifically, we establish a dichotomy theorem which asserts that each such restricted case either is II2P-complete or is in coNP. Morever, we provide efficiently checkable criteria that tell apart the "truly hard" cases from the "easier" ones.

UR - http://www.scopus.com/inward/record.url?scp=0034865416&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0034865416&partnerID=8YFLogxK

U2 - 10.1109/LICS.2001.932484

DO - 10.1109/LICS.2001.932484

M3 - Article

AN - SCOPUS:0034865416

SN - 1043-6871

SP - 71

EP - 80

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

ER -