시사 그래프

An implication graph representing the 2-satisfiability instance $\genfrac{}{}{0ex}{}{{\displaystyle (x_0\vee x_2)\wedge (x_0\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_4)\wedge (x_2\vee \mathrm{\neg }{x}_4)\wedge }}{(x_0\vee \mathrm{\neg }{x}_5)\wedge (x_1\vee \mathrm{\neg }{x}_5)\wedge (x_2\vee \mathrm{\neg }{x}_5)\wedge (x_3\vee x_6)\wedge (x_4\vee x_6)\wedge (x_5\vee x_6}$${\displaystyle \scriptscriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad \scriptscriptstyle (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land ($$x_{5}\lor x_{6}).$$}$

수학 논리학에서 시사 그래프는 정점 집합 V와 방향 모서리 집합 E로 구성된 스큐 대칭 지시 그래프 G = (V, E)이다.V의 각 꼭지점은 부울 리터럴의 진실 상태를 나타내며, 꼭지점 u에서 꼭지점 v까지의 각 방향 가장자리는 "만약 리터럴 u가 참이라면 리터럴 v도 참"이라는 물질적 함의를 나타낸다.시사 그래프는 원래 복잡한 부울 식을 분석하는 데 사용되었다.

적용들

2-만족도 인스턴스는 각각의 분열을 하나의 함축에 의해 대체함으로써 함축 그래프로 변형될 수 있다.For example, the statement ${\displaystyle (x_{0}\lor x_{1})}$ can be rewritten as the pair ${\displaystyle (\neg x_{0}\rightarrow x_{1}),(\neg x_{1}\rightarrow x_{0})}$. An instance is satisfiable if and only if no literal and its negation belong to the same stron함축성 그래프의 gly 연결 성분. 이 특성화는 선형 시간에서 2차원 가능성을 해결하는 데 사용될 수 있다.^[1]

CDCL SAT-솔루버에서 단위 전파는 결정 리터럴로부터 모든 잠재 리터럴을 도출하는 가능한 모든 방법을 포착하는 시사 그래프와 자연스럽게 연관될 수 있으며,^[2] 이는 절 학습에 사용된다.

참조