SATX is a declarative framework for modeling, analysis, and synthesis using exact SAT and model counting (#SAT) under a unified semantic discipline.
SATX treats satisfiability and model counting as coordinated operators, enabling existence checking, constructive synthesis, and structural analysis of solution spaces and theories.
- Public code version:
SATX 0.4.0 - Specification version:
SATX Specification 1.0
The public repository reflects an evolving implementation. The SATX Specification defines the full conceptual and semantic framework toward which the codebase is converging.
See VERSIONING.md for details.
SATX provides:
- Exact SAT-based decision and synthesis.
- Model counting (#SAT) as a semantic operator, not a probabilistic heuristic.
- Structural analysis via conditional ratios of model counts.
- Explicit modeling and enumeration of complete theories: laws, observers, and trajectories.
SATX is designed for rigorous symbolic reasoning, not statistical inference.
SATX does not rely on:
- Bayesian inference,
- probabilistic learning,
- sampling-based estimation,
- external probability distributions.
All reasoning is logical, structural, and solver-backed.
The following documents define and describe SATX at different levels.
-
SATX Defensive Publication Establishes prior art and defines the semantic scope of SATX.
-
SATX Technical Reference: SAT and #SAT Semantics, API, and Advanced Patterns Full technical documentation: semantics, API, modeling patterns, anti-patterns, and worked examples.
These documents define SATX Specification 1.0 and may describe features not yet fully reflected in the public code.
VERSIONING.md— relationship between code versions and the specificationLICENSE.md— licensing terms (AGPL + commercial)COMMERCIAL.md— commercial licensing optionsNOTICE.md— authorship and attribution
SATX can be applied to:
- formal verification and consistency checking,
- planning and synthesis,
- discrete causal inference,
- identification of dynamical laws,
- observer-dependent analysis,
- formal study of underdetermination and robustness.
SATX is dual-licensed:
- AGPL v3 for open-source use
- Commercial license for proprietary or closed-source applications
See LICENSE.md and COMMERCIAL.md for details.
- Align public code releases with SATX Specification 1.0
- Stabilize APIs toward
v1.0.0 - Expand solver backends and optimization passes
- Extend documentation with additional Transcendental-level examples
SATX is authored and maintained by Oscar Riveros.
If you use SATX in academic or technical work, please cite:
- SATX Specification 1.0
- SATX Defensive Publication
(Full citation details available in the documentation.)
SATX is both:
- a formal semantic framework, and
- an executable symbolic system.
The specification leads; the implementation follows.