Krom Formula

logic computation

Definition

Krom Formula

A Krom formula is a CNF formula where each clause contains at most two literals. These formulas are also referred to as 2-CNF formulas and can be solved in polynomial time.

Tractability

Krom formulas form a sub-class of SAT that is efficiently solvable.

Computing

Given a Krom formula $F$. As every clause only consists of two literals, every clause can be expressed as an implication:

$$(x_0\vee \neg x_3)\equiv (\neg x_0⟹\neg x_3)\equiv (x_3⟹x_0)$$

Implications are directed edges, meaning we can construct an implication graph based on $F$.

Indirection Graph

Consider the Krom formula

$$\begin{array}{rl}F=& (x_0\vee x_2)\wedge (x_0\vee \neg x_3)\wedge (x_1\vee \neg x_3)\wedge (x_1\vee \neg x_4)\\ & \wedge (x_2\vee \neg x_4)\wedge (x_0\vee \neg x_5)\wedge (x_1\vee \neg x_5)\wedge (x_2\vee \neg x_5)\\ & \wedge (x_3\vee x_6)\wedge (x_4\vee x_6)\wedge (x_5\vee x_6).\end{array}$$

Its implication graph is given by:

If some $x_i$ and $\neg x_i$ lie in the same strongly connected component, i.e. there exists some implication path s.t. they imply each other, we output a NO-instance. Otherwise, we output a YES-instance.

So if there is a path $u⇝v$, then if $u$ is true, $v$ must also be true. $x_i⇝\cdots ⇝\neg x_i$ means there’s a contradiction (law of excluded middle), and the formula is unsatisfiable.

Implication Graph: Strongly Connected Components

Trivially, every vertex is a singleton in its own strongly connected component:

Therefore, there are no contradictory paths, meaning $F$ concludes in a YES-instance.