CNF and SAT Builder | AI Playgrounds

Propositional sentences (one per line)

Syntax

~ not
& and
| or
-> implies
<-> iff
( ) grouping
Variables: letters/words
# at line start = comment

Examples:

1. Parsed input

Your sentences as parsed by the engine. Errors flagged here.

2. Conjunctive Normal Form (step by step)

Standard rewrite pipeline: eliminate ↔, eliminate →, push ¬ in (De Morgan), distribute ∨ over ∧.

Speed Stage 0

result

Show all five stages at once

3. Satisfiability: exhaustive reference check

Exhaustive enumeration of all 2ⁿ assignments (cap n = 12).

Trace mode:

CDCL mode is a bounded educational first-UIP trace. It shows decisions, propagation, conflicts, learned clauses, and backjumps; production optimizations such as watched literals, restarts, activity heuristics, and clause deletion are intentionally omitted.

Learning rule: start from the false conflict clause and repeatedly resolve on the latest current-level propagated literal until one current-level literal remains (the first UIP). Backjump to the highest decision level among the learned clause's other literals, or level 0 if there is none.

Misread to avoid: a learned clause is a logical consequence of resolution, not a guessed shortcut; a backjump removes assignments above its target level but does not erase earlier decisions.

Speed Step 0

working clause set

4. Entailment by resolution

To prove KB ⊨ α, add ¬α to the knowledge base and apply the resolution rule until you derive the empty clause (contradiction) or stop. AIMA Ch 7.5.

Query α:

🎯 Try these scenarios first

Pick a scenario, predict what should happen, then apply it and compare the result with your prediction.

Scenario 1: Modus ponens: a satisfiable formula

Core question: How can a conclusion be forced even when several truth assignments are possible?

Run and watch: Load the modus-ponens example, convert it to conjunctive normal form (CNF), and inspect the satisfying assignments.

Predict first: Predict which variable must be true in every model.

Explain afterward: Explain how the premises eliminate any assignment where the conclusion is false.

Scenario 2: A biconditional becomes several CNF clauses

Core question: Why can one compact sentence expand into several standardized clauses?

Run and watch: Load the Wumpus breeze rule and step through the rewrite from a biconditional to conjunctive normal form (CNF).

Predict first: Predict which rewrite step will create the largest increase in clauses.

Explain afterward: Explain why the longer form is easier for a general solver to process.

Scenario 3: Graph coloring as a satisfiability problem

Core question: How can a color-choice problem become true-or-false variables?

Run and watch: Load the triangle three-coloring example and inspect the valid assignments.

Predict first: Predict how many colorings remain after adjacent nodes are forced to differ.

Explain afterward: Connect each valid assignment to one legal coloring of the triangle.

Scenario 4: Conflicting XOR constraints create a contradiction

Core question: How can individually reasonable constraints become impossible together?

Run and watch: Load the conflicting XOR constraint set and inspect why every truth-table row fails.

Predict first: Predict whether changing one clause could make the formula satisfiable.

Explain afterward: Identify the exact set of requirements that cannot all be true at once.

Scenario 5: Resolution proves a query by contradiction

Core question: How can proving that the opposite is impossible establish a conclusion?

Run and watch: Use the modus-ponens knowledge base, negate the query, and run resolution until the empty clause appears.

Predict first: Predict what the empty clause means before running the proof.

Explain afterward: Explain why deriving a contradiction shows that the original query follows from the knowledge base.

✨ Featured comparison

Featured comparison

Compare a satisfiable formula with a contradiction. DPLL is not guessing randomly; it is pruning impossible branches.

Apply one scenario that satisfies, then one that forces backtracking or contradiction.

🧭 Visual explanation

Live state to watch

No state captured yet. Run or adjust the applet first.

Misread to avoid

📚 Lesson tour (5 steps)

Step 1/5: -

📝 Worksheet (3 questions)

Q1. Load the Modus ponens example and click Convert. How many satisfying assignments does the SAT enumeration find?

0: the clauses contradict each other, so nothing satisfies them. 1: forcing P=T and Q=T leaves exactly one satisfying row. 4: all four truth-table rows for two variables satisfy it.

Q2. Load the Conflicting XOR (UNSAT) example. How many satisfying assignments?

1: there is always at least one satisfying assignment. 3: the satisfying rows are the ones with an odd number of trues. 0: UNSAT means no assignment satisfies every clause.

