Incidence Graph

graph-theory logic sat-solving

Definition

Incidence Graph

The incidence graph of a CNF formula $F$ is the bipartite graph whose vertex set consists of the variables of $F$ and the clauses of $F$. A variable vertex $x$ is adjacent to a clause vertex $C$ exactly if $x$ occurs in $C$, either positively as $x$ or negatively as $\neg x$.

Example: For the formula

$$F=(x_1\vee \neg x_2)\wedge (x_2\vee x_3)\wedge (\neg x_1\vee \neg x_3),$$

the incidence graph has variable vertices $x_1,x_2,x_3$ and clause vertices $C_1,C_2,C_3$, where

$$C_1=(x_1\vee \neg x_2),C_2=(x_2\vee x_3),C_3=(\neg x_1\vee \neg x_3),$$

together with the edges $x_1{C}_1$, $x_2{C}_1$, $x_2{C}_2$, $x_3{C}_2$, $x_1{C}_3$, and $x_3{C}_3$.

The corresponding incidence graph is: