Fixed-parameter tractability of satisfying beyond the number of variables

preprint2012arXivOpen access

Abstract

We consider a CNF formula FF as a multiset of clauses: F={c1,...,cm}F=\{c_1,..., c_m\}. The set of variables of FF will be denoted by V(F)V(F). Let BFB_F denote the bipartite graph with partite sets V(F)V(F) and FF and with an edge between v∈V(F)v \in V(F) and c∈Fc \in F if v∈cv \in c or vˉ∈c\bar{v} \in c. The matching number ν(F)ν(F) of FF is the size of a maximum matching in BFB_F. In our main result, we prove that the following parameterization of {\sc MaxSat} (denoted by (ν(F)+k)(ν(F)+k)-\textsc{SAT}) is fixed-parameter tractable: Given a formula FF, decide whether we can satisfy at least ν(F)+kν(F)+k clauses in FF, where kk is the parameter. A formula FF is called variable-matched if ν(F)=∣V(F)∣.ν(F)=|V(F)|. Let δ(F)=∣F∣−∣V(F)∣δ(F)=|F|-|V(F)| and δ∗(F)=max⁡F′⊆Fδ(F′).δ^*(F)=\max_{F'\subseteq F} δ(F'). Our main result implies fixed-parameter tractability of {\sc MaxSat} parameterized by δ(F)δ(F) for variable-matched formulas FF; this complements related results of Kullmann (2000) and Szeider (2004) for {\sc MaxSat} parameterized by δ∗(F)δ^*(F). To obtain our main result, we reduce (ν(F)+k)(ν(F)+k)-\textsc{SAT} into the following parameterization of the {\sc Hitting Set} problem (denoted by (m−k)(m-k)-{\sc Hitting Set}): given a collection C\cal C of mm subsets of a ground set UU of nn elements, decide whether there is X⊆UX\subseteq U such that C∩X≠∅C\cap X\neq \emptyset for each C∈CC\in \cal C and ∣X∣≤m−k,|X|\le m-k, where kk is the parameter. Gutin, Jones and Yeo (2011) proved that (m−k)(m-k)-{\sc Hitting Set} is fixed-parameter tractable by obtaining an exponential kernel for the problem. We obtain two algorithms for (m−k)(m-k)-{\sc Hitting Set}: a deterministic algorithm of runtime O((2e)2k+O(log⁡2k)(m+n)O(1))O((2e)^{2k+O(\log^2 k)} (m+n)^{O(1)}) and a randomized algorithm of expected runtime O(8k+O(k)(m+n)O(1))O(8^{k+O(\sqrt{k})} (m+n)^{O(1)}). Our deterministic algorithm improves an algorithm that follows from the kernelization result of Gutin, Jones and Yeo (2011).

Explore this paper’s authors, topics and related work.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Reviews 0

Write a reviewWrite

No reviews yet.

Discussion 0

Add a commentWrite

No comments yet.