Fixed-parameter tractability of satisfying beyond the number of variables

Abstract: 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 i n V (F)

and

c i n F

if

v i n c

or

. The matching number

u (F)

of

F

is the size of a maximum matching in

B_{F}

. In our main result, we prove that the following parameterization of {sc MaxSat} (denoted by

(u (F) + k)

- extsc{SAT}) is fixed-parameter tractable: Given a formula

F

, decide whether we can satisfy at least

u (F) + k

clauses in

F

, where

k

is the parameter. A formula

F

is called variable-matched if

u (F) = | V (F) | .

Let

d e l t a (F) = | F | - | V (F) |

and

d e l t a^{*} (F) = m a x_{F^{'} s u b s e t e q F} d e l t a (F^{'}) .

Our main result implies fixed-parameter tractability of {sc MaxSat} parameterized by

d e l t a (F)

for variable-matched formulas

F

; this complements related results of Kullmann (2000) and Szeider (2004) for {sc MaxSat} parameterized by

d e l t a^{*} (F)

. To obtain our main result, we reduce

(u (F) + k)

- extsc{SAT} into the following parameterization of the {sc Hitting Set} problem (denoted by

(m - k)

-{sc Hitting Set}): given a collection

c a l C

of

m

subsets of a ground set

U

of

n

elements, decide whether there is

X s u b s e t e q U

such that

C c a p X e q e m p t y s e t

for each

C i n c a l C

and

| X | l e m - k,

where

k

is the parameter. Gutin, Jones and Yeo (2011) proved that

(m - k)

-{sc Hitting Set} is fixed-parameter tractable by obtaining an exponential kernel for the problem. We obtain two algorithms for

(m - k)

-{sc Hitting Set}: a deterministic algorithm of runtime

O ((2 e)^{2 k + O (l o g^{2} k)} (m + n)^{O (1)})

and a randomized algorithm of expected runtime

O (8^{k + O (s q r t k)} (m + n)^{O (1)})

. Our deterministic algorithm improves an algorithm that follows from the kernelization result of Gutin, Jones and Yeo (2011).

Recommendations

Cites work

Cited in

(3)

This page was built for publication: Fixed-parameter tractability of satisfying beyond the number of variables