https://tyler-ai-logic-solver-sat-smt-dashboard.onrender.com An interactive symbolic reasoning platform built from the ground up using Python, Z3, and Flask — designed to help visualize and understand formal logic, SAT problems, and SMT solving in a creative and educational way.
-
🔁 3-SAT → 2-SAT Clause Reduction
Breaks down 3-literal clauses into logically equivalent 2-literal clauses using symbolic transformations. -
📊 Implication Graph Visualization
Generates directed graphs of variable dependencies for 2-SAT logic using Vis.js. -
⚙️ Tseitin CNF Transformation
Converts logic formulas to conjunctive normal form (CNF) using symbolic auxiliary variables. -
🧠 Z3 SMT Integration
Uses Z3 to reason about boolean satisfiability, symbolic constraints, and halting conditions. -
🤖 Turing Machine Simulation
Encodes and simulates bounded-step Turing Machines to study symbolic halting behavior. -
🧩 Collatz-Inspired Reductions (Tyler's Theory)
Reduces symbolic logic clauses using iterative transformations inspired by the Collatz function. -
🌐 Web Dashboard (Flask + JS)
Full UI for exploring logic, solving, reducing, and visualizing symbolic structures in real-time.
- Backend: Python, Flask, Z3 SMT Solver
- Frontend: HTML, CSS, JavaScript
- Visualization: Vis.js, Canvas/SVG
- Environment: Ubuntu on WSL (Windows Subsystem for Linux)
- Save/load session (JSON/CNF)
- Interactive proof tracing
- Exportable unsat core and CNF logs
- Custom Turing Machine designer
- UI toggles for reduction steps
- QBF (Quantified Boolean Formula) support
Tyler Smith
Self-taught developer, logic engineer, and creative technologist.
🔗 GitHub Profile
This project was designed to serve as a research-grade symbolic reasoning dashboard that helps others explore the bridge between computational logic and interactive visualization.
MIT License