命題的周縁化のための最小還元

Circumscription is an important logic framework for representing and reasoning common-sense knowledge. With efficient implementations for circumscription, including circ2dlp and aspino, it has been widely used in model-based diagnosis and other domains. We propose a notion of minimal reduct for propositional circumscription and prove a characterization theorem, i.e., that the models of a circumscription can be obtained from the minimal reduct of the circumscription. With the help of the minimal reduct, a new method circ-reduct for computing models of circumscription is presented. It iteratively computes smaller models under set inclusion (if possible), and the minimal reduct is used to simplify the circumscription in each iteration. The algorithm is proved to be correct. Extensive experiments are conducted on circuit diagnosis ISCAS85, random CNF instances, and some industrial SAT instances for the international SAT competition. These results demonstrate that the minimal reduct is effective in computing circumscription models. Compared to the widely used circumscription solver circ2dlp using the state-of-the-art answer set programming solver clingo, our algorithm circ-reduct achieves significantly shorter CPU time. Compared with aspino using glucose as the internal SAT solver and unsatisfiable core analysis technique, our algorithm achieves better CPU time for random and industrial CNF benchmarks, while it is comparable for circuit diagnosis benchmarks.