Problem:


Problem E: SAT-EN-3

彼女は悩んでいた。成績が良くないのだ。両親に無理を言って全寮制の学校に入学したものの、彼女の才能は一向に開花することはなかった。あるいは才能など元々なかったのかもしれないが、それはできるだけ考えたくない可能性だった。

そこで彼女が頼ったのは、インターネット上で見つけた怪しげな脳力トレーニングの教材だった。SAT-EN-3 (SATisifiability problem for Enhancement of Neuron: version 3) と銘打つその学習メソッドによると、充足可能性問題のようなもののインスタンスをひたすら手で解くことによって、計算力が向上し、引いては論理的思考力・直感力・想像力も豊かになり、部活動でも活躍できて恋愛もうまくいくのだという。さすがに最後の2つは眉唾ものじゃないかな、と彼女は思ったが、ソロバンや百マス計算のような例もあることだ。暗算が得意になったら儲けものかな、ぐらいの気楽さで、彼女はこの教材に取り組んでみることにした。

SAT-EN-3では、加法標準形で表される論理式の各変数に適切に割り当て、論理式の値を真にすることができるかどうか判定しなければならない。ちなみに、1つ以上の変数 (または、その否定) の論理積を 節 (clause) と呼び、いくつかの節の論理和で表される論理式のみが加法標準形に従っている。一般に充足可能性問題といえば論理式は乗法標準形で表されるが、SAT-EN-3では加法標準形であることに注意せよ。

彼女はしばらく SAT-EN-3 の問題集に取り組もうとして、ふと思い直した。問題集にお金を払うぐらいなら、プログラミングが得意な親友にパフェでもご馳走して、 SAT-EN-3 の問題を生成し、解くプログラムを書いてもらおう。そうすれば問題も解答もいくらでも手にはいるじゃないか。

こうして彼女の親友であるあなたは、SAT-EN-3を解くプログラムを書くことになったのである。

	

Input

入力は複数のケースからなる。
各ケースは以下のフォーマットで与えられる。

expression

入力の終わりは"#"からなる行によって与えられる

expressionは以下のBNFに従う。

ここでは文字列リテラルを""を用いて囲んでいる。
実際の入力に""は含まれない。
また入力には余計な空白は含まれていない。

<expression> ::= "("<clause>")" | "("<clause>")|("<expression>")"
<clause> ::= <literal>"&"<literal>"&"<literal>
<literal> ::= <variable> | "~"<variable>
<variable> ::= [a-z]|[A-z]

expressionの長さは500文字を超えない。

テストケースの数は1100個を超えない。

	

Output

与えられた式を満たす変数の割り当てが存在するのならばyesを、そうでなければnoを出力せよ。

Sample input

(B&B&f)|(~d&~i&i)|(~v&i&~V)|(~g&~e&o)|(~f&d&~v)|(d&~i&o)|(g&i&~B)|(~i&f&d)|(e&~i&~V)|(~v&f&~d)
(S&X&~X)
#

Sample output

yes
no

The University of Aizu Programming Contest 2011 Summer

原案: Tomoya Sakai

問題文: Takashi Tayama



Sample input:
(B&B&f)|(~d&~i&i)|(~v&i&~V)|(~g&~e&o)|(~f&d&~v)|(d&~i&o)|(g&i&~B)|(~i&f&d)|(e&~i&~V)|(~v&f&~d)
(S&X&~X)
#


Sample output:
yes
no

Submission status: Wrong Answer

Solution code:
def expr():
    global cur
    while cur < len(S):
        cur += 1 # '('
        if clause():
            return 1
        cur += 1 # ')'
    return 0

def clause():
    R = []
    global cur
    R.append(literal())
    cur += 1 # '&'
    R.append(literal())
    cur += 1 # '&'
    R.append(literal())
    return check(R)

def literal():
    global cur
    if S[cur] == '~':
        r = S[cur:cur+2]
        cur += 2 # '~a'
    else:
        r = S[cur]
        cur += 1 # 'a'
    return r

