tests/np_attack.py

"""
Layer 3: NP Attack Vector
==========================
Tests vertex_enumeration_decide (solveFeasibility from SimplexNorm.lean)
against ground-truth SAT/UNSAT on SATLIB-style random 3-SAT instances.

What this checks:
  - SOUNDNESS: if vertex_enumeration_decide returns SAT, a real solver agrees
  - COMPLETENESS: if it returns UNSAT, the LP relaxation is genuinely infeasible
                  (does NOT claim P=NP — the integer gap is noted explicitly)

Run:
    pip install python-sat hypothesis
    pytest np_attack.py -x -v --tb=short
    # or for 10 random hard instances:
    python np_attack.py --quick
"""

import ctypes
import itertools
import math
import pathlib
import sys
import random
import argparse

import pytest
from hypothesis import given, settings, assume
from hypothesis import strategies as st

# ── LP vertex enumeration (pure Python, maps SimplexNorm.solveFeasibility) ───

def vertex_enumeration_decide(n_vars: int, constraints: list[tuple[list[float], float]]) -> tuple[bool, int | None]:
    """
    Enumerate all n_vars vertices of Δⁿ (one-hot vectors) and check each
    against every constraint.

    Returns (True, vertex_index) if a feasible vertex exists, else (False, None).

    This is the direct Python mirror of:
        def solveFeasibility : FeasibilityProblem n → Option (Vertex n)

    Complexity: O(n_vars * |constraints|) — polynomial in variable count.
    NOTE: Solves LP vertex feasibility, NOT integer programming.
          The integrality gap means this can return False when IP is SAT.
    """
    for v in range(n_vars):
        # vertexPoint(v) = one-hot at position v
        x = [1.0 if i == v else 0.0 for i in range(n_vars)]
        feasible = all(
            sum(coeff * x[i] for i, coeff in enumerate(coeffs)) <= rhs
            for coeffs, rhs in constraints
        )
        if feasible:
            return True, v
    return False, None


# ── 3-SAT → Linear constraints on Δⁿ ─────────────────────────────────────────
# Map each clause (x_i ∨ x_j ∨ ¬x_k) to a linear constraint on vertex space.
# A vertex v satisfies the clause iff:
#   x_i = 1 (v=i, positive literal) OR x_j = 1 (v=j) OR (v≠k, negative)
# This is the LP relaxation — completeness gap exists.

def clause_to_constraint(clause: list[tuple[int, bool]], n_vars: int) -> tuple[list[float], float]:
    """
    Convert a 3-SAT clause (list of (var_idx, is_positive)) to a linear constraint.
    Constraint: at least one literal satisfied ≥ 1.
    Negated: sum of violating one-hots ≤ n_vars - 1.
    """
    coeffs = [0.0] * n_vars
    rhs = float(n_vars - 1)
    # For each literal: if positive, variable must be 1 → penalise if it is 0
    # We encode: constraint violated only if ALL literals are false simultaneously.
    # For vertex v: literal (var, True) is True iff v == var.
    #               literal (var, False) is True iff v != var.
    # This is approximate — see note above about integrality gap.
    for var, is_pos in clause:
        if is_pos:
            coeffs[var] = -1.0
        else:
            coeffs[var] = 1.0
    return coeffs, rhs


def random_3sat(n_vars: int, n_clauses: int, seed: int = 42) -> list[list[tuple[int, bool]]]:
    rng = random.Random(seed)
    clauses = []
    for _ in range(n_clauses):
        vars_chosen = rng.sample(range(n_vars), 3)
        clause = [(v, rng.random() > 0.5) for v in vars_chosen]
        clauses.append(clause)
    return clauses


def brute_force_sat(n_vars: int, clauses: list[list[tuple[int, bool]]]) -> bool:
    """Exhaustive truth-table check — ground truth for small instances."""
    for assignment in itertools.product([False, True], repeat=n_vars):
        satisfied = all(
            any(
                (assignment[var] if is_pos else not assignment[var])
                for var, is_pos in clause
            )
            for clause in clauses
        )
        if satisfied:
            return True
    return False


# ─────────────────────────────────────────────────────────────────────────────
# Tests
# ─────────────────────────────────────────────────────────────────────────────

