SAT + SMT Solver Dashboard

3-SAT → 2-SAT Reducer

Reduction Logs:

Reduced 2-SAT Clauses:

2-SAT Solver

Solver Logs:

Assignment Result (JSON):

CNF Clause Matrix & Implication Graph Visualizer

Click the button below to visualize the 2-SAT input clauses as a clause-literal matrix and an implication graph.

CNF Clause Matrix

Implication Graph

Unit Clause Extractor (1-SAT Mode)

Extracts unit clauses from the 2-SAT assignment and sends them to Tseitin Clause Engine.

Extracted Unit Clauses:

Tseitin Clause Engine (Stepwise Reduction)

Enter clauses (one clause per line, literals space-separated)

Final Transformed Clauses:

Reduction Steps:

Horn-SAT Solver

Horn-SAT Logs:

Horn-SAT Assignment (JSON):

SMT Solver (Z3 Python API)

SMT Logs:

SMT Result (JSON):

Collatz Solver

Collatz Result:

Collatz Induction (Experimental)

Check if Collatz reaches 1 within a bounded number of steps using Z3 SMT.

Start value (n ≥ 10): Max steps (k ≥ 1):

Result:

Goldbach Conjecture SMT Solver

Goldbach SMT Logs:

Result (Primes p1 + p2 = n):