2-SAT 충족 가능성 계산기

「둘 중 하나는 참」인 조건이 여럿 있을 때 모두를 만족하는 참·거짓 배정이 있는지 묻는 문제입니다. (a ∨ b) ∧ (¬a ∨ c)처럼 절마다 변수가 정확히 둘인 경우를 말합니다.

절마다 변수가 둘이면 절이 함의로 바뀌기 때문입니다. (a ∨ b)는 「a가 거짓이면 b가 참이어야 한다」와 같아, 절 하나가 화살표 두 개가 됩니다. 셋만 되어도(3-SAT) 이 변환이 통하지 않습니다 — (a ∨ b ∨ c)는 하나가 거짓일 때 나머지 둘 중 하나라는 또 다른 논리합이 되기 때문입니다.

함의 그래프를 강한 연결 요소로 묶었을 때 x와 ¬x가 같은 덩어리에 있으면 배정이 없습니다. 같은 덩어리라는 것은 서로 오갈 수 있다는 뜻이고, 곧 「x가 참이면 거짓이어야 하고 거짓이면 참이어야 한다」이기 때문입니다. 그런 변수가 하나도 없으면 반드시 배정이 있습니다.

덩어리를 정점으로 본 축약 그래프에는 사이클이 없어 위상 정렬이 됩니다. x와 ¬x 중 위상 순서에서 뒤에 오는 쪽을 참으로 두면 모든 함의가 지켜집니다. 화살표가 앞에서 뒤로만 가므로 「참 → 거짓」인 화살표가 생길 수 없기 때문입니다.

「A 아니면 B는 반드시」 꼴의 제약이 잔뜩 있는 배치 문제에 쓰입니다. 좌석 배정, 지도에 이름표를 겹치지 않게 놓기, 회로에서 두 값 중 하나를 고르기 같은 문제가 2-SAT으로 바뀝니다.

있습니다. 이 도구는 그중 하나를 찾아 줍니다. 위상 순서에서 뒤에 오는 쪽을 참으로 두는 규칙을 쓰므로 언제나 같은 답이 나오지만, 다른 배정도 얼마든지 있을 수 있습니다.

전송되지 않습니다. 모든 계산은 브라우저 안에서 이뤄지고, 입력값은 이 기기에만 남습니다.