Abstract

Propositional circumscription selects models that are minimal with respect to designated atoms while permitting another set of atoms to vary. For a clause theory φ, minimized atoms P, varied atoms Z, and a candidate interpretation M, the minimal-reduct characterization reduces candidate-model checking to the entailment Red[φ;P;Z,M]⊧⋀(M∩P). We establish a structural decomposition of this entailment using the collapsed negative dependency graph of the reduct. Each selected source component induces a scoped entailment, and the global entailment is equivalent to the finite sequence of local obligations generated by successive contraction. The proof combines graph-based source selection, constructive extension of scoped countermodels, and preservation under contraction. These results yield a sound and complete checker that contracts certified minimized atoms and records origin-preserving certificate fragments over the original clauses. We instantiate the framework by direct SAT-based entailment checking and MUS-based support extraction. Experiments on 5445 random 3CNF instances and 462 industrial CNF instances show complete agreement with the global reduct criterion, and every generated certificate is successfully replayed. MUS-based extraction reduces the mean accumulated support size by 97.4% and 99.85% on the two benchmark collections, respectively, while incurring additional running time. The results provide a formal basis for local, replayable certification of propositional circumscription models.

Keywords