소개

인생에서 당신의 사명은 간단합니다 : 인터넷에서 사람들을 잘못 증명하십시오!
이를 위해 일반적으로 진술을 신중하게 분석하고 모순을 지적하십시오.
이것을 자동화 할 때가되었지만, 게 으르면서 가능한 한 최소한의 노력으로 (사람들이 가장 짧은 코드를 읽음) 잘못을 증명하고자합니다.

사양

입력

입력 한 내용은 일반적인 형태 의 공식입니다 . 형식의 경우, 언어의 요구에 따라 아래 형식을 사용하거나 직접 정의 할 수 있습니다 (하지만 순수한 CNF보다 형식으로 더 많이 인코딩 할 수는 없습니다). 그러나 테스트 사례 (여기)는 아래 형식으로 제공됩니다 (자체 생성하기는 어렵지 않지만).

입력은 변수 목록의 목록입니다 (문자열로 읽거나 문자열 필요). 입력은 일련 의 절로 작성된 CNF (Conjunctive Normal Form)의 공식으로 , 각각 두 목록의 목록입니다. 절의 첫 번째 목록은 양수 리터럴 (변수)을 인코딩하고 두 번째 목록은 음수 (음수) 리터럴 (변수)을 인코딩합니다. 절의 모든 변수는 함께 OR되고 모든 절은 AND로 함께 있습니다.

보다 명확하게하려면 다음 [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]과 같이 읽을 수 있습니다.
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))

산출

출력은 부울 값입니다 (예 : 일부 실제 값 또는 일부 잘못된 값).

무엇을해야합니까?

간단합니다 : 주어진 공식이 만족 스러운지 확인하십시오. 예를 들어, 전체 공식이 “true”가되도록 모든 변수에 true와 false가 할당되어 있는지 확인하십시오. 수식을 만족할 수 있으면 출력이 “true”이고 그렇지 않으면 “false”가됩니다.
재미있는 사실 : 이것은 일반적인 경우 NP 완료 문제입니다.
참고 : 진리표를 생성하고 결과 항목이 true인지 확인하는 것이 허용됩니다.

코너 케이스

빈 3 단계 목록을 얻는다면 해당 절에 그러한 (긍정적 / 부정적) 변수가 없습니다-유효한 입력.
원하는 경우 다른 코너 케이스를 정의하지 않은 상태로 둘 수 있습니다.
빈 수식 (1 단계 목록)에서는 true를, 빈 절 (2 단계 목록)에서는 false를 반환 할 수도 있습니다.

누가 이겼어?

이것은 코드 골프이므로 바이트 단위의 최단 답변이 이깁니다!
물론 표준 규칙이 적용됩니다.

테스트 사례

[[[P],[Q,R]],[[Q,R],[P]],[[Q],[P,R]]] -> true
[[[],[P]],[[S],[]],[[R],[P]],[[U],[Q]],[[X],[R]],[[Q],[S]],[[],[P,U]],[[W],[Q,U]]] -> true
[[[],[P,Q]],[[Q,P],[]],[[P],[Q]],[[Q],[P]]] -> false
[[[P],[]],[[],[P,S]],[[P,T],[]],[[Q],[R]],[[],[R,S]],[[],[P,Q,R]],[[],[P]]] -> false
optional behavior (not mandatory, may be left undefined):
[] -> true (empty formula)
[[]] -> false (empty clause)
[[[],[]]] -> false (empty clause)

답변

SatisfiableQ

SatisfiableQ[Or@@Join[#,Not/@#2]&@@@And@@#]&

t=1<3
e%((t,f):r)=or((e<$>t)++map(not.e)f)&&e%r
e%_=t
u v b e s|s==v=b|t=e s
s e[]c=1<0
s e(v:w)c=e%c||s(u v t e)w c||s(u v(1<0)e)w c
g v[]=v
g v((t,f):r)=g(v++[x|x<-t++f,notElem x v])r
g[]>>=s(\x->t)

type Variable   = String
type CNF        = [([Variable], [Variable])]
type Evaluation = (Variable -> Bool)

satisfies :: Evaluation -> CNF -> Bool
satisfies eval [] = True
satisfies eval ((t,f):r) = or(map eval t ++ map (not.eval) f) && satisfies eval r

update :: Evaluation -> Variable -> Bool -> Evaluation
update eval s b var = if var == s then b else eval var

search :: Evaluation -> [Variable] -> CNF -> Bool
search eval [] cnf = False
search eval (v:vars) cnf = satisfies eval cnf || search (update eval v True) vars cnf || search (update eval v False) vars cnf

getVars :: CNF -> [Variable] -> [Variable]
getVars [] vars = vars
getVars ((t,f):cnf) vars = getVars cnf (vars ++ [v |v<-(t++f), notElem v vars])

isSat :: CNF -> Bool
isSat cnf = search (\x->True) (getVars cnf []) cnf

x=>f=(v,e)=>(e=v.pop())?[0,1].some(t=>f([...v],eval(e+'=t'))):eval(x)

f('a|b')(['a','b'])
true