A Karp reduction turns every instance of one problem into an instance of another, in polynomial time, so that the answers agree. Here a 3-CNF formula φ with n clauses becomes a graph G with a triangle per clause and an edge between every pair of complementary literals; the threshold is k = 2n. The page builds G, then walks through both directions of the correctness proof. Everything is live: click a literal to fix its variable, click a vertex to put it into or take it out of S.
-3 is ¬x3; !x3, ~x3, ¬x3 work too, and
∨, |, parentheses are ignored). Lines starting with # are comments.
# φ from the lecture 1 2 -3 -1 3 4 -1 -2 -4 2 3 4 cols 2 assign -1 -2 -3 4
cols c sets how many clause triangles go in one row; assign l₁ l₂ … presets an
assignment as a list of true literals. To place a clause by hand, append @ x y to its line
(grid units: one clause pitch is 1, so @ 0 0, @ 1 0, @ 0.5 1 …).
Limits: 12 clauses, variables x1…x16.
V, then E, then one edge u v per line
(vertices 0 … V−1). Optionally, after the edges, exactly V lines x y with the drawing coordinates
of the vertices (any scale; the picture is fitted to the box). A line S 0 2 3 presets the set S.
Lines starting with # are comments. At most 30 vertices.