2SAT은 주어진 2-CNF(conjunctive normal form)의 해가 있는지 없는지 판정하고, 해가 있다면 그것이 무엇인지 알아내는 문제입니다.
Krom의 방법은 각 두 절로부터 resolution을 이용해서 새로운 절(논리적 귀결)들을 가능한 한 유도하면서 모순이 있는지 알아보고, 모순이 없다면 임의로 남은 문자에 진리값을 부여하고 위의 과정을 다시 진행하는 걸 끝날 때까지 반복합니다.
제 의문은 이 방법이 3SAT에 대해서도 되지 않을까 하는 것입니다.
resolution을 통해서 나오는 절의 리터럴 수가 3개 이하가 될 때만 그 절을 전체에 추가하기로 하고 말입니다.
여러분들 생각은 어떠신가요
