two-sat

two-sat問題を解きます。 このプログラムはsccを基にして作られています。（つまり、sccにバグがあった場合、two-satにもバグが含まれている可能性が高いです。）

使用例

clauseは各要素が4次元タプルであるようなリストとなっています。ここは本家ACLと同じです。

ans=two_sat(N,clause)

のように呼び出されます。ここで、条件を満たすような割当が存在しないならばansはNoneであり、条件を満たすような割当が存在するならばその割当の一つが返ってきます。その場合、ansは長さがNのリストであって、各要素はTrueまたはFalseとなります。

(https://atcoder.jp/contests/practice2/tasks/practice2_h)

def two_sat(n,clause):
    #(中略)

N,D=map(int,input().split())
X=[0 for i in range(N)]
Y=[0 for i in range(N)]
for i in range(N):
    X[i],Y[i]=map(int,input().split())
clause=[]
for i in range(N):
    for j in range(i+1,N):
        if abs(X[i]-X[j])<D:
            clause.append((i,True,j,True))
        if abs(X[i]-Y[j])<D:
            clause.append((i,True,j,False))
        if abs(Y[i]-X[j])<D:
            clause.append((i,False,j,True))
        if abs(Y[i]-Y[j])<D:
            clause.append((i,False,j,False))

ans=two_sat(N,clause)
if ans==None:
    print("No")
else:
    print("Yes")
    for i in range(N):
        if ans[i]:
            print(Y[i])
        else:
            print(X[i])

(https://judge.yosupo.jp/problem/two_sat)

def two_sat(n,clause):
    #(中略)

p,cnf,N,M=input().split()
N,M=map(int,(N,M))
clause=[]
for i in range(M):
    a,b,z=map(int,input().split())
    c,d=(a//abs(a)+1)//2,(b//abs(b)+1)//2
    c,d=bool(c),bool(d)
    clause.append((abs(a)-1,c,abs(b)-1,d))
result=two_sat(N,clause)
if result==None:
    print("s UNSATISFIABLE")
else:
    print("s SATISFIABLE")
    print("v",*[(i+1) if result[i] else (-1-i) for i in range(N)]+[0])