Q3. Modus ponens KB. In the query box, type Q and click "Prove by resolution". Does it succeed (empty clause derived)?

Yes: negating Q and resolving derives the empty clause. No: resolution can only check satisfiability, not prove entailment. No: Q does not follow from the knowledge base.

🧪 Quick Assign · QA-SAT-01 · 10–15 min

QA-SAT-01 · Level 1 · 10–15 min
SAT, UNSAT, or entailed?

Convert a knowledge base, inspect DPLL or CDCL evidence, then explain what CNF, learned clauses, and backjumps establish.

Predict

Observe

Explain

Transfer

State snapshot appears here.

♿ Text and keyboard support

Keyboard path

Use Tab and Shift+Tab to move through controls.
Use Enter or Space on buttons, and arrow keys on sliders or select controls.
The visual region is focusable and described by the state summary below.

Text state summary

Reduced motion and non-visual support

Reduced-motion settings are honored where possible. The current state is also available as text, so the main result does not depend only on color, animation, or spatial position.

Accessibility note: this layer gives a text equivalent for the applet state. It does not replace a full human screen-reader audit.

↓ Read the explanation

Propositional logic uses variables that are either true or false and connectives such as NOT, AND, OR, implication, and equivalence. The satisfiability problem, or SAT, asks whether at least one truth assignment makes an entire formula true. This applet shows how formulas are standardized and then searched.

Literal, clause, and CNF

A literal is a variable such as P or its negation ¬P. A clause is an OR of literals. A formula is in conjunctive normal form, or CNF, when it is an AND of clauses. For example, (P ∨ ¬Q) ∧ (R ∨ Q) contains two clauses.

Clause-based SAT solvers operate on CNF or an equivalent clause representation. Higher-level modeling systems may accept richer syntax and compile it into clauses before invoking the core solver. CNF gives algorithms such as DPLL and CDCL a regular structure for unit propagation, conflict analysis, and efficient watched-literal updates.

This applet deliberately shows a direct logically equivalent rewrite so each transformation can be inspected. Production SAT pipelines often introduce auxiliary variables with a Tseitin-style encoding. That produces a compact CNF that is equisatisfiable with the original formula, meaning both are satisfiable or unsatisfiable together, even though they are not identical under every assignment to the added variables.

The five-step equivalent rewrite

Eliminate equivalence: A ↔ B becomes (A → B) ∧ (B → A).
Eliminate implication: A → B becomes ¬A ∨ B.
Push negation inward: use De Morgan's laws and remove double negation.
Distribute OR over AND: A ∨ (B ∧ C) becomes (A ∨ B) ∧ (A ∨ C).
Flatten: read the result as a list of clauses and literals.

Direct distribution can make an equivalent CNF exponentially larger. Practical encodings often use a Tseitin transformation: introduce helper variables to produce a CNF that is linear in size and equisatisfiable with the original formula, although not necessarily logically equivalent over the added variables.

Brute force and structured search

With n variables there are 2ⁿ possible truth assignments. The applet can enumerate small cases so every model is visible. At 30 variables there are more than one billion assignments; at 100 variables there are about 1.27 × 10³⁰. SAT is NP-complete, so no polynomial-time algorithm is known for every instance. Modern solvers are effective on many large structured problems because propagation, learned clauses, restarts, and branching heuristics avoid examining most assignments explicitly.

The Wumpus rule as a bridge

The formula B11 ↔ (P12 ∨ P21) says that there is a breeze at cell (1,1) exactly when at least one adjacent cell contains a pit. A logical agent combines many rules of this kind and asks whether a proposed danger or safety claim follows from the knowledge base. SAT provides one computational route for answering those propositional queries.

What this model leaves out

Production SAT solvers use conflict-driven clause learning, watched literals, preprocessing, restarts, and carefully designed branching heuristics. First-order logic adds variables that range over objects and quantifiers; general first-order validity is undecidable, although theorem provers can establish many useful results. This applet stays with finite propositional formulas so the full assignment space can be inspected.

For teachers

Curriculum: Propositional syntax, logical equivalence, CNF, SAT, satisfiable versus unsatisfiable formulas, model counting, and the limits of brute force.

Pre-exploration prompts:

What is the difference between two formulas being equivalent and merely both being satisfiable?
How does P → Q differ from Q → P?
What does one truth assignment represent?

