beam: 2-SAT solver (Tarjan SCC) with randomized brute-force tests

wizard-work/beam/test_two_sat.py

@@ -0,0 +1,70 @@
+from two_sat import solve
+
+def check(n, clauses, assign):
+    for a, b in clauses:
+        def val(lit):
+            v = abs(lit)-1
+            x = assign[v]
+            if lit > 0:
+                return x
+            return not x
+        assert val(a) or val(b), (a,b,assign)
+
+# basic satisfiable
+sat, a = solve(2, [(1,2),(-1,2),(1,-2)])
+assert sat and a == [True, True], (sat,a)
+check(2, [(1,2),(-1,2),(1,-2)], a)
+
+# unsat: (x1) and (!x1)
+sat, a = solve(1, [(1,1),(-1,-1)])
+assert not sat and a is None
+
+# empty
+sat, a = solve(3, [])
+assert sat
+
+# classic: (x1 or x2) and (!x1 or x2) and (x1 or !x2) and (!x1 or !x2) -> unsat
+sat, a = solve(2, [(1,2),( -1,2),(1,-2),(-1,-2)])
+assert not sat
+
+# unit-ish via duplicate
+sat, a = solve(1, [(1,1)])
+assert sat and a[0] is True
+check(1, [(1,1)], a)
+
+sat, a = solve(1, [(-1,-1)])
+assert sat and a[0] is False
+check(1, [(-1,-1)], a)
+
+# larger random brute force
+import itertools
+def brute(n, clauses):
+    for bits in itertools.product([False,True], repeat=n):
+        ok = True
+        for x,y in clauses:
+            def val(lit):
+                v=abs(lit)-1
+                b=bits[v]
+                return b if lit>0 else (not b)
+            if not (val(x) or val(y)):
+                ok=False;break
+        if ok:
+            return True, list(bits)
+    return False, None
+
+import random
+random.seed(42)
+for _ in range(2000):
+    n=random.randint(1,6)
+    m=random.randint(0,8)
+    clauses=[(random.randint(1,n)*random.choice([1,-1]),
+            random.randint(1,n)*random.choice([1,-1])) for _ in range(m)]
+    # ensure literals valid
+    clauses=[(a if a!=0 else 1, b if b!=0 else 1) for a,b in clauses]
+    s1,a1=solve(n,clauses)
+    s2,a2=brute(n,clauses)
+    assert s1==s2, (n,clauses,s1,s2)
+    if s1:
+        check(n,clauses,a1)
+
+print("ALL 2SAT TESTS PASSED")

wizard-work/beam/two_sat.py

@@ -0,0 +1,90 @@
+"""2-SAT solver via implication graph + strongly connected components (Tarjan).
+
+API:
+    solve(n, clauses) -> (sat, assignment)
+- n: number of boolean variables x_0..x_{n-1}.
+- clauses: iterable of (a, b) where each literal is an int in [-n, n]\\{0};
+  positive k means x_{k-1} true, negative -k means x_{k-1} false.
+  Each clause is (lit1 OR lit2). A unit clause can be (lit, lit) or (lit, 0)? We
+  require two literals; pass (lit, lit) for unit.
+- Returns (True, [bool,...]) if satisfiable, else (False, None).
+
+A clause (u OR v) becomes implications (!u -> v) and (!v -> u).
+Variable i true  -> node 2*i, false -> node 2*i+1 (0-based i).
+Negation of node x is x^1.
+"""
+from __future__ import annotations
+
+
+def _solve(n, clauses):
+    N = 2 * n
+    adj = [[] for _ in range(N)]
+    radj = [[] for _ in range(N)]
+
+    def node(lit):
+        # lit: signed 1-based variable index
+        v = abs(lit) - 1
+        if lit > 0:
+            return 2 * v          # true
+        return 2 * v + 1          # false
+
+    for a, b in clauses:
+        na, nb = node(a), node(b)
+        # (!a -> b) and (!b -> a)
+        # negation of node x is x^1
+        adj[na ^ 1].append(nb)
+        adj[nb ^ 1].append(na)
+        radj[nb].append(na ^ 1)
+        radj[na].append(nb ^ 1)
+
+    # Tarjan SCC (iterative to avoid recursion limits)
+    index_counter = [0]
+    stack = []
+    on_stack = [False] * N
+    indices = [-1] * N
+    lowlink = [0] * N
+    comp = [-1] * N
+    comp_count = [0]
+
+    import sys
+    sys.setrecursionlimit(max(sys.getrecursionlimit(), N + 100))
+
+    def strongconnect(v):
+        indices[v] = index_counter[0]
+        lowlink[v] = index_counter[0]
+        index_counter[0] += 1
+        stack.append(v)
+        on_stack[v] = True
+        for w in adj[v]:
+            if indices[w] == -1:
+                strongconnect(w)
+                lowlink[v] = min(lowlink[v], lowlink[w])
+            elif on_stack[w]:
+                lowlink[v] = min(lowlink[v], indices[w])
+        if lowlink[v] == indices[v]:
+            while True:
+                w = stack.pop()
+                on_stack[w] = False
+                comp[w] = comp_count[0]
+                if w == v:
+                    break
+            comp_count[0] += 1
+
+    for v in range(N):
+        if indices[v] == -1:
+            strongconnect(v)
+
+    for i in range(n):
+        if comp[2 * i] == comp[2 * i + 1]:
+            return False, None
+
+    # assignment: for each variable, if comp[true_node] > comp[false_node] then true
+    # (in reverse topological order of SCCs; higher comp index = earlier in topo order)
+    assign = [False] * n
+    for i in range(n):
+        assign[i] = comp[2 * i] < comp[2 * i + 1]
+    return True, assign
+
+
+def solve(n, clauses):
+    return _solve(n, clauses)