Complexity of Reasoning with Cardinality Minimality Conditions

TL;DR

This paper analyzes the computational complexity of the CardMinSat problem, which involves determining the truth of an atom in a cardinality-minimal model of a propositional formula, providing a complete classification within Schaefer's framework.

Contribution

It offers a complete complexity classification of CardMinSat, a problem relevant to AI reasoning, using advanced algebraic tools within Schaefer's propositional logic framework.

Findings

Classified the complexity of CardMinSat across all propositional logic fragments.

Identified tractable and intractable cases within Schaefer's framework.

Enhanced understanding of minimality conditions in AI reasoning problems.

Abstract

Many AI-related reasoning problems are based on the problem of satisfiability of propositional formulas with some cardinality-minimality condition. While the complexity of the satisfiability problem (SAT) is well understood when considering systematically all fragments of propositional logic within Schaefer's framework (STOC 1978) this is not the case when such minimality condition is added. We consider the CardMinSat problem, which asks, given a formula F and an atom x, whether x is true in some cardinality-minimal model of F. We completely classify the computational complexity of the CardMinSat problem within Schaefer's framework, thus paving the way for a better understanding of the tractability frontier of many AI-related reasoning problems. To this end we use advanced algebraic tools developed by (Schnoor & Schnoor 2008) and (Lagerkvist 2014).