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