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 . As every clause only consists of two literals, every clause can be expressed as an implication:

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

Indirection Graph

Consider the Krom formula

Its implication graph is given by:

If some and 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 , then if is true, must also be true. 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 concludes in a YES-instance.