Maximum Exact-4-SAT Optimisation Problem

Definition

Maximum Exact-4-SAT Optimisation Problem

Instance: A CNF formula , where each clause consists of exactly four literals on four distinct variables.

Feasible solutions: All truth assignments .

Objective: Maximise the number of satisfied clauses:

Here is when holds and otherwise. “Exact-4” specifies clause length, not a requirement that exactly one literal be true. Clauses may share variables with other clauses.