71 lines
1.8 KiB
Python
71 lines
1.8 KiB
Python
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")
|