2-SAT — Implication Graph & SCC

Clause → two implications → SCC → satisfiability verdict & assignment
1. Build graph 2. SCC pass 3. Verdict

Formula (2-CNF)

One clause per line. Use x0, ~x1 (~ = NOT), separated by a space. Example: x0 x1 means (x0 ∨ x1).

Presets

Playback

Speed

Legend

literal visiting on SCC stack x & ¬x same SCC assigned true assigned false
Verdict: — pending —
Variables: 0
Clauses: 0
SCCs found: 0
Step: 0

Clauses & implications

Trace log