논리곱 표준형

3. 변환

고전 논리에서 모든 명제 논리식은 그와 논리적 동치인 논리곱 표준형(CNF) 형태로 변환될 수 있다. 이러한 변환은 논리적 동치 관계에 기반하며, 주로 이중 부정 제거, 드 모르간의 법칙, 분배 법칙과 같은 규칙들이 사용된다.

모든 논리식을 CNF로 변환할 수 있다는 점 때문에, 논리 증명 등에서 모든 논리식이 CNF 형태임을 전제로 하는 경우가 많다.

그러나 CNF로의 변환 과정에서 원래의 논리식보다 훨씬 길어지는 경우가 발생할 수 있다. 예를 들어, 다음과 같은 형태의 논리식은

$(X\_1\; \backslash wedge\; Y\_1)\; \backslash vee\; (X\_2\; \backslash wedge\; Y\_2)\; \backslash vee\; \backslash dots\; \backslash vee\; (X\_n\; \backslash wedge\; Y\_n)$

CNF로 변환하면, $2^n$ 개의 절(clause)을 가지는 매우 긴 식이 될 수 있다.

$(X\_1\; \backslash vee\; X\_2\; \backslash vee\; \backslash cdots\; \backslash vee\; X\_n)\; \backslash wedge\; (Y\_1\; \backslash vee\; X\_2\; \backslash vee\; \backslash cdots\; \backslash vee\; X\_n)\; \backslash wedge\; \backslash cdots\; \backslash wedge\; (Y\_1\; \backslash vee\; Y\_2\; \backslash vee\; \backslash cdots\; \backslash vee\; Y\_n)$

이러한 지수적인 크기 증가 문제를 피하기 위해, 논리적 동치성은 유지하지 않지만 충족 가능성은 보존하는 변환 방법도 존재한다. 이 방법은 새로운 변수를 도입하여 논리식의 크기가 선형적으로 증가하도록 제한한다. 예를 들어 위의 논리식은 새로운 변수 $Z\_1,\; \backslash dots,\; Z\_n$을 도입하여 다음과 같은 CNF로 변환할 수 있다.

$(Z\_1\; \backslash vee\; \backslash cdots\; \backslash vee\; Z\_n)\; \backslash wedge\; (\backslash neg\; Z\_1\; \backslash vee\; X\_1)\; \backslash wedge\; (\backslash neg\; Z\_1\; \backslash vee\; Y\_1)\; \backslash wedge\; \backslash cdots\; \backslash wedge\; (\backslash neg\; Z\_n\; \backslash vee\; X\_n)\; \backslash wedge\; (\backslash neg\; Z\_n\; \backslash vee\; Y\_n)$

이 변환된 식은 원래 식과 충족 가능성은 동일하지만(equisatisfiable), 완전히 논리적으로 동치(equivalent)인 것은 아니다. 즉, $Z\_i$ 변수들은 원래 식의 만족 여부와는 별개로 값을 가질 수 있다.

3. 1. 변환 방법

진리표에서 $\backslash phi$의 결과값이 거짓(F)이 되는 경우들을 찾는다. 각 경우에 대해, 변수 $V$가 참(T)이면 $\backslash lnot\; V$를, 거짓(F)이면 $V$를 논리합(OR)으로 연결하여 절(clause)을 만든다. 이렇게 만들어진 모든 절들을 논리곱(AND)으로 연결하면 CNF가 된다.

진리표에서 $\backslash phi$가 거짓(F)인 경우는 다음과 같다.

• p=T, q=T, r=T → $(\backslash lnot\; p\; \backslash lor\; \backslash lnot\; q\; \backslash lor\; \backslash lnot\; r)$
• p=T, q=T, r=F → $(\backslash lnot\; p\; \backslash lor\; \backslash lnot\; q\; \backslash lor\; r)$
• p=T, q=F, r=F → $(\backslash lnot\; p\; \backslash lor\; q\; \backslash lor\; r)$
• p=F, q=T, r=F → $(p\; \backslash lor\; \backslash lnot\; q\; \backslash lor\; r)$

4. 일차 논리에서의 CNF

일차 논리에서 논리곱 정규형(CNF)은 논리식의 절 정규형(Clausal Normal Form)으로 더욱 발전될 수 있으며, 이는 일차 해상도를 사용하여 자동 정리 증명을 수행하는 데 사용된다.^[1]

해상도 기반 자동 정리 증명에서 논리곱 정규형(CNF)은 다음과 같은 형태를 가지며,

$(l\_\{11\}\; \backslash lor\; \backslash ldots\; \backslash lor\; l\_\{1n\_1\})\; \backslash land\; \backslash ldots\; \backslash land\; (l\_\{m1\}\; \backslash lor\; \backslash ldots\; \backslash lor\; l\_\{mn\_m\})$

일반적으로 리터럴(literal) 집합의 집합으로 표현된다.

$\backslash \{\; \backslash \{\; l\_\{11\},\; \backslash ldots,\; l\_\{1n\_1\}\; \backslash \},\; \backslash ldots,\; \backslash \{\; l\_\{m1\},\; \backslash ldots,\; l\_\{mn\_m\}\; \backslash \}\; \backslash \}$

일차 논리식을 CNF로 변환하는 과정은 다음과 같다.^[2]

# '''부정 정규형(NNF)으로 변환한다.'''

## 함의($\backslash rightarrow$)와 동치($\backslash leftrightarrow$)를 제거한다: $P\; \backslash rightarrow\; Q$를 $\backslash lnot\; P\; \backslash lor\; Q$로 반복해서 바꾸고, $P\; \backslash leftrightarrow\; Q$를 $(P\; \backslash lor\; \backslash lnot\; Q)\; \backslash land\; (\backslash lnot\; P\; \backslash lor\; Q)$로 바꾼다. 이 과정을 통해 모든 함의와 동치 기호를 제거한다.

## 부정($\backslash lnot$) 기호를 안쪽으로 이동시킨다: 드 모르간의 법칙을 반복 적용하여 $\backslash lnot\; (P\; \backslash lor\; Q)$를 $(\backslash lnot\; P)\; \backslash land\; (\backslash lnot\; Q)$로, $\backslash lnot\; (P\; \backslash land\; Q)$를 $(\backslash lnot\; P)\; \backslash lor\; (\backslash lnot\; Q)$로 바꾼다. 또한, $\backslash lnot\backslash lnot\; P$는 $P$로, $\backslash lnot\; (\backslash forall\; x\; P(x))$는 $\backslash exists\; x\; \backslash lnot\; P(x)$로, $\backslash lnot\; (\backslash exists\; x\; P(x))$는 $\backslash forall\; x\; \backslash lnot\; P(x)$로 바꾼다. 이 과정을 마치면 부정 기호는 술어 기호 바로 앞에만 나타나게 된다.

# '''변수를 표준화한다.'''

## 서로 다른 한정 기호(quantifier)에서 동일한 변수 이름을 사용하는 경우, 변수 이름을 변경한다. 예를 들어, $(\backslash forall\; x\; P(x))\; \backslash lor\; (\backslash exists\; x\; Q(x))$와 같은 식은 $(\backslash forall\; x\; P(x))\; \backslash lor\; (\backslash exists\; y\; Q(y))$처럼 변경한다. 이는 나중에 한정 기호를 제거할 때 혼동을 방지하기 위함이다. 예를 들어, $\backslash forall\; x\; [\backslash exists\; y\; \backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)]\; \backslash lor\; [\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)]$는 $\backslash forall\; x\; [\backslash exists\; y\; \backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)]\; \backslash lor\; [\backslash exists\; z\; \backslash mathrm\{Loves\}(z,x)]$로 이름을 변경한다.

# '''스콜렘 정규형(Skolem Normal Form)으로 변환한다.'''

