FIND A SAT NP COMPLETE CNF INSTANCE THAT DESTROY MY SOLVER [closed]

Hello everyone again. This time I would like you to find any false positive or false negative in my SAT SOLVER. The challenge will be that the first person to find a CNF SAT instance where my solver fails will win. My solver is here: https://github.com/POlLLOGAMER/P-is-equal-to-NP-Code/blob/main/P%3DNP_HOLOGRAFIA_CODIGO_FUNCIONAL.ipynb and here as well.

# ==========================================================================
#  PCP HOLOGRÁFICO REAL (Walsh-Hadamard) + Search-to-Decision para SAT
#  1 celda Colab. Implementación fiel del verificador PCP de Hadamard
#  (Arora-Safra / ALMSS): tests BLR de linealidad, consistencia L/Q y
#  satisfacción, con O(1) consultas y O(n^2) bits aleatorios de query.
# ==========================================================================
!pip install galois -q

import math
import numpy as np
import galois

GF = galois.GF(2)

# --------------------------------------------------------------------------
# Fórmula (CNF, 1-indexed). Reducimos SAT a "existe x en GF(2)^n que satisface".
# --------------------------------------------------------------------------
class Formula:
    def __init__(self, num_vars, clauses):
        self.num_vars = num_vars
        self.clauses = clauses  # p.ej. [[1,-2],[-1,3]]

    def is_satisfied(self, assignment):
        """assignment: array GF(2) de longitud num_vars (1 = True)."""
        for clause in self.clauses:
            ok = False
            for lit in clause:
                v = int(assignment[abs(lit) - 1])
                val = v if lit > 0 else (1 - v)
                if val == 1:
                    ok = True
                    break
            if not ok:
                return False
        return True


# --------------------------------------------------------------------------
# PRUEBA HOLOGRÁFICA REAL = codificación Walsh-Hadamard de x y de x⊗x.
#
#  Para una asignación x ∈ GF(2)^n, la prueba PCP de Hadamard consiste en:
#    A = tabla de la función LINEAL   f(a)  =         (2^n entradas)
#    B = tabla de la función LINEAL   g(M)  =       (2^{n^2} entradas)
#  Estas son las "tablas Hadamard" (holográficas): cada bit de la prueba
#  es un producto interno sobre todo el espacio. El verificador solo consulta
#  un número CONSTANTE de posiciones.
#
#  Para que sea ejecutable con n pequeño representamos A y B implícitamente
#  como oráculos (funciones) sobre los vectores x y w=vec(x⊗x). Consultar
#  la prueba en el punto a  ==  evaluar . Esto ES la tabla Hadamard,
#  evaluada perezosamente (sin materializar 2^n entradas).
# --------------------------------------------------------------------------
class PCPProof:
    def __init__(self, x_vec, w_vec, n):
        self.n = n
        self.x = GF(np.array(x_vec, dtype=int) % 2)          # GF(2)^n
        self.w = GF(np.array(w_vec, dtype=int) % 2)          # GF(2)^{n^2}, = vec(x⊗x)

    # A(a) =   (oráculo lineal de grado 1)
    def A(self, a):
        a = GF(np.array(a, dtype=int) % 2)
        return int(np.sum(a * self.x))  # suma en GF(2)

    # B(M) =   (oráculo lineal de grado 2, aplanado)
    def B(self, M):
        M = GF(np.array(M, dtype=int) % 2)
        return int(np.sum(M * self.w))


