On the Query Complexity of Selecting Few Minimal Sets.
João P. Marques-Silva, Mikoláš Janota · Electronic colloquium on computational complexity · 2014
Propositional Satisfiability (SAT) solvers are routinely used for solving many function problems. A natural question that has seldom been addressed is: what is the best worst-case number of calls to a SAT solver for solving some target function problem? This paper develops tighter upper bounds on the query complexity of solving several function problems defined on propositional formulas. These include computing the backbone of a formula and computing the set of independent variables of a formula. For the general case, the paper develops tighter upper bounds on the query complexity of computing a minimal set when the number of minimal sets is constant. This applies for example to the computation of a minimal unsatisfiable subset (MUS) for CNF formulas, but also to the computation of prime implicants and implicates.