## 한정 기호를 식의 바깥쪽으로 이동시킨다: $P$가 변수 $x$를 포함하지 않을 때, $P\; \backslash land\; (\backslash forall\; x\; Q(x))$를 $\backslash forall\; x\; (P\; \backslash land\; Q(x))$로, $P\; \backslash lor\; (\backslash forall\; x\; Q(x))$를 $\backslash forall\; x\; (P\; \backslash lor\; Q(x))$로, $P\; \backslash land\; (\backslash exists\; x\; Q(x))$를 $\backslash exists\; x\; (P\; \backslash land\; Q(x))$로, $P\; \backslash lor\; (\backslash exists\; x\; Q(x))$를 $\backslash exists\; x\; (P\; \backslash lor\; Q(x))$로 바꾼다. 이전 단계에서 변수를 표준화했기 때문에 이러한 변환은 논리적 동치성을 유지한다. 이 과정을 거치면 모든 한정 기호는 식의 가장 앞부분에 위치하게 된다.

## 존재 한정 기호($\backslash exists$)를 제거한다: $\backslash forall\; x\_1\; \backslash ldots\; \backslash forall\; x\_n\; \backslash ;\; \backslash exists\; y\; \backslash ;\; P(y)$ 형태의 식을 $\backslash forall\; x\_1\; \backslash ldots\; \backslash forall\; x\_n\; \backslash ;\; P(f(x\_1,\backslash ldots,x\_n))$으로 반복해서 바꾼다. 여기서 $f$는 이전에 사용되지 않은 새로운 $n$-항 함수 기호이며, 이를 스콜렘 함수(Skolem function)라고 한다. 만약 존재 한정 기호가 다른 전체 한정 기호의 범위 내에 있지 않다면($n=0$), 새로운 0-항 함수 기호, 즉 스콜렘 상수(Skolem constant)를 사용한다. 이 단계는 논리적 동치성을 보장하지는 않지만, 충족 가능성(satisfiability)을 보존한다. 즉, 원본 식이 충족 가능하면 변환된 식도 충족 가능하며, 그 반대도 성립한다. 이 과정을 통해 모든 존재 한정 기호를 제거한다.

# '''모든 전체 한정 기호($\backslash forall$)를 제거한다.'''

## 모든 변수는 이제 전체 한정 기호에 의해 제한되므로, 전체 한정 기호를 생략해도 무방하다. 모든 변수는 암묵적으로 전체적으로 한정된 것으로 간주한다.

# '''논리합($\backslash lor$)을 논리곱($\backslash land$) 안으로 분배한다.'''

## 분배 법칙을 반복 적용하여 $P\; \backslash lor\; (Q\; \backslash land\; R)$ 형태를 $(P\; \backslash lor\; Q)\; \backslash land\; (P\; \backslash lor\; R)$ 형태로 바꾼다. 최종 결과는 논리곱으로 연결된 논리합들의 형태, 즉 CNF가 된다.

'''예시'''

"모든 동물을 사랑하는 사람은 누군가에게 사랑받는다"라는 문장을 CNF로 변환하는 과정은 다음과 같다. (각 단계에서 변경되는 부분을 $\{\backslash color\{red\}\{\backslash text\{빨간색\}\}\}$으로 표시)

1. 원본 문장: $\backslash forall\; x\; ((\backslash forall\; y\; \backslash mathrm\{Animal\}(y)\; \backslash color\{red\}\backslash rightarrow\; \backslash mathrm\{Loves\}(x,\; y))\; \backslash color\{red\}\backslash rightarrow\; (\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)))$

2. 함의 제거 (1.1): $\backslash forall\; x\; (\backslash lnot\; (\backslash forall\; y\; \backslash lnot\; \backslash mathrm\{Animal\}(y)\; \backslash lor\; \backslash mathrm\{Loves\}(x,\; y))\; \backslash lor\; (\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)))$

3. 부정 기호 안쪽 이동 (1.2): $\backslash forall\; x\; ((\backslash exists\; y\; \backslash lnot\; (\backslash lnot\; \backslash mathrm\{Animal\}(y)\; \backslash lor\; \backslash mathrm\{Loves\}(x,\; y)))\; \backslash lor\; (\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)))$

