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")