A 3-SAT verifier for the unmodified Commodore 64, implementing Coleman Dimensional Encoding (CDE) — a geometric reading of Boolean satisfiability where clauses become hyperplane constraints and variable assignments become points in {0,1}ⁿ. Given a CNF formula and a candidate assignment, ChronoSAT decides satisfaction in O(m·k) time using a sparse 6-bytes-per-clause encoding.
Not a SAT solver. ChronoSAT does not search the 2ⁿ assignment space — that would be P = NP. It verifies a given witness.
The verifier ships twice over identical data: sat-ref?, a readable threaded-Forth
reference, and sat?, a hand-assembled native 6502 kernel. For 2048 variables
× 1024 clauses (satisfiable):
| Verifier | Cycles / run | Wall clock @ 1.023 MHz | Speedup |
|---|---|---|---|
sat-ref? (threaded Forth) |
2,364,678 | 2.31 s | 1.0× |
sat? (native 6502 kernel) |
183,412 | 0.18 s | 12.9× |
Both return the identical SAT/UNSAT flag on every instance (verified by a fuzz
cross-check). Measured cycle-exact with chrono6502, a 6502 core that boots
the real ChronoForth image in-process — validated against hand-derived counts and
VICE. See PERFORMANCE.md for methodology and the cycle budget.
- Clause structure: CNF clause list with variable indices and polarity.
- Assignment state: current partial assignment bitset.
- Implication graph: directed edges between assignments induced by propagation.
- Heuristics: per-variable activity scores and decision levels.
ChronoSAT is optimized for:
- “Given a CNF formula, determine satisfiability and produce a model if one exists.”
- “Given the current assignment, compute unit propagations and detect conflicts.”
- “Given a conflict, produce a learned clause and backtrack level.”
A CDCL solver’s behavior is entirely driven by:
- Clause structure,
- Current assignment,
- Implication graph, and
- Heuristic scores.
This combination is sufficient to answer any query about search progress or satisfiability. Encoding exactly these yields a CDE layout that is MSS for SAT solving.
Coleman Dimensional Encoding reframes SAT verification as polytope membership:
- Clauses become Linear Inequalities: Each clause becomes a constraint
- Assignment becomes Point: Variable assignment is a point in {0,1}^n
- SAT Check becomes Membership: Does the point satisfy all constraints?
Verification is O(m×k) where m=clauses, k=literals per clause.
- Proper 3-SAT with negation support
- Sparse storage (6 bytes per clause)
- Polynomial-time verification, O(m·k)
- Native 6502 kernel — the clause walk hand-assembled through ChronoForth's
built-in
code … end-codeassembler: zero threading overhead, short-circuit clauses, pointer-walked storage, branchless negation (~12.9× the Forth path) - Self-validating: the native kernel is cross-checked against the Forth reference on every run
- SAT and UNSAT detection
- Runs on 1970s hardware
- VICE C64 emulator
- ChronoForth disk image
# Build ChronoForth
cd ../chronoforth
make chronoforth.d64
# Add ChronoSAT to disk
cd ../chronosat
./add-to-disk.sh ../chronoforth/chronoforth.d64
# Run in emulator
x64sc ../chronoforth/chronoforth.d64
```text
### In the Emulator
```forth
INCLUDE CHRONOSAT
DEMO
```text
This runs:
1. **SAT test** - Verifies a satisfying assignment
2. **UNSAT test** - Correctly rejects a broken assignment
## Repository Structure
```text
chronosat/
├── README.md # This file
├── ARCHITECTURE.md # System design
├── PERFORMANCE.md # Complexity analysis
├── PROOF.md # Mathematical proof
├── CDE_VS_DP.md # CDE vs Dynamic Programming
├── src/
│ └── chronosat.fs # Forth implementation
├── paper/
│ └── chronosat-paper.tex # LaTeX paper
└── examples/
└── *.cnf # Example problems
```text
## Documentation
- [ARCHITECTURE.md](ARCHITECTURE.md) - Component design and data flow
- [PERFORMANCE.md](PERFORMANCE.md) - Complexity proofs and benchmarks
- [PROOF.md](PROOF.md) - Complete mathematical explanation
- [CDE_VS_DP.md](CDE_VS_DP.md) - Why CDE is not Dynamic Programming
## The Paper
See `paper/chronosat-paper.tex` for formal mathematical treatment.
```bash
cd paper
pdflatex chronosat-paper.tex
```text
## What CDE Is (and Is Not)
**CDE IS:**
- A geometric interpretation of SAT verification
- Polynomial-time validation of candidate solutions
- A novel perspective on satisfiability
**CDE IS NOT:**
- A polynomial-time SAT solver (that would be P=NP)
- Faster than standard verification asymptotically
- A replacement for DPLL/CDCL solvers
## Contributing
See [CONTRIBUTING.md](CONTRIBUTING.md) for development guidelines.
## License
MIT License - see [LICENSE](LICENSE) for details.
## Author
Jacob Coleman
## Acknowledgments
- Built on [ChronoForth](https://github.com/chronomancy-io/chronoforth)
- Forked from [DurexForth](https://github.com/jkotlinski/durexforth)
---
*Standardized with [chronoboiler](https://github.com/chronomancy-io/chronoboiler) v1.0.0*