$\backslash forall\; x\; ((\backslash exists\; y\; (\backslash lnot\backslash lnot\; \backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)))\; \backslash lor\; (\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)))$

$\backslash forall\; x\; ((\backslash exists\; y\; (\backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)))\; \backslash lor\; (\backslash exists\; y\; \backslash mathrm\{Loves\}(y,\; x)))$

4. 변수 표준화 (2): (두 번째 $\backslash exists\; y$를 $\backslash exists\; z$로 변경)

$\backslash forall\; x\; ((\backslash exists\; y\; (\backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y)))\; \backslash lor\; (\backslash color\{red\}\backslash exists\; z\; \backslash mathrm\{Loves\}(z,\; x)))$

5. 스콜렘화 (3.1, 3.2): (한정 기호 밖으로 이동 후 스콜렘 함수 $f(x)$, $g(x)$ 도입)

$\backslash forall\; x\; \backslash exists\; z\; (\backslash exists\; y\; (\backslash mathrm\{Animal\}(y)\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; y))\; \backslash lor\; \backslash mathrm\{Loves\}(z,\; x))$ (한정 기호 이동은 생략 가능)

$\backslash forall\; x\; ((\backslash mathrm\{Animal\}(\backslash color\{red\}\{f(x)\})\; \backslash land\; \backslash lnot\; \backslash mathrm\{Loves\}(x,\; \backslash color\{red\}\{f(x)\}))\; \backslash lor\; \backslash mathrm\{Loves\}(\backslash color\{red\}\{g(x)\},\; x))$

• 여기서 $g(x)$는 $x$를 사랑하는 존재를 나타내는 스콜렘 함수이고, $f(x)$는 $x$가 사랑하지 않는 동물을 나타내는 스콜렘 함수이다.

5. 계산 복잡도

계산 복잡도 이론에서 논리곱 표준형(CNF)으로 표현된 부울 공식의 만족 가능성 문제는 중요한 위치를 차지한다. 이는 주어진 CNF 공식을 참으로 만드는 변수 값 할당이 존재하는지 찾는 문제로, SAT(Satisfiability) 문제라고 불린다.

특히, CNF 공식에서 각 논리합(절, disjunction)이 최대 ''k''개의 리터럴을 포함하는 경우의 만족 가능성 문제를 '''k-SAT''' 문제라고 한다. 3-SAT 문제는 대표적인 NP-완전 문제로 알려져 있으며, 이는 ''k'' > 2인 다른 모든 ''k''-SAT 문제에도 해당된다. 반면, 2-SAT 문제는 다항 시간 안에 해결할 수 있는 것으로 알려져 있다.^[2]

이러한 복잡도 차이 때문에, CNF 공식을 만족 가능성을 유지하면서 DNF로 변환하는 작업은 NP-어려움 문제이다. 마찬가지로, 유효성을 유지하면서 CNF로 변환하거나, 등가성을 유지하면서 DNF 또는 CNF로 변환하는 것 역시 NP-어려움에 속한다.

실제 응용에서는 각 절에 3개 이하의 리터럴을 갖는 "3CNF" 형식의 공식이 자주 등장하며, 매우 큰 규모(예: 100,000개의 변수와 1,000,000개의 절)를 가질 수 있다. $k\; \backslash ge\; 3$인 CNF 공식은 새로운 변수 ''Z''를 도입하여 $X\_1\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_k\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_n$을 두 개의 절 $X\_1\; \backslash vee\; \backslash ldots\; \backslash vee\; X\_\{k-1\}\; \backslash vee\; Z$와 $\backslash neg\; Z\; \backslash vee\; X\_k\; \backslash lor\; \backslash ldots\; \backslash vee\; X\_n$으로 대체하는 과정을 반복함으로써, 만족 가능성이 동일한 ''k''CNF 형식(특히 3CNF)으로 변환할 수 있다.

