단위 전파

단위 전파(UP) 또는 부울 구속조건 전파(BCP) 또는 1리터 규칙(OLR)은 일련의 (일반적으로 명제) 조항을 단순화할 수 있는 자동화된 정리 절차다.

정의

절차는 단위 절, 즉 하나의 리터럴로 구성된 절들을 결합 정상 형태로 기초로 한다.각 조항이 충족되어야 하기 때문에, 우리는 이 문자 그대로가 사실이어야 한다는 것을 알고 있다.조항 집합에 단위 조항 $l{\displaystyle }$ ${\displaystyle l}$이 포함된 경우$,$ 다른 조항은 다음 두 규칙을 적용하여 단순화된다.

1. $l{\displaystyle }$ ${\displaystyle l}$을(를) 포함하는 모든 조항(단위 조항 자체를 제외한)이 제거됨$$($l{\displaystyle }$ ${\displaystyle l}$인 경우$$ 해당 조항이 충족됨);
2. $\neg {\displaystyle \mathrm{}}$ ${\displaystyle l}$ ${\displaystyle \neg l}$을(를) 포함하는 모든 절에서 이$$ 리터럴은 삭제된다$$( ${\displaystyle l}$l ${\displaystyle \neg$ l$}).$

이 두 규칙을 적용하면 구약에 준하는 조항이 새로 생기게 된다.

예를 들어 다음과 같은 조항 집합은 단위 절 $a{\displaystyle }$ ${\displaystyle a}$을(를) 포함하기 때문에 단위 전파를 통해 단순화할 수 있다$.$

$\displaystyle \{a\vee b,\neg a\bee c,\neg c\bee d,a\}}$

${\displaystyle \vee }$ ${\displaystyle b}$ ${\displaystyle a\vee b}$은(는) 리터럴 $a{\displaystyle }$ ${\displaystyle a}$을(를) 포함하므로 이 절을 모두 제거할 수 있다$.$${\displaystyle \neg }$ ${\displaystyle c}$ ${\displaystyle \neg$ a$\ve$ c$}$은 단위 절에서 리터럴의 부정을 포함하므로$$, 이 리터럴은 절에서 제거할 수 있다.단위 절 $a{\displaystyle }$ ${\displaystyle a}$은(는) 제거되지$$ 않는다. 이렇게 하면 결과 세트가 원래 절과 동일하지 않을 수 있다. 이 절은 이미 다른 형태로 저장된 경우 제거할 수 있다("부분 모델 사용" 섹션 참조).단위 전파의 효과는 다음과 같이 요약할 수 있다.

${\displaystyle \{}$	$a\vee b,}$	$\displaystyle \neg a\bee c,}$	$\displaystyle \neg c\vee d,}$	$(\displaystyle a}$	${\displaystyle \}}$
	(iii)	$({\displaystyle \neg a}$ ${\displaystyle \mathrm{삭제}}$됨)	(iii)	(iii)
${\displaystyle \{}$		$(\displaystyle c,})$	$\displaystyle \neg c\vee d,}$	$(\displaystyle a}$	${\displaystyle \}}$

결과적인 절들의 ${\displaystyle \mathrm{집합}}$은 ${\displaystyle 위}$의 것과 같다$$$.{$ d$,a\}.$단위 전파의 결과인$$ $새로운{\displaystyle }$ 단위 조항 c ${\displaystyle c}$을(를) 장치 전파의 추가 적용에 사용할 수 있으며, 이 경우 $\neg {\displaystyle \mathrm{}}$ ${\displaystyle c}$ ${\displaystyle \vee }$ d ${\displaystyle \neg$ c$\ve d}$이(가) $d{\displaystyle }$ ${\displaystyd}$로 변환된다$.$

단위 전파 및 분해능

단위 전파의 두 번째 규칙은 제한된 형태의 분해능으로 볼 수 있으며, 두 개의 분해능 중 하나는 항상 단위 절이어야 한다.결의에 대해서는, 단위 전파는, 구절이 수반하지 않는 새로운 조항을 결코 생산하지 않는다는 점에서, 올바른 추론 규칙이다.단위 전파와 분해능의 차이는 다음과 같다.

