Byt-Wyze develops deterministic SAT generators, CNF preprocessing tooling, and reproducible research standards for the SAT and formal-methods community.

We make SAT experimentation transparent, auditable, and repeatable — from instance generation to solver preprocessing and model lifting.

Our Principles:

• ✅ Deterministic by design
• ✅ Scientifically rigorous
• ✅ Fully reproducible
• ✅ Open standards, commercial-grade execution

A deterministic, reversible format for recording CNF preprocessing steps

The SAT community needs a standard way to track what solvers do during preprocessing. STTF provides exactly that.

Key Features:

• ✅ Minimal opcode set covering all core CNF transformations
• ✅ Full trace from original CNF → simplified CNF
• ✅ Deterministic reverse-map for lifting solver models
• ✅ Reference replay + validation engine
• ✅ Designed for research, benchmarking, solver development, and competitions

Status: Open specification for community adoption

Use Cases:

• Competition organizers tracking solver behavior
• Researchers validating preprocessing claims
• Solver developers debugging transformations
• Academic reproducibility requirements

🔗 View Repository

Deterministic SAT instance generator with mathematically rigorous hardness control

Generate SAT instances with predictable structural properties using the proprietary CES (Combinatorial Exponential Sequence) framework.

Key Features:

• ✅ Deterministic generation (same seed = same instance)
• ✅ Tunable difficulty parameters
• ✅ Mathematically grounded (not random)
• ✅ DIMACS CNF output format
• ✅ Millisecond generation speed

Pricing:

• Free tier: 100 calls/month
• Pro: $59/mo – 1,000 calls
• Ultra: $299/mo – 10,000 calls

Use Cases:

• Solver benchmarking and testing
• ML training data generation
• Academic research and coursework
• Automated testing pipelines

🔗 Try the API | 📊 See Examples

101 mathematically rigorous SAT instances with full analysis

Free, open-source collection demonstrating what SAT Maker API can produce.

What's Included:

• ✅ 50 SATISFIABLE instances
• ✅ 50 UNSATISFIABLE instances
• ✅ 1 STALL-class instance (extreme difficulty)
• ✅ Interactive HTML viewer
• ✅ Complete solver metrics and analysis
• ✅ 3×3 hardness taxonomy classification

Perfect for:

• Evaluating new SAT solvers
• Educational demonstrations
• Research paper baselines
• Algorithm validation

🔗 View Library

• SAT Maker API v1.0 launched
• SAT Benchmark Instance Library released (101 instances)
• Interactive HTML viewer
• 3×3 hardness taxonomy
• BYT-WYZE™ trademark secured

• STTF v1.0 specification
• STTF OIS registration
• SAT Maker API v2.0

• Deterministic dataset suites
• Additional SAT analysis tools
• Alternative mathematical generation models
• Expanded API ecosystem

We actively seek collaboration with:

🔬 Researchers — reproducible datasets & academic partnerships
⚙️ Solver Developers — STTF integration & benchmarking
🏆 Competition Organizers — deterministic datasets & trace standards
👥 Contributors — tooling, docs & spec improvements

• 📧 info@byt-wyze.com
• 🌐 https://byt-wyze.com
• 💬 Open an issue
• 🤝 Collaborations welcome

• Opaque preprocessing
• Random instances = inconsistent research
• No trace standards
• Static, non-customisable benchmarks

• STTF: transparent preprocessing
• SAT Maker: deterministic generation
• Open standards
• Production APIs

• STTF Specification
• SAT Maker API Docs
• Instance Library Guide
• SAT Competition
• DIMACS Format

General: info@byt-wyze.com
Website: https://byt-wyze.com
API Support: RapidAPI Dashboard
GitHub: https://github.com/Byt-wyze-technology