0과 1을 입력하면 0과 1을 출력하는 디지털 회로(정확히는 combinational circuit)를 명제논리식으로 표현할 수 있다는 것은 모두 익히 알고 있을 거야. 예를 들어 입력이 0일 때 출력이 1, 입력이 1일 때 출력이 0인 인버터는 입력값 = a, 출력값 = b 일 때 a ≡ ¬b 가 성립하므로 NOT 게이트라 불리기도 하지.


그렇다면 여기서 문제. 3개의 입력 와이어 p, q, r이 있고, 이를 각각 반전하는 출력 와이어 p', q', r' 을 가진 간단한 회로를 설계한다고 하자. 예를 들어 p, q, r 의 신호가 1, 0, 1 일 때 p', q', r' 의 신호는 0, 1, 0 이어야 한다. 하지만 가장 중요한 인버터는 단 2개밖에 사용할 수 없다. 대신 AND 게이트와 OR 게이트는 무제한으로 사용할 수 있다. 이 설계 조건을 충족시킬 수 있을까?


논리적으로 표현하자면 다음과 같다. 문제의 조건을 지키며 구성할 수 있는 와이어의 집합을 S라 하자. 이 경우,


1. p, q, r ∈ S.

2. 임의의 a 와 b에 대해, a, b ∈ S 라면 (a ∧ b) ∈ S.

3. 임의의 a 와 b에 대해, a, b ∈ S 라면 (a ∨ b) ∈ S.

4. 임의의 a에 대해, a ∈ S 라면 ¬a ∈ S.

5. 단, 4번 규칙은 2번 밖에 사용할 수 없다.


이 룰을 준수하면서 p ≡ ¬p', q ≡ ¬q', r ≡ ¬r' 가 성립하는 p', q', r' ∈ S 를 찾으면 된다.


문제는 간단하지만 풀이는 쉽지 않다. 나는 손으로 푸는 건 포기하고 SMT solver를 썼는데, 문제의 요점을 기술하고 자동화하는 감각을 익히는 연습으로는 그것도 나쁘지 않음.


출처는 John Harrison의 Handbook of Practical Logic and Automated Reasoning. 퍼즐의 원 저자는 인텔의 E. Snow라고 한다.