[Challenge] Audit my Binary-Search SAT Solver — Find a counterexample or prove it correct

−2

Background

I've been experimenting with a novel approach to SAT solving: treat variable assignments as integers and binary-search over the solution space. I call it Binary-SAT Collapse.

The key insight: an n-variable assignment can be read as an n-bit integer. So the 2^n possible assignments are just the integers [0, 2^n - 1]. If I can binary-search over this range using a range-oracle, I can find a solution in O(log 2^n) = O(n) oracle calls.

The Algorithm

from itertools import product

def eval_cnf(cnf, assignment):
    for clause in cnf:
        if not any(
            (lit > 0 and assignment[abs(lit)-1] == 1) or
            (lit < 0 and assignment[abs(lit)-1] == 0)
            for lit in clause
        ):
            return False
    return True

def int_to_bits(x, n):
    return tuple((x >> i) & 1 for i in range(n))

def exists_solution_in_range(cnf, n, L, R):
    for x in range(L, R + 1):
        if eval_cnf(cnf, int_to_bits(x, n)):
            return True
    return False

def binary_sat_collapse(cnf, n):
    L = 0
    R = 2**n - 1
    while L <= R:
        m = (L + R) // 2
        if exists_solution_in_range(cnf, n, L, m):
            R = m - 1
        else:
            L = m + 1
    v = int_to_bits(L, n)
    return v if eval_cnf(cnf, v) else None

The Claim

binary_sat_collapse always returns a satisfying assignment if one exists, and None if the formula is unsatisfiable.

The Challenge

Either:

Option A: Find a CNF instance where the algorithm returns the wrong answer (False SAT or False UNSAT). Verify with Glucose/MiniSAT.
Option B: Prove the algorithm is correct — or prove why it can never be a practical SAT solver despite being "correct".

Scoring

Option A: score = number of literals in your counterexample CNF (fewer = better)
Option B: a clean proof or complexity argument, voted by the community