Is there any variant of the Boolean SAT or Max-SAT problem that has a flavor of maximizing or minimizing the average of the weights of the satisfied clauses of a WCNF formula? Any literature on an optimization problem of similar flavor would be appreciated. Thanks.
1
-
$\begingroup$ What type of results or research into this would you like to find? $\endgroup$– JuhoCommented Aug 8, 2020 at 19:49
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
This problem is new to me. It has similar hardness to weighted MaxSAT; there is a polynomial-time Turing reduction in both directions. Here is a key fact:
Let $\varphi,(w_1,\dots,w_n)$ denote a weighted CNF formula, where $w_1,\dots,w_n$ are the weights on the clauses. Then the following two conditions are equivalent:
- There is an assignment to $\varphi,(w_1,\dots,w_n)$ so that the average of the weights of the satisfied clauses is at least $a$.
- There is an assignment to $\varphi,(w_1-a,\dots,w_n-a)$ so that the sum of the weights of the satisfied clauses is at least $0$.
This lemma yields an equivalence between weighted MaxSAT and weighted MaxAverageSAT.
For instance, if you have an instance of weighted MaxAverageSAT that you want to solve, here is how you can solve it using an off-the-shelf solver for weighted MaxSAT. Basically, use binary search on the average $a$. Given $a$, you can test whether it is possible to achieve an average at least $a$, by using the solver on $\varphi,(w_1-a,\dots,w_n-a)$ and checking whether it gives you an assignment where the sum of the weights is at least $0$; you can then use this to determine whether to increase $a$ or decrease $a$ in the binary search. After polynomially many iterations of binary search, you'll narrow it down to a small enough range that you can uniquely determine the maximum achievable average.
