[Model] NonTautology

[isPANN]

Motivation

NON-TAUTOLOGY (P260) from Garey & Johnson, A9 LO8. The dual of SAT under De Morgan's laws — asks whether a Boolean expression has a falsifying assignment. Introduces DNF as a formula representation. While interreducible with SAT via complementation, the distinct input format (DNF disjuncts vs CNF clauses) and evaluation semantics make it a separate model.

Associated rules:

• [Rule] SATISFIABILITY to NON-TAUTOLOGY #868: SATISFIABILITY → NonTautology (classical NP-completeness proof from G&J)

Definition

Name: NonTautology
Reference: Garey & Johnson, Computers and Intractability, A9 LO8

**Canonical name:** Non-Tautology, also called DNF Falsifiability or co-SAT (when viewed as the complement of tautology checking).

Mathematical definition:

INSTANCE: Boolean expression E over a set U of variables, using the connectives "¬" (not), "∨" (or), "∧" (and), and "→" (implies).
QUESTION: Is E not a tautology, i.e., is there a truth assignment for U that makes E false?

NP-complete restriction: Remains NP-complete when E is in disjunctive normal form (DNF) with at most 3 literals per disjunct.

Variables

• Count: n = |U| (one variable per Boolean variable)
• Per-variable domain: binary {0, 1} (false/true)
• Meaning: x_i = 1 if variable u_i is assigned true. The question asks whether there exists an assignment making E evaluate to false.

Schema (data type)

Type name: NonTautology
Variants: none

Field	Type	Description
num_vars	usize	Number of Boolean variables
disjuncts	Vec<Vec<i32>>	DNF disjuncts; each disjunct is a conjunction of literals (signed integers: positive = variable, negative = negated variable)

Notes:

• This is a feasibility (decision) problem: Value = Or (does a falsifying assignment exist?).
• Evaluation: E is false iff ALL disjuncts are false, i.e., for each disjunct, at least one literal in its conjunction is false.
• Key getter methods: num_vars(), num_disjuncts() (= disjuncts.len()).
• Duality with SAT: A DNF Non-Tautology instance with disjuncts D_1,...,D_m is exactly the negation of a CNF SAT instance with clauses C_1,...,C_m where each clause C_j has the complemented literals of D_j.

Complexity

• Decision complexity: NP-complete (Cook, 1971; transformation from Satisfiability). Remains NP-complete when E is in DNF with at most 3 literals per disjunct.
• Best known exact algorithm: Same as SAT, since Non-Tautology and SAT are interreducible with zero overhead. For DNF with 3 literals per disjunct (equivalent to 3-SAT): O*(1.307^n) by Biased-PPSZ (Scheder & Steinberger, 2017).
• Concrete complexity expression: "1.307^num_vars" (for declare_variants!)
• Special cases:
  • DNF with ≤ 2 literals per disjunct: polynomial (equivalent to 2-SAT)
  • CNF Non-Tautology: trivially decidable (check if any clause is a tautology)
• References:
  • S.A. Cook (1971). "The Complexity of Theorem-Proving Procedures." STOC 1971, pp. 151-158.
  • D. Scheder, J.P. Steinberger (2017). "PPSZ for General k-SAT — Making Hertli's Analysis Simpler and 3-SAT Faster." CCC 2017.

Extra Remark

Full book text:

