A rendezvous of logic, complexity, and algebra

Abstract

An emerging area of research studies the complexity of constraint satisfaction problems under restricted constraint languages. This article gives a self-contained, contemporary presentation of Schaefer's theorem on Boolean constraint satisfaction, the inaugural result of this area, as well as analogs of this theorem for quantified formulas. Our exposition makes use of and may serve as an introduction to logical and algebraic tools that have recently come into focus. 1. POP QUIZ Recall the propositional satisfiability (SAT) problem: we are given a propositional formula such as (s ∨ t) ∧ (¬s) ∧ (¬u ∨ s ∨ ¬t) ∧ (¬s ∨ t) consisting of a conjunction of clauses, where a clause is a disjunction of literals; a literal is either a variable v (a positive literal) or the negation of a variable ¬v (a negative literal). We are to decide if there is an assignment to the variables satisfying the formula, that is, an assignment under which every clause contains at least one true literal. The example formula is satisfied by the assignment f where f (s) = f (u) = false and f (t) = true. The SAT problem is famously regarded as the first natural problem to be identified as NP-complete. Two special cases of the SAT problem that are well known to be decidable in polynomial time are the 2-SAT problem, in which every clause is a 2-clause, a clause having