def check(R):
    for l0 in R:
        if len(l0) == 1:
            for l1 in R:
                if len(l1) == 2 and l1[1] == l0:
                    return 0
    return 1


ans = []
while 1:
    S = input()
    if S == '#':
        break
    cur = 0
    ans.append('yes' if expr() else 'no')
print(*ans, sep='\n')

Submission status: Wrong Answer

Solution code:
def judge(exp,torf,i):
	if i==len(dic):
		return eval(exp)
	else:
		return judge(exp,dic+[True],i+1) or judge(exp,dic+[False],i+1)
while 1:
	exp=list(raw_input())
	if exp[0]=="#":break
	dic=[]
	for i in range(len(exp)):
		if exp[i]=="&":exp[i]="and"
		elif exp[i]=="~":exp[i]="not"
		elif exp[i]=="|":exp[i]="or"
		elif exp[i]!="(" and exp[i]!=")":
			if exp[i] not in dic:
				dic.append(exp[i])
				exp[i]="torf["+str(len(dic)-1)+"]"
			else:
				exp[i]="torf["+str(dic.index(exp[i]))+"]"
	exp=" ".join(map(str,exp))
	print "yes" if judge(exp,[],0) else "no"

Submission status: Time Limit Exceeded

Solution code:
def judge(exp,torf,i):
	if i==len(dic):
		return eval(exp)
	else:
		return judge(exp,torf+[True],i+1) or judge(exp,torf+[False],i+1)
while 1:
	exp=list(raw_input())
	if exp[0]=="#":break
	dic=[]
	for i in range(len(exp)):
		if exp[i]=="&":exp[i]="and"
		elif exp[i]=="~":exp[i]="not"
		elif exp[i]=="|":exp[i]="or"
		elif exp[i]!="(" and exp[i]!=")":
			if exp[i] not in dic:
				dic.append(exp[i])
				exp[i]="torf["+str(len(dic)-1)+"]"
			else:
				exp[i]="torf["+str(dic.index(exp[i]))+"]"
	exp=" ".join(map(str,exp))
	print "yes" if judge(exp,[],0) else "no"

Submission status: Accepted

Solution code:
# AOJ 1078: SAT-EN-3
# Python3 2018.7.10 bal4u

def clause(e):
	f = True
	dic = {}
	f = e.split('&')
	for x in f:
		pm, t = 1, x[0]
		if t == '~':
			pm, t = -1, x[1]
		if t in dic and dic[t] + pm == 0: f = False
		dic[t] = pm
	return f

while True:
	p = input()
	if p == '#': break
	exp = list(p.split('|'))
	ans = False
	for e in exp:
		if clause(e[1:-1]):
			ans = True
			break
	print("yes" if ans else "no")

Submission status: Accepted

Solution code:
while True:
    s = input().strip()
    if s == '#': break

    clauses = s.split('|')
    for clause in clauses:
        literals = clause[1:-1].split('&')
        ntil = clause.count('~')
        if ntil == 0 or ntil == 3:
            print('yes')
            break
        if ntil == 1:
            x = [v[1] for v in literals if v[0] == '~'][0]
            if clause.count(x) == 1:
                print('yes')
                break
        if ntil == 2:
            x = [v for v in literals if len(v) == 1][0]
            if clause.count(x) == 1:
                print('yes')
                break
    else:
        print('no')

Submission status: Accepted

Solution code:
def expr():
    global cur
    while cur < len(S):
        cur += 1 # '('
        if clause():
            return 1
        cur += 2 # ')|'
    return 0

def clause():
    R = []
    global cur
    R.append(literal())
    cur += 1 # '&'
    R.append(literal())
    cur += 1 # '&'
    R.append(literal())
    return check(R)

def literal():
    global cur
    if S[cur] == '~':
        r = S[cur:cur+2]
        cur += 2 # '~a'
    else:
        r = S[cur]
        cur += 1 # 'a'
    return r

