[Rule] SATISFIABILITY to NON-TAUTOLOGY

[isPANN]

Source: SATISFIABILITY
Target: NON-TAUTOLOGY

Motivation: Establishes NP-completeness of Non-Tautology via a trivial De Morgan duality reduction from SAT. Non-Tautology introduces DNF as a formula representation in the codebase, complementing the existing CNF-based models. The reduction is essentially a syntactic transformation with zero overhead.

Reference: Garey & Johnson, Computers and Intractability, Appendix A9.2, p.261

GJ Source Entry

[LO8] NON-TAUTOLOGY
INSTANCE: Boolean expression E over a set U of variables, using the connectives "¬" (not), "V" (or), "∧" (and), and "→" (implies).
QUESTION: Is E not a tautology, i.e., is there a truth assignment for U that makes E false?
Reference: [Cook, 1971a]. Transformation from SATISFIABILITY.
Comment: Remains NP-complete even if E is in "disjunctive normal form" with at most 3 literals per disjunct.

Reduction Algorithm

Reference: [Cook, 1971a]. Transformation from SATISFIABILITY.

Summary:
Given a SAT instance — a CNF formula φ = C₁ ∧ C₂ ∧ ... ∧ Cₘ over variables U = {x₁,...,xₙ} — construct a Non-Tautology instance as follows:

1. Negate the formula using De Morgan's laws:

   • ¬φ = ¬C₁ ∨ ¬C₂ ∨ ... ∨ ¬Cₘ
   • Each ¬Cⱼ: negate a clause (l₁ ∨ l₂ ∨ ... ∨ lₖ) → (¬l₁ ∧ ¬l₂ ∧ ... ∧ ¬lₖ)
   • Result: a DNF formula E = D₁ ∨ D₂ ∨ ... ∨ Dₘ

2. Each disjunct Dⱼ is a conjunction of negated literals from the original clause Cⱼ. If Cⱼ = (l₁ ∨ l₂ ∨ l₃), then Dⱼ = (¬l₁ ∧ ¬l₂ ∧ ¬l₃).

3. The Non-Tautology question asks: is E = ¬φ not a tautology? I.e., is there an assignment making E false?

Correctness:

• E is false ⟺ ¬φ is false ⟺ φ is true
• So E is not a tautology ⟺ there exists a falsifying assignment for E ⟺ there exists a satisfying assignment for φ
• Therefore: φ is satisfiable ⟺ ¬φ is not a tautology ✓

Solution extraction: The falsifying assignment for E is exactly the satisfying assignment for φ (same variable values, no transformation needed).

Note on the DNF restriction: G&J notes that Non-Tautology remains NP-complete even when E is in DNF with at most 3 literals per disjunct. The reduction above naturally produces a DNF where each disjunct has the same number of literals as the corresponding clause in the original CNF.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	n (same variables, no auxiliaries)
num_disjuncts	m (one disjunct per original clause)
max_literals_per_disjunct	max clause size in original CNF

This is an isometric reduction — the target instance is exactly the same size as the source.

Validation Method

• Closed-loop test: reduce a SAT instance, solve Non-Tautology with BruteForce, verify the falsifying assignment satisfies the original CNF
• Test with both satisfiable (non-tautology ¬φ) and unsatisfiable (tautology ¬φ) CNF instances
• Verify syntactic correctness: each disjunct in the DNF is the bitwise complement of the corresponding clause

Example

Source instance (SAT, CNF):
Variables: x₁, x₂, x₃, x₄
Clauses:

• C₁ = (x₁ ∨ ¬x₂ ∨ x₃)
• C₂ = (¬x₁ ∨ x₂ ∨ x₄)
• C₃ = (x₂ ∨ ¬x₃ ∨ ¬x₄)
• C₄ = (¬x₁ ∨ ¬x₂ ∨ x₃)

φ = C₁ ∧ C₂ ∧ C₃ ∧ C₄

Satisfying assignment: x₁=T, x₂=F, x₃=T, x₄=F.

Constructed target instance (Non-Tautology, DNF):

E = ¬φ = ¬C₁ ∨ ¬C₂ ∨ ¬C₃ ∨ ¬C₄

• D₁ = ¬C₁ = (¬x₁ ∧ x₂ ∧ ¬x₃)
• D₂ = ¬C₂ = (x₁ ∧ ¬x₂ ∧ ¬x₄)
• D₃ = ¬C₃ = (¬x₂ ∧ x₃ ∧ x₄)
• D₄ = ¬C₄ = (x₁ ∧ x₂ ∧ ¬x₃)

E = (¬x₁ ∧ x₂ ∧ ¬x₃) ∨ (x₁ ∧ ¬x₂ ∧ ¬x₄) ∨ (¬x₂ ∧ x₃ ∧ x₄) ∨ (x₁ ∧ x₂ ∧ ¬x₃)

Verification with x₁=T, x₂=F, x₃=T, x₄=F:

• D₁: F ∧ F ∧ F = F
• D₂: T ∧ T ∧ T = T ← this disjunct is true
• D₃: T ∧ T ∧ F = F
• D₄: T ∧ F ∧ F = F
• E = F ∨ T ∨ F ∨ F = T

So E is true under this assignment → this is NOT a falsifying assignment for E.

Falsifying assignment (making E false = making all Dⱼ false):
x₁=T, x₂=F, x₃=T, x₄=F makes D₂ true, so not falsifying.

Actually, φ is satisfiable, so ¬φ is NOT a tautology. A falsifying assignment for E must make φ true. Let's verify: x₁=F, x₂=F, x₃=T, x₄=T:

• C₁: F∨T∨T = T ✓, C₂: T∨F∨T = T ✓, C₃: F∨F∨F = F ✗ → φ is false, so E is true here.

Try x₁=T, x₂=T, x₃=T, x₄=F:

• C₁: T∨F∨T = T ✓, C₂: F∨T∨F = T ✓, C₃: T∨F∨T = T ✓, C₄: F∨F∨T = T ✓ → φ = true
• D₁: F∧T∧F = F, D₂: T∧F∧T = F, D₃: F∧T∧F = F, D₄: T∧T∧F = F → E = F ✓

Falsifying assignment found: x₁=T, x₂=T, x₃=T, x₄=F makes E false (= makes φ true).

Solution mapping: The falsifying assignment for E is directly the satisfying assignment for φ. No transformation needed.

References

• [Cook, 1971a]: [Cook1971a] S. A. Cook (1971). "The complexity of theorem-proving procedures". In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151–158. Association for Computing Machinery.

[zazabap]

verify-reduction report

Ran /verify-reduction SAT NonTautology against this issue's algorithm (PR #975).

Result: Reduction VERIFIED, example has a bug.

• Python: 6,954 checks, 0 failures
• De Morgan identity verified exhaustively for all CNF formulas on n ≤ 4 variables
• Forward + backward + solution extraction all pass

Bug in worked example: The claimed satisfying assignment x₁=T, x₂=F, x₃=T, x₄=F does not satisfy the formula. Clause C₂ = (¬x₁ ∨ x₂ ∨ x₄) evaluates to (F ∨ F ∨ F) = False.

A correct satisfying assignment exists (the formula is satisfiable), but the specific one listed in the issue is wrong. This should be fixed before implementation.

Script: docs/paper/verify-reductions/verify_sat_nontautology.py