# Is MAX-averageSAT a well-known problem?

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.

• What type of results or research into this would you like to find?
– Juho
Commented Aug 8, 2020 at 19:49

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