Parameterized complexity of weighted satisfiability problems: decision, enumeration, counting (Q2805407)

From the text: The goal of this paper is to show that Post's lattice allows to completely classify the complexity of weighted satisfiability for all possible sets of allowed Boolean functions. We consider both circuits and formulae, and the complexity to decide whether they admit a satisfying assignment of weight exactly \(k\). We show that depending on the set \(B\) of allowed connectives the parametrized weighted satisfiability problem is either W[P]-complete (for circuits) and W[SAT]-complete for formulae, or in P. More precisely, we prove that the complexity of these problems is W[P]-complete or W[SAT]-complete (depending on whether they concern circuits or formulae) as soon as \(B\) can express either the function \(x\wedge (y\vee z)\), or any 2-threshold function as for example the ternary majority function. The problem becomes solvable in polynomial time in all remaining cases. Thus, in a sense, we exactly pinpoint the reason for intractability of weighted satisfiability by exhibiting which Boolean functions make the problem hard.NEWLINENEWLINEBesides the decision problem, we study the complexity of the corresponding enumeration and counting problems. For those problems with efficient decision algorithms we provide efficient enumeration algorithms (in the sense of a polynomial delay). Also for counting we prove a dichotomy theorem in showing that the problems are either \#W[P]-complete (or \#W[SAT]-complete), or in FP (the class of functions computable in polynomial time). The frontier of this dichotomy is not the same as in the decision case, since some tractable decision problems, as, e.g., the weighted satisfiability problem in which only the connective \(\rightarrow\) is allowed, become hard counting problems.