How do I enter DIMACS CNF?

Begin with p cnf VARIABLES CLAUSES, such as p cnf 2 2. Positive integers mean true variables, negative integers mean negated variables, and each clause ends with 0. For example, 1 2 0 and -1 2 0 require variable 2 to be true. A clause may span lines, and multiple clauses may share a line. Comment lines begin with c. Headers, counts and variable ranges are checked strictly; decimal literals omit leading zeros and plus signs.

How do explicit clause rows differ?

Each nonblank row is one OR clause, with signed nonzero integer literals separated by spaces and no DIMACS terminator. Rows are joined by AND. A lone 0 explicitly represents an empty, false clause. Blank input is an empty conjunction, which is true. Lines beginning with # are comments. Variables run from 1 through the largest referenced number, so use a DIMACS header when you need to declare unused variables.

What are assumptions?

Each optional signed literal becomes an additional unit clause for this run. Assumptions must use the formula's declared or inferred variable range and omit 0 terminators and commas. Contradictory assumptions make the combined formula unsatisfiable. The original formula remains separate in the JSON result, while DIMACS export appends assumptions as unit clauses and updates the header.

What do SAT, UNSAT and UNKNOWN mean?

SAT means the returned complete Boolean assignment was checked against every original clause and assumption. UNSAT means this deterministic DPLL search exhausted its branches and found no assignment for the combined formula. UNKNOWN means search stopped, hit a resource limit or could not run; it makes no satisfiability claim. The first 256 search events form a teaching summary, not a formal proof certificate or minimal unsatisfiable core.

Combined formula and assumptions are limited to 128 KiB of UTF-8 input, 128 variables, 2000 clauses and 20000 literal occurrences. Assumptions count as unit clauses. Each search has a five-second deadline including worker startup and a configurable budget up to 100000 search nodes. Zero nodes deliberately returns UNKNOWN. Large or difficult instances can exceed these limits even when their text is short. The dedicated worker is terminated on stop, input replacement, timeout and navigation.

Are duplicates, tautologies and empty formulas preserved?

Yes. Original clause order, duplicate literals and tautologies remain in the clause review and normalized export. The search may deduplicate literals and skip tautologies because those transformations preserve satisfiability. An empty clause is false and makes the conjunction UNSAT. An empty conjunction is SAT, with an empty witness when no variables are declared. Unneeded declared variables are filled false in a SAT witness.

What do the exports contain?

DIMACS export contains all original literal occurrences in order, plus assumption unit clauses. Result JSON includes the original formula, assumptions, status, complete SAT assignment and clause evaluations when available, search statistics and the bounded step summary. The copyable report states the same current result. Inputs stay in memory and are not uploaded or saved automatically.

Boolean SAT Solver

Enter DIMACS CNF or explicit clause rows, add optional assumptions and run a bounded Boolean satisfiability search. A SAT result includes a complete assignment checked against every original clause and assumption. UNSAT appears only after the search closes every branch; stopping or reaching a limit returns UNKNOWN. Inspect the step summary and original clauses, then export the normalized formula or complete result.

Your CNF workspace

Example input

Input syntaxSearch node budget0 to 100000; time is capped at 5 seconds.

FormulaBegin with p cnf VARIABLES CLAUSES. End every clause with 0. Clauses may span lines. Use c at the start of comment lines.Optional assumptionsEach literal becomes a unit clause. Use variables within the formula's declared or inferred range.

At most 128 variables, 2000 clauses, 20000 literal occurrences and 128 KiB of combined UTF-8 input, including assumptions. Input remains in memory.

Current result and evidence

SAT requires a verified witnessUNSAT requires complete searchUNKNOWN on stop or limit

The example is ready to explore. Enter your own CNF to solve a supplied instance.

Search nodes: 0
Unit propagations: 0
Closed conflicts: 0
Reported elapsed: No result

Finite Boolean satisfiability only, not natural-language, arithmetic or SMT solving. Large instances may exceed the five-second/node budget. A timeout never means unsatisfiable. No minimal unsatisfiable core, optimal assignment or industrial solver performance claim.

Common questions

How do I enter DIMACS CNF?: Begin with p cnf VARIABLES CLAUSES, such as p cnf 2 2. Positive integers mean true variables, negative integers mean negated variables, and each clause ends with 0. For example, 1 2 0 and -1 2 0 require variable 2 to be true. A clause may span lines, and multiple clauses may share a line. Comment lines begin with c. Headers, counts and variable ranges are checked strictly; decimal literals omit leading zeros and plus signs.
How do explicit clause rows differ?: Each nonblank row is one OR clause, with signed nonzero integer literals separated by spaces and no DIMACS terminator. Rows are joined by AND. A lone 0 explicitly represents an empty, false clause. Blank input is an empty conjunction, which is true. Lines beginning with # are comments. Variables run from 1 through the largest referenced number, so use a DIMACS header when you need to declare unused variables.
What are assumptions?: Each optional signed literal becomes an additional unit clause for this run. Assumptions must use the formula's declared or inferred variable range and omit 0 terminators and commas. Contradictory assumptions make the combined formula unsatisfiable. The original formula remains separate in the JSON result, while DIMACS export appends assumptions as unit clauses and updates the header.
What do SAT, UNSAT and UNKNOWN mean?: SAT means the returned complete Boolean assignment was checked against every original clause and assumption. UNSAT means this deterministic DPLL search exhausted its branches and found no assignment for the combined formula. UNKNOWN means search stopped, hit a resource limit or could not run; it makes no satisfiability claim. The first 256 search events form a teaching summary, not a formal proof certificate or minimal unsatisfiable core.
What are the limits?: Combined formula and assumptions are limited to 128 KiB of UTF-8 input, 128 variables, 2000 clauses and 20000 literal occurrences. Assumptions count as unit clauses. Each search has a five-second deadline including worker startup and a configurable budget up to 100000 search nodes. Zero nodes deliberately returns UNKNOWN. Large or difficult instances can exceed these limits even when their text is short. The dedicated worker is terminated on stop, input replacement, timeout and navigation.
Are duplicates, tautologies and empty formulas preserved?: Yes. Original clause order, duplicate literals and tautologies remain in the clause review and normalized export. The search may deduplicate literals and skip tautologies because those transformations preserve satisfiability. An empty clause is false and makes the conjunction UNSAT. An empty conjunction is SAT, with an empty witness when no variables are declared. Unneeded declared variables are filled false in a SAT witness.
What do the exports contain?: DIMACS export contains all original literal occurrences in order, plus assumption unit clauses. Result JSON includes the original formula, assumptions, status, complete SAT assignment and clause evaluations when available, search statistics and the bounded step summary. The copyable report states the same current result. Inputs stay in memory and are not uploaded or saved automatically.