V

Algorithm Visualizer

ZHEN
Share on WeiboShare on XGitHub repositoryAuthor website
Learning ToolsAlgorithm Complexity ReferenceAlgorithm Learning Paths
Data StructuresArrayLinked ListStackQueue and DequeBinary Search TreeBinary HeapHash TableGraphTrieDisjoint Set UnionLRU CacheSkip ListSegment TreeB+ TreeBloom FilterFenwick Tree
SortingBubble SortCocktail Shaker SortBitonic SortSelection SortInsertion SortBinary Insertion SortShell SortMerge SortTop-Down Merge SortQuick SortThree-Way Quick SortDual-Pivot Quick SortHeap SortCounting SortRadix SortBucket Sort
Graph AlgorithmsDijkstra's Shortest PathKruskal's Minimum Spanning TreePrim's Minimum Spanning TreeBellman-Ford Shortest PathsTopological SortFloyd-WarshallStrongly Connected Components2-SATMaximum FlowBipartite MatchingLowest Common AncestorEulerian Path
Dynamic ProgrammingEdit Distance0/1 KnapsackUnbounded KnapsackLongest Common SubsequenceLongest Increasing SubsequenceCoin ChangeStone MergingTraveling Salesperson DPTree Dynamic ProgrammingDigit DPRerooting DP
Backtracking and SearchN-QueensSubsetsPermutationsCombination SumMaze Solving with DFSNumber of IslandsWord SearchSudoku SolverA* Search
StringsKMP String MatchingRabin-Karp String MatchingBoyer-Moore String MatchingManacher's Longest Palindromic SubstringSuffix ArrayLCP ArrayAho-Corasick AutomatonZ Function
Math and Number TheorySieve of EratosthenesLinear SieveEuclidean AlgorithmBinary ExponentiationExtended Euclidean AlgorithmChinese Remainder TheoremEuler's Totient FunctionMiller-Rabin Primality TestFast Fourier TransformPollard's Rho Factorization
Computational GeometryConvex HullRotating CalipersClosest Pair of PointsLine Segment IntersectionBentley-Ottmann Sweep Line
SearchingBinary SearchLower and Upper BoundSearch in a Rotated Sorted ArrayBinary Search on the AnswerTernary Search

2-SAT

Convert two-literal clauses into implications, group them by SCC, and derive a satisfying assignment.

Core idea

Clause a or b is equivalent to two implications: not a implies b, and not b implies a. Strongly connected components expose contradictions and provide an assignment order.

Read the visualization

Each variable appears as two literal vertices. Clause edges arrive in pairs, SCC colors group mutual implications, and the final badges show the selected truth values.

A¬AB¬BC¬C

Create one implication-graph vertex for every literal and its negation.

1function twoSat(n: number, clauses: [number, number][]): boolean[] | null {
2 const g: number[][] = Array.from({ length: 2 * n }, () => []); // 2n literal init node, implication init empty
3 for (const [a, b] of clauses) { // init clause init count implication edge
4 g[a ^ 1].push(b); // ¬a → b
5 g[b ^ 1].push(a); // ¬b → a
6 }
7 const comp = tarjan(2 * n, g); // Tarjan compute SCC( number 7 scc), comp=scc
8 for (let v = 0; v < n; v++) // verdict: x and ¬x scc group ⟺ no solution
9 if (comp[2 * v] === comp[2 * v + 1]) return null;
10 const assign: boolean[] = [];
11 for (let v = 0; v < n; v++) // assign value: take assign literal assign as true
12 assign.push(comp[2 * v] < comp[2 * v + 1]);
13 return assign; // done solution
14}
variable3(A,B,C)
clause(A∨B) ∧ (A∨¬B) ∧ (A∨C) ∧ (¬A∨¬B)
implication edge0 / 8
1 / 16

Complexity and tradeoffs

Time: O(V+E). Space: O(V+E). A formula is impossible exactly when a variable and its negation share one strongly connected component.

Invariant: A partial implication graph represents exactly the clauses already inserted; a variable is contradictory only if both literals enter one SCC.

Where it fits

2-SAT models pairwise choices, scheduling exclusions, orientation constraints, and configuration flags. Clauses with three or more unrestricted literals make the general problem NP-complete.