Maximum 3-SAT Optimisation Problem

Definition

Maximum 3-SAT Optimisation Problem

Instance: A CNF formula $F=C_1\wedge \cdots \wedge C_m$, where every clause contains at most three literals.

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

Objective: Maximise the number of satisfied clauses:

$${\mathrm{val}}_F(\sigma )=\sum _{j=1}^{m}1[\sigma \models C_j],\mathrm{OPT}(F)=\underset{\sigma }{\max }{\mathrm{val}}_F(\sigma ).$$

Here $1[P]$ is $1$ if $P$ holds and $0$ otherwise. An assignment is optimal exactly when its value equals $\mathrm{OPT}(F)$. Each clause occurrence counts separately.

This is the restriction of MaxSAT to clauses of length at most three; unit and two-literal clauses are allowed.

At Most Three versus Exactly Three

MaxE3SAT requires exactly three literals on distinct variables in every clause. It is a special case of Max3SAT, not a different spelling of the same restriction.

Uniform independent random assignment satisfies a three-variable clause with probability $7/8$, but a unit clause only with probability $1/2$. Thus the $7/8$ random-assignment guarantee for MaxE3SAT does not apply directly to general Max3SAT.

Example

A mixed-length instance

The formula $F=(x)\wedge (\neg x\vee y)\wedge (x\vee \neg y\vee z)$ is a Max3SAT instance but not a MaxE3SAT instance. Setting $x=y=z=1$ satisfies all three clauses, so $\mathrm{OPT}(F)=3$.