CNF 형식은 SAT 문제 해결을 위한 중요한 표현 방식이며, 이진 결정도(BDD)와 같은 자료 구조를 활용하여 효율적으로 해를 찾는 연구가 진행되고 있다.^[2]

6. 활용

연언 정규형(CNF)은 다양한 분야에서 활용된다.

• 자동 정리 증명: 연언 정규형으로부터 절 정규형을 만들 수 있으며, 이 절 정규형은 도출과 같은 자동 정리 증명 기법의 입력 형식으로 사용된다. 이를 통해 논리식의 타당성이나 모순 여부를 기계적으로 증명할 수 있다.
• 충족가능성 문제(SAT) 해결: 계산 복잡도 이론에서 중요한 문제 중 하나는 주어진 연언 정규형 논리식을 참(True)으로 만드는 변수 값의 조합이 존재하는지 찾는 충족가능성 문제(SAT)이다. CNF는 SAT 솔버의 표준 입력 형식으로 널리 사용된다. 변수가 3개인 3-SAT 문제는 NP 완전 문제로 알려져 있지만 (3개 이상 변수를 갖는 SAT 문제도 마찬가지이다), 변수가 2개인 2-SAT 문제는 다항 시간 안에 풀 수 있는 효율적인 알고리즘이 존재한다.
• 이진 결정 그래프(BDD): 연언 정규형으로 표현된 논리식의 모든 충족 해를 구하는 방법 중 하나로 이진 결정 그래프를 활용할 수 있다. 논리식을 이진 결정 그래프로 표현하고 압축하면, 충족가능성 문제나 최적화 문제의 해를 실용적으로 도출하는 데 도움이 될 수 있다.^[2]

7. 한국의 관련 연구 및 동향

논리곱 표준형(CNF)은 계산 복잡도 이론에서 중요한 문제인 충족가능성 문제(SAT)와 밀접한 관련이 있다. SAT 문제는 주어진 CNF 형식의 논리식을 "참"으로 만드는 각 변수의 참/거짓 조합을 찾는 문제이다. 특히 3개의 변수를 사용하는 3-SAT 문제는 NP 완전 문제로 분류되어 해결하기 어려운 문제로 알려져 있지만, 2개의 변수를 사용하는 2-SAT 문제는 다항 시간 안에 풀 수 있다.

한국의 여러 대학 및 연구소에서는 이러한 SAT 문제의 효율적인 해결을 위한 SAT 솔버 개발 및 성능 향상 연구를 활발히 진행하고 있다. 또한, CNF는 소프트웨어 공학 분야에서 모델 체킹 기술을 활용하여 소프트웨어의 오류를 검증하고 신뢰성을 높이는 데 중요한 역할을 한다. 이 과정에서 복잡한 시스템의 상태나 속성을 CNF로 표현하고 분석하는 기법이 사용된다.

인공지능 분야에서도 CNF 기반의 접근 방식이 문제 해결, 계획 수립, 논리적 추론 등 다양한 영역에서 활용되고 있다. 예를 들어, 특정 조건을 만족하는 계획을 찾거나 지식 베이스로부터 새로운 사실을 추론하는 데 CNF와 SAT 솔버 기술이 응용될 수 있다.

CNF 식의 모든 해를 구하거나 최적의 해를 찾는 조합 최적화 문제 해결을 위해 이진 결정 그래프와 같은 자료 구조를 활용하는 연구도 이루어지고 있다. 이진 결정 그래프는 논리식을 간결하게 표현하고 조작할 수 있게 하여, 실용적인 문제 해결에 도움을 줄 수 있다.^[2] 이러한 연구들은 한국의 관련 학계 및 산업계에서 꾸준히 진행되며 기술 발전에 기여하고 있다.

참조

_[1] 문서 Disjunctive normal form#Conversion to DNF
_[2] 논문 Graph-Based Algorithms for Boolean Function Manipulation https://www.cs.cmu.e[...] IEEE Transactions on Computers 1986