INSTANCE: Boolean expression E over a set U of variables, using the connectives "¬" (not), "∨" (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.

How to solve

• It can be solved by (existing) bruteforce. (Enumerate all 2^n assignments; check if any makes E false.)
• It can be solved by reducing to integer programming. (Negate to get CNF, encode as ILP; or directly encode "all disjuncts false" as ILP constraints. Companion rule issue to be filed separately.)
• Other: Reduce to SAT via De Morgan negation, use any SAT solver.

Example Instance

Input:
n = 5 variables: x_1, x_2, x_3, x_4, x_5
DNF expression:
E = (x_1 ∧ x_2 ∧ x_3) ∨ (¬x_1 ∧ x_4) ∨ (¬x_2 ∧ ¬x_3 ∧ x_5) ∨ (x_3 ∧ ¬x_4 ∧ ¬x_5) ∨ (¬x_1 ∧ x_2 ∧ ¬x_5)

Represented as:

disjuncts = [[1, 2, 3], [-1, 4], [-2, -3, 5], [3, -4, -5], [-1, 2, -5]]

Falsifying assignment: (x_1, x_2, x_3, x_4, x_5) = (T, F, F, T, F):

• D_1: T∧F∧F = F ✓
• D_2: F∧T = F ✓
• D_3: T∧T∧F = F ✓
• D_4: F∧F∧T = F ✓
• D_5: F∧F∧T = F ✓
• E = F ∨ F ∨ F ∨ F ∨ F = FALSE ✓

Answer: YES — E is not a tautology. There are 13 falsifying assignments out of 32 total.

Non-satisfying assignment (E is true): (x_1, x_2, x_3, x_4, x_5) = (F, F, F, T, F):

• D_2: ¬x_1 ∧ x_4 = T∧T = TRUE → E = TRUE.
  This assignment makes E true, so it is not a witness for non-tautology.

Python validation script

falsifying = []
for bits in range(32):
    x = [(bits >> i) & 1 for i in range(5)]
    d1 = x[0] and x[1] and x[2]
    d2 = (1-x[0]) and x[3]
    d3 = (1-x[1]) and (1-x[2]) and x[4]
    d4 = x[2] and (1-x[3]) and (1-x[4])
    d5 = (1-x[0]) and x[1] and (1-x[4])
    E = d1 or d2 or d3 or d4 or d5
    if not E:
        falsifying.append(tuple(x))

assert len(falsifying) == 13
assert (1, 0, 0, 1, 0) in falsifying  # proposed solution
assert (0, 0, 0, 1, 0) not in falsifying  # E is true here
print(f"Falsifying: {len(falsifying)}/32 (non-tautology confirmed)")

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but ILP claim lacks companion rule issue
Non-trivial	✅ Pass	Structurally dual to SAT with distinct input format (DNF vs CNF)
Correctness	❌ Fail	Complexity bound 1.3289^n is incorrect; correct bound is 1.308^n (Hertli 2011)
Well-written	❌ Fail	Missing Expected Outcome section header; no linked [Rule] NonTautology to ILP issue

Overall: 1 passed, 1 warning, 2 failed

---

Usefulness

Problem existence: NonTautology does not exist in the codebase — novel problem. ✅

Reduction connectivity: The issue mentions R204 (SATISFIABILITY → NonTautology), which connects it to the existing graph. ✅

Motivation: The motivation is substantive — references Garey & Johnson A9 LO8, explains the duality with SAT under De Morgan's laws, and introduces DNF as a formula representation. ✅

Solver path: The issue checks both brute-force and ILP boxes. However, direct ILP solvability is claimed without linking a companion [Rule] NonTautology to ILP issue as required by the template. ⚠️ Warn — add a companion rule issue or remove the ILP claim.

Non-trivial

NonTautology on DNF is the structural dual of Satisfiability on CNF. While they are interreducible with zero overhead via De Morgan's laws, they have genuinely different:

• Input formats: DNF (disjuncts = conjunctions of literals) vs CNF (clauses = disjunctions of literals)
• Evaluation semantics: "all disjuncts false" vs "all clauses true"
• Schema fields: disjuncts vs clauses

This is a legitimate distinct problem listed separately in Garey & Johnson (A9 LO8). ✅ Pass.

Correctness

Definition correctness: The formal definition is mathematically well-formed. The INSTANCE/QUESTION format from G&J is correctly reproduced. ✅

Complexity verification: ❌ Fail. The issue claims:

O(1.3289^n) by PPSZ algorithm (Paturi, Pudlak, Saks, Zane, 2005)

This is incorrect on multiple counts:

1. The number 1.3289 does not appear in the PPSZ (2005) paper. The original PPSZ bound for unique 3-SAT was O(1.3071^n).
2. The best known bound for general 3-SAT is O(1.308^n), achieved by Hertli (2011) via an improved analysis of PPSZ. See: Hertli, "3-SAT Faster and Simpler — Unique-SAT Bounds for PPSZ Hold in General," FOCS 2011 (arXiv:1103.2165).
3. Hansen et al. (2019) further improved to O(1.307^n) via Biased-PPSZ (already in project bibliography as hansen2019).

Recommendation: Update the complexity to O(1.307^num_vars) citing Hansen et al. (2019), which is already in the project bibliography.

Reference verification: The Cook (1971) reference for the original NP-completeness proof is standard and correct. The PPSZ (2005) paper exists (JACM 52(3), pp. 337–364) but the bound cited from it is wrong. ⚠️

Example verification: ✅ The claimed falsifying assignment x1=T, x2=F, x3=F, x4=T, x5=F was independently verified to make E evaluate to false. The instance has 13 falsifying assignments out of 32 total, confirming it is not a tautology and is non-trivial.

Well-written

Information completeness:

• Motivation: ✅ Present and substantive
• Name: ✅ NonTautology — correct naming (no optimization prefix needed for a feasibility problem)
• Reference: ✅ G&J A9 LO8
• Definition: ✅ Well-formed INSTANCE/QUESTION
• Variables: ✅ Count, domain, meaning all specified
• Schema: ✅ Type name, field table present
• Complexity: ✅ Present (but incorrect value — see Correctness above)
• How to solve: ⚠️ ILP checked but no companion rule issue linked
• Example Instance: ✅ Present with 5 variables
• Expected Outcome: ❌ Fail — no dedicated "Expected Outcome" section. The falsifying assignment is shown inline in the example, but the template requires an explicit expected outcome stating the solution and brief justification as a separate section.

Definition completeness: The definition uses the G&J format with explicit INSTANCE and QUESTION. The NP-complete restriction (DNF with at most 3 literals per disjunct) is noted. ✅

Symbol consistency: Symbols are consistent across sections — U for variable set, E for expression, n = |U|, xᵢ for variables. ✅

Example quality:

• Non-trivial: ✅ 5 variables, 5 disjuncts, 13 falsifying out of 32 — good complexity
• Exercises core structure: ✅ Multiple disjuncts with mixed positive/negative literals
• Round-trip testable: ✅ Multiple feasible (falsifying) and infeasible (satisfying) assignments
• Expected outcome: ❌ Not explicitly stated as a separate section

ILP companion issue: ❌ The "How to solve" section checks the ILP box but does not link a [Rule] NonTautology to ILP companion issue as required.

Recommendations

• Update complexity bound from 1.3289^n to 1.307^num_vars citing Hansen et al. (2019) (hansen2019 in project bibliography)
• Add an explicit Expected Outcome section: "The expression is not a tautology. A falsifying assignment is x1=T, x2=F, x3=F, x4=T, x5=F, which makes all 5 disjuncts evaluate to false."
• Either create and link a [Rule] NonTautology to ILP companion issue, or uncheck the ILP box in "How to solve"

[isPANN]

Fix-issue changelog

• Complexity: Fixed incorrect bound 1.3289^n (not from PPSZ) → 1.307^n (Scheder & Steinberger 2017). Added concrete expression "1.307^num_vars" for declare_variants!.
• Associated rules: Linked rule [Rule] SATISFIABILITY to NON-TAUTOLOGY #868 (SATISFIABILITY → NonTautology).
• ILP: Added companion rule note.
• Schema notes: Added getter methods (num_vars(), num_disjuncts()).
• Example: Added non-satisfying assignment example (E=TRUE) to complement the falsifying assignment. Added count: 13/32 falsifying.
• Added Python validation script verifying falsifying count and proposed assignments.

Applied by /fix-issue.