Parameterized complexity of Weighted Satisfiability with few variable occurrences

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).

• How would one show "that this problem is NP-complete in classical complexity even if we fix l to be 3"? $\;\;\;\;\;\;$ – user12859 May 23 '15 at 1:35
• 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) – Martin Lackner May 26 '15 at 10:03
• 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. $\;\;\;\;$ – user12859 May 26 '15 at 10:24
• 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. – Martin Lackner May 27 '15 at 14:52