Maximum 2-SAT Optimisation Problem

Definition

Maximum 2-SAT Optimisation Problem

Instance: A CNF formula $F=C_1\wedge \cdots \wedge C_m$, where every clause contains at most two 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 two; unit clauses are allowed.

Satisfiability versus Maximisation

Testing whether all clauses of a 2-CNF formula can be satisfied is polynomial-time solvable. Finding the largest number that can be satisfied is NP-hard. The tractability of 2-SAT therefore does not imply the tractability of Max2SAT.

The linear reduction from MaxE3SAT transfers both exact hardness and an approximation lower bound to Max2SAT.

Example

A feasible assignment need not satisfy the formula

For $F=(x)\wedge (\neg x)\wedge (x\vee y)$, no assignment satisfies every clause. Setting $x=1$ satisfies the first and third clauses, so $\mathrm{OPT}(F)=2$.