1
$\begingroup$

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.

$\endgroup$
1
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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