Approximation algorithms for an instance of the Monotone circuit satisfiability

Question

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:

1. The number of outermost clauses (connected via AND) is same as the number of literals.
2. 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.

Answer 1

If this is a practical problem, rather than an approximation algorithm, I suggest using an off-the-shelf SAT solver. There are standard ways to encode the constraint that at most $k$ variables are set to true, using an at-most-$k$-out-of-$n$ constraint. For instance, Z3 has good support for this kind of constraint.

My impression is that approximation algorithms for SAT-like problems tend to perform very poorly.