TY - GEN

T1 - On the complexity of model checking and inference in minimal models extended abstract

AU - Kirousis, Lefteris M.

AU - Kolaitis, Phokion G.

PY - 2001

Y1 - 2001

N2 - Every logical formalism gives rise to two fundamental algorithmic problems: model checking and inference. In propositional logic, the model checking problem is polynomial-time solvable, while the inference problem is coNP-complete. In propositional circumscription, however, these problems have higher computational complexity, namely the model checking problem is coNP-complete, while the inference problem is πP/2 -complete. In this paper, we survey recent results on the computational complexity of restricted cases of these problems in the context of Schaefer's framework of generalized satisfiability problems. These results establish dichotomies in the complexity of the model checking problem and the inference problem for propositional circumscription. Specifically, in each restricted case the model checking problem for propositional circumscription either is coNP-complete or is polynomial-time solvable. Furthermore, in each restricted case the inference problem for propositional circumscription either is πP/2 -complete or is in coNP. These dichotomy theorems yield a complete classification of the "hard" and the "easier" cases of the model checking problem and the inference problem for propositional circumscription. Moreover, they provide efficiently checkable criteria that tell apart the "hard" cases from the "easier" ones.

AB - Every logical formalism gives rise to two fundamental algorithmic problems: model checking and inference. In propositional logic, the model checking problem is polynomial-time solvable, while the inference problem is coNP-complete. In propositional circumscription, however, these problems have higher computational complexity, namely the model checking problem is coNP-complete, while the inference problem is πP/2 -complete. In this paper, we survey recent results on the computational complexity of restricted cases of these problems in the context of Schaefer's framework of generalized satisfiability problems. These results establish dichotomies in the complexity of the model checking problem and the inference problem for propositional circumscription. Specifically, in each restricted case the model checking problem for propositional circumscription either is coNP-complete or is polynomial-time solvable. Furthermore, in each restricted case the inference problem for propositional circumscription either is πP/2 -complete or is in coNP. These dichotomy theorems yield a complete classification of the "hard" and the "easier" cases of the model checking problem and the inference problem for propositional circumscription. Moreover, they provide efficiently checkable criteria that tell apart the "hard" cases from the "easier" ones.

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

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

U2 - 10.1007/3-540-45402-0_3

DO - 10.1007/3-540-45402-0_3

M3 - Conference contribution

AN - SCOPUS:34547210373

SN - 3540425934

SN - 9783540425939

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 42

EP - 53

BT - Logic Programming and Nonmonotonic Reasoning - 6th International Conference, LPNMR 2001, Proceedings

T2 - 6th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2001

Y2 - 17 September 2001 through 19 September 2001

ER -