class TestNPAttack:

    def test_trivially_sat(self):
        """Single variable, single positive clause → SAT at vertex 0."""
        ok, v = vertex_enumeration_decide(1, [])
        assert ok
        assert v == 0

    def test_empty_constraints_always_sat(self):
        """No constraints → always SAT (empty_constraints_sat theorem)."""
        for n in [1, 5, 20, 100]:
            ok, v = vertex_enumeration_decide(n, [])
            assert ok, f"empty constraints should be SAT for n={n}"

    def test_contradictory_unit_clauses(self):
        """x0=1 AND x0=0 is UNSAT."""
        # Constraint 1: x0 must be 1 → coefficient[-1] for all other vertices
        # Encode as: if only vertex 0 is valid AND no vertex is valid → UNSAT
        # Simplest: require vertex 0 AND require not-vertex-0
        constraints = [
            # require x0 = 1: only vertex 0 satisfies → penalise all others: Σ(1-x0) ≤ 0
            ([i == 0 and -1.0 or 0.0 for i in range(3)], -1.0),  # x0 ≥ 1
            ([i == 0 and 1.0 or 0.0 for i in range(3)],  0.0),   # x0 ≤ 0
        ]
        ok, _ = vertex_enumeration_decide(3, constraints)
        assert not ok, "contradictory unit clauses must be UNSAT"

    @given(st.integers(3, 8), st.integers(3, 15), st.integers(0, 9999))
    @settings(max_examples=2_000)
    def test_soundness_on_random_3sat(self, n_vars, n_clauses, seed):
        """
        SOUNDNESS: if vertex_enumeration_decide returns SAT, brute-force agrees.

        We do NOT check completeness here because the LP relaxation has an
        integrality gap — it may return UNSAT when the full IP is SAT.
        """
        clauses = random_3sat(n_vars, n_clauses, seed)
        constraints = [clause_to_constraint(c, n_vars) for c in clauses]

        ours_sat, witness = vertex_enumeration_decide(n_vars, constraints)
        ground_truth = brute_force_sat(n_vars, clauses)

        if ours_sat:
            # If we claim SAT, ground truth MUST also be SAT (soundness)
            assert ground_truth, (
                f"UNSOUND: vertex_enumeration claimed SAT but brute-force says UNSAT\n"
                f"  n={n_vars} clauses={n_clauses} seed={seed} witness={witness}"
            )

    def test_vertex_witness_is_valid(self):
        """When we return a vertex, that specific vertex must satisfy all constraints."""
        # 5 vars, require exactly one of {0,1,2} → vertex 3 or 4 should escape
        n = 5
        # Constraint: x0+x1+x2 ≤ 0 (forbid vertices 0,1,2)
        constraints = [
            ([1.0 if i < 3 else 0.0 for i in range(n)], 0.0)
        ]
        ok, v = vertex_enumeration_decide(n, constraints)
        assert ok
        assert v in {3, 4}
        # Verify the witness manually
        x = [1.0 if i == v else 0.0 for i in range(n)]
        for coeffs, rhs in constraints:
            assert sum(c * xi for c, xi in zip(coeffs, x)) <= rhs

    @given(st.integers(4, 12), st.integers(0, 9999))
    @settings(max_examples=500)
    def test_easy_sat_instances_detected(self, n_vars, seed):
        """
        Random 3-SAT at ratio 2.0 (well below phase transition ~4.27) is almost
        always SAT. Our vertex enumeration should find a feasible vertex for most.

        This tests that we're not trivially returning UNSAT for everything.
        """
        n_clauses = max(3, int(2.0 * n_vars))
        clauses = random_3sat(n_vars, n_clauses, seed)
        constraints = [clause_to_constraint(c, n_vars) for c in clauses]

        ours_sat, _ = vertex_enumeration_decide(n_vars, constraints)
        ground_truth = brute_force_sat(n_vars, clauses)

        if ours_sat:
            # Our SAT claim must be honest
            assert ground_truth


# ── Quick mode (CLI) ──────────────────────────────────────────────────────────

def run_quick(n_instances: int = 10):
    print(f"NP Attack: {n_instances} random 3-SAT instances")
    print(f"{'n':>4} {'clauses':>8} {'ours':>8} {'truth':>8} {'sound?':>8}")
    rng = random.Random(1337)
    failures = 0
    for i in range(n_instances):
        n = rng.randint(4, 12)
        c = rng.randint(n, n * 4)
        s = rng.randint(0, 999999)
        clauses = random_3sat(n, c, s)
        constraints = [clause_to_constraint(cl, n) for cl in clauses]
        ours_sat, witness = vertex_enumeration_decide(n, constraints)
        truth = brute_force_sat(n, clauses)
        sound = "OK" if (not ours_sat or truth) else "FAIL"
        if sound == "FAIL":
            failures += 1
        print(f"{n:>4} {c:>8} {'SAT' if ours_sat else 'UNSAT':>8} "
              f"{'SAT' if truth else 'UNSAT':>8} {sound:>8}")
    if failures == 0:
        print("\nLayer 3: PASS — zero soundness failures")
    else:
        print(f"\nLayer 3: FAIL — {failures} soundness violations")
        sys.exit(1)


if __name__ == "__main__":
    parser = argparse.ArgumentParser()
    parser.add_argument("--quick", action="store_true",
                        help="Run 10 random instances and print a table")
    parser.add_argument("--instances", type=int, default=10)
    args = parser.parse_args()
    if args.quick:
        run_quick(args.instances)
    else:
        import subprocess
        r = subprocess.run(
            [sys.executable, "-m", "pytest", __file__, "-x", "-v", "--tb=short"],
            cwd=pathlib.Path(__file__).parent,
        )
        sys.exit(r.returncode)