Maximum Exact-4-SAT Optimisation Problem

Definition

Maximum Exact-4-SAT Optimisation Problem

Instance: A CNF formula $F=C_1\wedge \cdots \wedge C_m$, where each clause consists of exactly four literals on four distinct variables.

Feasible solutions: All truth assignments $\sigma :\mathrm{Var}(F)\to \{\top ,\perp \}$.

Objective: Maximise the number of satisfied clauses:
$\mathrm{OPT}={\max }_{\sigma }{\sum }_{j=1}^{m}1[\sigma \models C_j].$
Here $1[P]$ is $1$ when $P$ holds and $0$ otherwise. “Exact-4” specifies clause length, not a requirement that exactly one literal be true. Clauses may share variables with other clauses.