Fixed-parameter tractability of satisfying beyond the number of variables

Robert Crowston, Gregory Gutin*, Mark Jones, Venkatesh Raman, Saket Saurabh, Anders Yeo

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review


We consider a CNF formula F as a multiset of clauses: F={c 1,.,c m }. The set of variables of F will be denoted by V(F). Let B F denote the bipartite graph with partite sets V(F) and F and with an edge between vâ̂̂V(F) and câ̂̂F if vâ̂̂c or \bar{v} \in c. The matching number ν(F) of F is the size of a maximum matching in B F . In our main result, we prove that the following parameterization of MaxSat (denoted by (ν(F)+k)-SAT) is fixed-parameter tractable: Given a formula F, decide whether we can satisfy at least ν(F)+k clauses in F, where k is the parameter. A formula F is called variable-matched if ν(F)=|V(F)|. Let δ(F)=|F|-|V(F)| and δ â̂ - (F)=max F′⊆F δ(F′). Our main result implies fixed-parameter tractability of MaxSat parameterized by δ(F) for variable-matched formulas F; this complements related results of Kullmann (IEEE Conference on Computational Complexity, pp. 116-124, 2000) and Szeider (J. Comput. Syst. Sci. 69(4):656-674, 2004) for MaxSat parameterized by δ â̂ - (F). To obtain our main result, we reduce (ν(F)+k)-SAT into the following parameterization of the Hitting Set problem (denoted by (m-k)-Hitting Set): given a collection \mathcal{C} of m subsets of a ground set U of n elements, decide whether there is X⊆U such that Câ̂

Original languageEnglish
Issue number3
Pages (from-to)739-757
Publication statusPublished - 2014
Externally publishedYes


Dive into the research topics of 'Fixed-parameter tractability of satisfying beyond the number of variables'. Together they form a unique fingerprint.

Cite this