4
$\begingroup$

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This problem is W[2]-complete with respect to the parameter $k$.

Let $l$ be the maximum number of clauses that share a common variable, i.e., how often a variable occurs at most in $\phi$. My question is the following: What is the complexity of Weighted Satisfiability parameterized by both $k$ and $l$? Is anyone aware of work in this regard?

Note that this problem is NP-complete in classical complexity even if we fix $l$ to be 3, as we can introduce add copies of the variables and make them equivalent ($a\leftrightarrow a'$). This idea does not help in the parameterized setting with $k$ and $l$ as parameters, as it would require unbounded $k$ (all copies have to be set to true).

This problem seems to be connected to the model checking problem p-MC with bounded degree: Given a first-order logic $\psi$ formula and a labelled graph $G$, decide if G is a model of $\psi$. (See Logic, Graphs and Algorithms by Martin Grohe pdf)

This problem is fixed-parameter tractable with respect to the parameters length of $\psi$ and maximum degree of $G$. In principle, Weighted Satisfiability (with bounded occurrences) can be translated to a p-MC instance, but I do not see how to achieve this with bounded degree. Vertices corresponding to variables would have bounded degree (they are only connected to a bounded number of clauses), but vertices corresponding to clauses could have unbounded degree (they may contain a large number of variables).

$\endgroup$
4
  • $\begingroup$ How would one show "that this problem is NP-complete in classical complexity even if we fix l to be 3"? $\;\;\;\;\;\;$ $\endgroup$
    – user12859
    May 23, 2015 at 1:35
  • $\begingroup$ By a reduction from Satisfiability. First, Weighted Satisfiability with arbitrary $k$ is "plain" Satisfiability (by setting $k$ to the number of variables). Then, we replace the $i$-th occurrence of a variable $v$ with a new variable $v_i$. As a last step, we make all copies of $v$ equivalent by adding two clauses $(\neg v_i \vee v_j)\wedge (\neg v_j \vee v_i)$ for all i,j. Each $v_i$ appears at most three times (once in the original formula, twice in the two clauses establishing equivalence) $\endgroup$ May 26, 2015 at 10:03
  • $\begingroup$ Which "two clauses establishing equivalence"? $\:$ Your sentence before that would put in one pair of clauses involving $v_i$ for each other occurrence of $v$ in the original formula. $\;\;\;\;$ $\endgroup$
    – user12859
    May 26, 2015 at 10:24
  • $\begingroup$ In my previous comment I wrote that we establish equivalence for all $i,j$ - this is nonsense since it would increase $l$ too much. Sorry. To ensure that $l=3$, we actually need an implication cycle: If variable $v$ appears $r$ times, we have $v_1,\ldots,v_r$. We create an implication between $v_1$ and $v_2$ ($v_1\implies v_2$), $v_2$ and $v_3$ ($v_2\implies v_3$), etc, and finally between $v_r$ and $v_1$ ($v_r\implies v_1$). This implication cycle ensures that either all or none of the $v_i$'s are set to true. Now each $v_i$ occurs twice in an implication and once in the original formula. $\endgroup$ May 27, 2015 at 14:52

1 Answer 1

1
$\begingroup$

As I stumbled upon this today and found after some further research out that this has been solved, I want to mention this here.

screenshot of abstract

By this, the asked problem is FPT (so $t=0$ for the last sentence in the abstract).

The paper is "On the parameterized complexity of (k,s)-SAT" by Paulusma and Szeider, Inf. Proc. Letter, Volume 143, March 2019, Pages 34-36.

https://www.sciencedirect.com/science/article/abs/pii/S002001901830228X?via%3Dihub

Here is also a version not behind the Elsevier-paywall: https://www.ac.tuwien.ac.at/files/tr/ac-tr-18-008.pdf

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.