Graph Theory37 sections · 1633 units
Open in Course

Example Conversion

(Building the graph)

Say you have three clauses: "x OR y", "NOT x OR z", "NOT y OR NOT z". Let me build the graph step by step. Clause 11 adds edges: NOT x → y and NOT y → x. Clause 22 adds: x → z and NOT z → NOT x. Clause 33 adds: y → NOT z and z → NOT y. That is your implication graph. It has 66 nodes (x, NOT x, y, NOT y, z, NOT z) and 66 edges total.

Now you run SCC on this graph to check satisfiability. The SCC structure will tell you if this formula has a solution.