Decomposition-Based Checking and Local Certification for Propositional Circumscription via Minimal Reducts

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.