Unique satisfiability

A formula in conjunctive normal form is uniquely satisfiable when it has exactly one satisfying assignment of its variables. Formulas here have variables numbered by ℕ, and an assignment ℕ → Bool also gives values to the infinitely many variables that do not occur; so USAT asks for a satisfying assignment with which every satisfying assignment agrees on the variables of the formula (Cslib.Logic.PL.CNF.vars).

Valiant and Vazirani consider the promise problem PromiseUSAT whose yes-instances are the uniquely satisfiable formulas and whose no-instances are the unsatisfiable ones Valiant and Vazirani, Arora and Barak, Section 17.4. Formulas with two or more satisfying assignments are outside the promise, so a function solves PromiseUSAT when the set it accepts lies between USAT and SAT (solvedBy_PromiseUSAT_iff); deciding either USAT or SAT does (solvedBy_USAT, solvedBy_SAT). PromiseUSAT lies in PromiseNP, separated by SAT (PromiseUSAT_mem_PromiseNP).

Main definitions

• Cslib.Complexity.USAT: the uniquely satisfiable formulas.
• Cslib.Complexity.PromiseUSAT: unique satisfiability as a promise problem.

Main results

• Cslib.Complexity.USAT_subset_SAT: a uniquely satisfiable formula is satisfiable.
• Cslib.Complexity.solvedBy_PromiseUSAT_iff: the solutions of PromiseUSAT.
• Cslib.Complexity.solvedBy_USAT, Cslib.Complexity.solvedBy_SAT: deciding USAT, or SAT, solves PromiseUSAT.
• Cslib.Complexity.PromiseUSAT_mem_PromiseNP: PromiseUSAT lies in PromiseNP.

References

• A. Blass, Y. Gurevich, On the unique satisfiability problem
• L. G. Valiant, V. V. Vazirani, NP is as easy as detecting unique solutions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.Complexity.USAT : Set (Logic.PL.CNF ℕ)

The uniquely satisfiable formulas: some assignment satisfies the formula, and every satisfying assignment agrees with it on every variable of the formula Blass and Gurevich.

theorem Cslib.Complexity.mem_USAT {φ : Logic.PL.CNF ℕ} : φ ∈ USAT ↔ ∃ (σ : ℕ → Bool), Logic.PL.CNF.eval σ φ = true ∧ ∀ (τ : ℕ → Bool), Logic.PL.CNF.eval τ φ = true → ∀ v ∈ φ.vars, τ v = σ v

theorem Cslib.Complexity.USAT_subset_SAT : USAT ⊆ SAT

A uniquely satisfiable formula is satisfiable.

theorem Cslib.Complexity.disjoint_USAT_UNSAT : Disjoint USAT UNSAT

No uniquely satisfiable formula is unsatisfiable.

def Cslib.Complexity.PromiseUSAT : PromiseProblem (Logic.PL.CNF ℕ)

Unique satisfiability as a promise problem: the yes-instances are the uniquely satisfiable formulas, the no-instances the unsatisfiable ones, and formulas with at least two satisfying assignments are outside the promise.

@[simp]

theorem Cslib.Complexity.yes_PromiseUSAT : PromiseUSAT.yes = USAT

@[simp]

theorem Cslib.Complexity.no_PromiseUSAT : PromiseUSAT.no = UNSAT

theorem Cslib.Complexity.solvedBy_PromiseUSAT_iff {f : Logic.PL.CNF ℕ → Bool} : PromiseUSAT.SolvedBy f ↔ USAT ⊆ {φ : Logic.PL.CNF ℕ | f φ = true} ∧ {φ : Logic.PL.CNF ℕ | f φ = true} ⊆ SAT

A function solves PromiseUSAT exactly when the set it accepts lies between USAT and SAT.

theorem Cslib.Complexity.solvedBy_USAT : PromiseUSAT.SolvedBy fun (φ : Logic.PL.CNF ℕ) => decide (φ ∈ USAT)

Deciding USAT solves PromiseUSAT.

theorem Cslib.Complexity.solvedBy_SAT : PromiseUSAT.SolvedBy fun (φ : Logic.PL.CNF ℕ) => decide (φ ∈ SAT)

Deciding SAT also solves PromiseUSAT: its answers on formulas outside the promise are irrelevant.

theorem Cslib.Complexity.PromiseUSAT_mem_PromiseNP : PromiseUSAT ∈ PromiseNP encCNF

PromiseUSAT lies in PromiseNP, separated by SAT ∈ NP.