Skip to workspace

∴LOGIC LAB

ECS651U / Computability, Complexity & Algorithms / Week 5

Week 5 Interactive notebook

From choices to certificates.

Follow implications in a 2-SAT graph. Build a resolution proof that someone else can check.

x → y
¬y → ¬x

The formula

Example

Edit or enter a CNF

One clause per line

Write !x | y, ¬x ∨ y or NOT x OR y. Lines, ∧, & and AND separate clauses. Blank input is the empty conjunction ⊤ (true); () or □ is the empty clause (false). At most 8 variables and 20 clauses.

Logic Lab · ECS651U Week 5 · Søren Riis and Marc Roth Runs entirely in this browser: no account, network or tracking.

The building blocks

A little logic before you begin

Variable: Takes the value 0 (false) or 1 (true).
Literal: A variable or its negation: x or ¬x.
Clause: An OR of literals. At least one must be true.
CNF: An AND of clauses. Every clause must be true.
SAT / UNSAT: At least one satisfying assignment exists / none exists.
2-CNF: At most two literals in each clause. A unit clause (x) is allowed; it is the same as (x ∨ x).

The empty clause □ has no literals and is false. The empty conjunction ⊤ has no clauses and is true.

Keyboard. Tab moves between controls; Enter or Space activates them. Graph vertices are buttons: activate one to assume that literal is true. In lecture mode, → / PageDown steps forward and ← / PageUp steps back in the current view (graph building, tracing, the reachability table, or worked resolution steps).

Nothing is revealed automatically. Answers, paths, components and worked proof steps appear only when you ask.