Counterexample Guided Abstraction Refinement Algorithm for Propositional\n Circumscription

Circumscription is a representative example of a nonmonotonic reasoning\ninference technique. Circumscription has often been studied for first order\ntheories, but its propositional version has also been the subject of extensive\nresearch, having been shown equivalent to extended closed world assumption\n(ECWA). Moreover, entailment in propositional circumscription is a well-known\nexample of a decision problem in the second level of the polynomial hierarchy.\nThis paper proposes a new Boolean Satisfiability (SAT)-based algorithm for\nentailment in propositional circumscription that explores the relationship of\npropositional circumscription to minimal models. The new algorithm is inspired\nby ideas commonly used in SAT-based model checking, namely counterexample\nguided abstraction refinement. In addition, the new algorithm is refined to\ncompute the theory closure for generalized close world assumption (GCWA).\nExperimental results show that the new algorithm can solve problem instances\nthat other solutions are unable to solve.\n