def check(R):
    for l0 in R:
        if len(l0) == 1:
            for l1 in R:
                if len(l1) == 2 and l1[1] == l0:
                    return 0
    return 1


ans = []
while 1:
    S = input()
    if S == '#':
        break
    cur = 0
    ans.append('yes' if expr() else 'no')
print(*ans, sep='\n')

Submission status: Accepted

Solution code:
def judge(exp,torf,i):
	if i==3:
		return eval(exp)
	else:
		return judge(exp,torf+[True],i+1) or judge(exp,torf+[False],i+1)
		
while 1:
	exp=raw_input().split("|")
	if exp[0]=="#":break
	for j in range(len(exp)):
		dic=[]
		exp[j]=list(exp[j])[1:-1]
		for i in range(len(exp[j])):
			if exp[j][i]=="&":exp[j][i]="and"
			elif exp[j][i]=="~":exp[j][i]="not"
			else:
				if exp[j][i] not in dic:
					dic.append(exp[j][i])
					exp[j][i]="torf["+str(len(dic)-1)+"]"
				else:
					exp[j][i]="torf["+str(dic.index(exp[j][i]))+"]"
		exp[j]=" ".join(map(str,exp[j]))
	for clause in exp:
		if judge(clause,[],0):
			print "yes"
			break
	else:
		print "no"

Submission status: Accepted

Solution code:
def judge(ex,torf,i):
	if i==3:
		return eval(ex)
	else:
		return judge(ex,torf+[True],i+1) or judge(ex,torf+[False],i+1)
		
while 1:
	ex=raw_input().split("|")
	if ex[0]=="#":break
	for j in range(len(ex)):
		dic=[]
		ex[j]=list(ex[j])[1:-1]
		for i in range(len(ex[j])):
			if ex[j][i]=="&":ex[j][i]="and"
			elif ex[j][i]=="~":ex[j][i]="not"
			else:
				if ex[j][i] not in dic:
					dic.append(ex[j][i])
					ex[j][i]="torf["+str(len(dic)-1)+"]"
				else:
					ex[j][i]="torf["+str(dic.index(ex[j][i]))+"]"
		ex[j]=" ".join(map(str,ex[j]))
	for clause in ex:
		if judge(clause,[],0):
			print "yes"
			break
	else:
		print "no"

Submission status: Accepted

Solution code:
while 1:
	exps=raw_input().split("|")
	if exps[0]=="#":break
	for i in range(len(exps)):
		v=True
		lits=exps[i][1:-1].split("&")
		for lit1 in lits:
			for lit2 in lits:
				if (lit1=="~"+lit2) or ("~"+lit1==lit2):
					v=False
		if v:
			print "yes"
			break
	else:
		print "no"

Submission status: Accepted

Solution code:
while 1:
	exps=raw_input().split("|")
	if exps[0]=="#":break
	for exp in exps:
		v=1
		lit=exp[1:-1].split("&")
		for i in range(2):
			for j in range(i+1,3):
				if (lit[i]=="~"+lit[j]) or ("~"+lit[i]==lit[j]):
					v=0
		if v:
			print "yes"
			break
	else:
		print "no"

Submission status: Accepted

Solution code:
while True:
    s = input()
    if s == '#':
        break
    ans = False
    clauses = s.split('|')
    for cla in clauses:
        clause = cla[1:-1]
        c = clause.split('&')
        tmp = True
        for ele in c:
            tmp &= not ('-' + ele if len(ele) == 1 else ele[-1]) in c
        ans |= tmp
    print("yes" if ans else "no")

Submission status: Accepted

Solution code:
while True:
    s = input()
    if s == "#":
        break

    clauses = s.split("|")
    for clause in clauses:
        literals = set(clause[1:-1].split("&"))
        for literal in literals:
            if literal[0] == "~" and literal[1] in literals:
                break
        else:
            print("yes")
            break
    else:
        print("no")