-3- CNF-SAT

Question

다음과 같이 3 CNF-SAT 문제를 변경하는 경우, 각각 C _I 들어
, _I = -x _I1 OR -x _I2 c를 OR x _i3 변수 중 하나가 부정을 나타내지 않음을 의미합니다.
또한 x의 일부 또는 모두에 값 (0 또는 1)이 제공됩니다.
다항식 시간에 문제를 해결하거나 (문제를 만족하는 x 값을 찾거나 충족 할 수 없다는 것을 증명할 수 있어야 함) 문제를 해결할 수 있어야합니다.

1. 이 문제를 해결하는 다항식 러닝 타임 알고리즘이란 무엇입니까?
2. 증명이 다항식 시간으로 실행됩니다.

힌트 : 표시하는 _C I = I1 -x _{OR -x I2} OR X _I3는 = C와 동일하다 (X I1 _{AND -x I2) - > x i3}

Answer 1

수식은 호른 수식의 하위 집합입니다. 따라서 만족 성 문제는 Horn satisfiability보다 어렵지 않으며 동일한 선형 시간 솔루션을 허용합니다.