Post-exploration prompts:

Load modus ponens. Which clauses force Q?
Load an unsatisfiable example and identify the conflict that rules out each branch.
Convert the Wumpus rule. Which rewrite step creates the greatest increase in size?
Explain why a clause-based solver benefits from CNF even though users may write richer syntax.

Misconceptions to test: every formula has one unique CNF; direct distribution is the only practical conversion; SAT solvers simply enumerate all assignments; first-order theorem proving is the same finite problem with different symbols.

命题逻辑使用只能取真或假的变量，以及非、与、或、蕴含和等价等连接词。可满足性问题 SAT 询问：是否至少存在一种真值赋值，使整个公式为真。本工具展示如何先把公式标准化，再进行搜索。

文字、子句与 CNF

文字是变量 P 或其否定 ¬P。子句是若干文字的析取，也就是 OR。一个公式如果是若干子句的合取，也就是 AND，就处于合取范式 CNF。例如 (P ∨ ¬Q) ∧ (R ∨ Q) 包含两个子句。

基于子句的 SAT 求解器在 CNF 或等价的子句表示上运行。更高层建模系统可以接受更丰富的语法，再把它编译成子句后调用核心求解器。CNF 为 DPLL 和 CDCL 等算法提供规则结构，便于执行单元传播、冲突分析和高效的监视文字更新。

本工具故意展示直接的逻辑等价改写，让每一步都可以检查。实际 SAT 流程常用 Tseitin 式编码引入辅助变量，以得到更紧凑的 CNF。这样的 CNF 与原公式是等可满足的，也就是二者会一起可满足或一起不可满足，但对新增变量的每一种赋值并不要求逻辑完全等价。

五步等价改写

消去等价：A ↔ B 改写为 (A → B) ∧ (B → A)。
消去蕴含：A → B 改写为 ¬A ∨ B。
把否定向内推进：使用德摩根律并消去双重否定。
把 OR 对 AND 分配：A ∨ (B ∧ C) 改写为 (A ∨ B) ∧ (A ∨ C)。
展平：把结果读成子句与文字的列表。

直接进行分配可能使逻辑等价的 CNF 指数膨胀。实际编码常使用 Tseitin 变换：引入辅助变量，在线性规模内生成与原公式等可满足的 CNF。加入新变量后，它不必在所有变量上与原公式完全逻辑等价。

穷举与结构化搜索

n 个变量共有 2ⁿ 种真值赋值。本工具可以枚举小型情况，使每个模型都可见。30 个变量已有超过十亿种赋值；100 个变量约有 1.27 × 10³⁰ 种。SAT 是 NP 完全问题，目前没有已知算法能在所有实例上保证多项式时间。现代求解器之所以能处理许多大型结构化问题，是因为传播、学习子句、重启和分支启发式会避免显式检查绝大多数赋值。

用 Wumpus 规则连接知识表示

公式 B11 ↔ (P12 ∨ P21) 表示：格子 (1,1) 有微风，当且仅当相邻格子中至少有一个存在陷阱。逻辑智能体会组合许多这样的规则，并询问某个危险或安全结论是否由知识库推出。SAT 是回答这些命题查询的一种计算方法。

这个模型省略了什么

生产级 SAT 求解器会使用冲突驱动子句学习、监视文字、预处理、重启和精心设计的分支启发式。一阶逻辑还加入了取值于对象的变量和量词；一般的一阶逻辑有效性问题不可判定，不过定理证明器仍能证明许多有用结果。本工具限定在有限命题公式，使学习者可以检查完整赋值空间。

教师指导

课程目标：命题语法、逻辑等价、CNF、SAT、可满足与不可满足公式、模型计数和穷举的限制。

探索前问题：

两个公式逻辑等价，与两个公式都可满足，有什么不同？
P → Q 与 Q → P 有何不同？
一种真值赋值代表什么？

探索后问题：

载入肯定前件。哪些子句迫使 Q 为真？
载入不可满足示例，找出排除每个分支的冲突。
转换 Wumpus 规则。哪一步使公式规模增加最多？
用户可以写更丰富语法时，基于子句的求解器为什么仍受益于 CNF？

需要检验的误解：每个公式只有一个唯一 CNF；直接分配是唯一实用转换；SAT 求解器只会枚举全部赋值；一阶定理证明只是换了符号的有限 SAT。