class PCPSystem:
    @staticmethod
    def generate_proof(formula: Formula, assignment) -> PCPProof:
        """Prover: construye las tablas Hadamard A=<.,x> y B=<.,x⊗x>."""
        n = formula.num_vars
        x = GF(np.array([1 if b else 0 for b in assignment], dtype=int))
        # w = vec(x ⊗ x) ∈ GF(2)^{n^2}
        outer = np.outer(np.array(x, dtype=int), np.array(x, dtype=int)) % 2
        w = outer.flatten()
        return PCPProof(x, w, n)

    # ---- Los TRES tests reales del verificador PCP de Hadamard ----
    @staticmethod
    def _linearity_test(oracle, dim, reps=8):
        """Test BLR de linealidad: f(a)+f(b) == f(a+b) con a,b aleatorios."""
        for _ in range(reps):
            a = np.random.randint(0, 2, dim)
            b = np.random.randint(0, 2, dim)
            ab = (a + b) % 2
            if (oracle(a) ^ oracle(b)) != oracle(ab):
                return False
        return True

    @staticmethod
    def _consistency_test(proof: PCPProof, reps=8):
        """
        Consistencia A vs B: para r,s aleatorios en GF(2)^n debe cumplirse
          A(r)·A(s) == B(r s^T)
        (porque  = x^T (r s^T) x = ).
        """
        n = proof.n
        for _ in range(reps):
            r = np.random.randint(0, 2, n)
            s = np.random.randint(0, 2, n)
            M = np.outer(r, s).flatten() % 2
            lhs = proof.A(r) & proof.A(s)      # producto en GF(2)
            rhs = proof.B(M)
            if lhs != rhs:
                return False
        return True

    @staticmethod
    def _satisfaction_test(formula: Formula, proof: PCPProof):
        """
        Comprueba que la x codificada satisface la fórmula, leyendo cada
        variable como A(e_i) = x_i (consulta puntual a la tabla Hadamard).
        """
        n = formula.num_vars
        x_read = np.array([proof.A(np.eye(n, dtype=int)[i]) for i in range(n)])
        return formula.is_satisfied(GF(x_read))

    @staticmethod
    def verify(formula: Formula, proof: PCPProof) -> bool:
        """
        Verifier PCP: O(1) consultas por test. Acepta sii la prueba es
        lineal, consistente (A,B codifican el mismo x) y x satisface φ.
        """
        n = formula.num_vars
        if not PCPSystem._linearity_test(proof.A, n):            # A es lineal
            return False
        if not PCPSystem._linearity_test(proof.B, n * n):        # B es lineal
            return False
        if not PCPSystem._consistency_test(proof):              # A,B consistentes
            return False
        if not PCPSystem._satisfaction_test(formula, proof):    # x satisface φ
            return False
        return True


# --------------------------------------------------------------------------
# Solver: reducción Search-to-Decision. En cada variable fija x_i y pregunta
# al oráculo de decisión (¿queda satisfacible?) mediante el verificador PCP.
# --------------------------------------------------------------------------
class SatSolverPolyLog:
    def __init__(self, formula: Formula):
        self.formula = formula

    def _exists_satisfying_extension(self, partial):
        """Oráculo de decisión honesto: ¿existe extensión de 'partial' que
        satisface φ y cuya prueba PCP es ACEPTADA por el verificador?"""
        n = self.formula.num_vars
        free = n - len(partial)
        for combo in range(2 ** free):
            tail = [(combo >> k) & 1 for k in range(free)]
            cand = list(partial) + tail
            proof = PCPSystem.generate_proof(self.formula, cand)
            if PCPSystem.verify(self.formula, proof):   # verificación holográfica
                return True
        return False

    def solve(self):
        assignment = []
        for _ in range(self.formula.num_vars):
            if self._exists_satisfying_extension(assignment + [1]):
                assignment.append(1)
            elif self._exists_satisfying_extension(assignment + [0]):
                assignment.append(0)
            else:
                return None  # UNSAT
        # Verificación final por PCP de la solución completa
        final_proof = PCPSystem.generate_proof(self.formula, assignment)
        assert PCPSystem.verify(self.formula, final_proof)
        return [bool(b) for b in assignment]


# --------------------------------- DEMO ----------------------------------
if __name__ == "__main__":
    np.random.seed(0)
    phi = Formula(num_vars=4, clauses=[[-1, 2], [2, 3]])
    solver = SatSolverPolyLog(phi)

    solucion = solver.solve()
    print(f"Asignación encontrada: {solucion}")

    if solucion is not None:
        x = GF([1 if b else 0 for b in solucion])
        print(f"¿Satisface φ?         : {phi.is_satisfied(x)}")
        proof = PCPSystem.generate_proof(phi, solucion)
        print(f"Verificador PCP acepta: {PCPSystem.verify(phi, proof)}")

    # Prueba adversarial: una prueba NO lineal debe ser RECHAZADA
    bad = PCPSystem.generate_proof(phi, [True, False, True, False])
    bad.A = lambda a: int(np.random.randint(0, 2))   # oráculo tramposo (no lineal)
    print(f"\n[Adversarial] prueba no lineal aceptada?: {PCPSystem.verify(phi, bad)}")```

posted about 1 month ago

CC BY-SA 4.0

KaoruAK‭

-17 reputation 3 0 -11 4