I have the following problem. Given a below boolean formula (of the type explained below) containing $n$ literals and two parameter $k$ and $l$, come up with a satisfying assignment of literals such that no more than $k$ of them are set to true. ($l$ will be explained below.)
An example boolean formula with 4 literals is as follows: $ (x_1 \lor (x_2 \land x_4)) \land (x_2 \lor (x_3 \land x_1)) \land (x_3 \lor (x_4 \land x_1)) \land (x_4 \lor (x_3 \land x_2)) $. Some properties of the kind of formulae I am dealing with:
- The number of outermost clauses (connected via AND) is same as the number of literals.
- There is a restriction on size of the innermost AND clauses, they can have at most $l$ literals. For example $l=2$ in the example above.
I did some literature search to realize that this is called as the "Monotone circuit satisfiability" problem in the complexity parameterization literature. My interest in the problem is largely practical, so I am looking for the best approximation algorithm known for the above problem. Any help / suggestions are much appreciated.