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.