1. 분해능은 단위 전파가 아닌 동안 완전한 반박 절차다. 다시 말하면, 조항 세트가 모순되더라도 단위 전파가 불일치를 발생시키지 않을 수 있다.
2. 일반적으로 해결된 두 조항은 생성된 조항을 세트에 추가한 후 제거할 수 없다. 반대로 장치 전파에 관련된 비단위 조항은 세트에 단순화가 추가될 때 제거할 수 있다.
3. 일반적으로 해상도는 단위 전파에 사용되는 첫 번째 규칙을 포함하지 않는다.

서브섬션을 포함하는 분해능 계산은 서브섬션에 의해 규칙 1을, 유닛 분해능 단계에 따라 규칙 2를 모델링할 수 있다.

새로운 단위 조항이 생성될 때 반복적으로 적용되는 단위 전파는 명제 Horn 절의 집합에 대한 완전한 만족도 알고리즘이다. 또한 만족도가 높을 경우 집합에 대한 최소 모델을 생성한다: Horn 만족도 참조.

부분 모형 사용

절의 집합에 존재하거나 그것으로부터 파생될 수 있는 단위 절은 부분 모델 형태로 저장할 수 있다(이 부분 모델은 적용에 따라 다른 리터럴을 포함할 수도 있다).이 경우 부분모형의 리터럴을 기준으로 단위 전파를 수행하며, 그 리터럴이 모형에 있으면 단위 절이 제거된다.위의 예에서, 단위 절 $a{\displaystyle }$ ${\displaystyle a}$이 부분 모델에 추가될 것이다$$. 그런 다음 절 세트의 단순화는 단위 절 $a{\displaystyle }$ ${\displaystyle a}$이(가) 세트에서 제거되었다는$$ 차이와 함께 위와 같이 진행될 것이다.결과적인 절들의 집합은 부분모형의 리터럴의 타당성을 가정했을 때 원래의 것과 동등하다.

복잡성

단위 전파를 직접 시행하는 데는 점검할 세트의 전체 크기에서 2차적으로 시간이 소요되는데, 이는 모든 조항의 크기의 합으로 정의되며, 여기서 각 조항의 크기는 그 조항의 크기가 포함된 리터럴의 수이다.

그러나 단위 전파는 각 변수에 대해 각 리터럴이 들어 있는 절의 목록을 저장함으로써 선형적으로 이루어질 수 있다.예를 들어 위의 세트는 각 절에 다음과 같이 번호를 매겨 나타낼 수 있다.

${\displaystyle \{1:a\vee b,2:\neg a\vee c,3:\neg c\vee d,4:a\}}$

변수 또는 부정을 포함하는 절 목록을 각 변수에 대해 저장하십시오.

$a:1\ 2\ 4}$

${\displaystyle b:1}}$

$(\displaystaystyle c:2\ 3}$

${\displaystyle d:3}$

이 간단한 데이터 구조는 세트 크기에서 시간 선형으로 구축될 수 있으며 변수를 포함하는 모든 절을 매우 쉽게 찾을 수 있다.리터럴의 단위 전파는 리터럴의 변수를 포함하는 절의 목록만 스캔하면 효율적으로 수행될 수 있다.보다 정확히 말하면, 모든 단위 절에 대해 단위 전파를 수행하기 위한 총 가동 시간은 절 집합의 크기에서 선형이다.

참고 항목

• 경적 만족도
• 경적절
• 자동 정리 증명
• DPLL 알고리즘

참조

• Dowling, William F.; Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming, 1 (3): 267–284, doi:10.1016/0743-1066(84)90014-1, MR 0770156.
• H. 장과 M.스틱엘(1996년).단위 제안을 위한 효율적인 알고리즘.인공지능과 수학에 관한 제4차 국제심포지엄의 진행에서.