TR14-031 Authors: Joao Marques-Silva, Mikolas Janota

Publication: 7th March 2014 09:40

Downloads: 1805

Keywords:

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.