4 releases
Uses new Rust 2024
| 0.1.3 | Feb 6, 2026 |
|---|---|
| 0.1.2 | Jan 21, 2026 |
| 0.1.1 | Jan 12, 2026 |
| 0.1.0 | Jan 12, 2026 |
#2976 in Algorithms
29 downloads per month
Used in 7 crates
(2 directly)
4.5MB
99K
SLoC
oxiz-nlsat
Non-linear arithmetic solver for OxiZ using Cylindrical Algebraic Decomposition (CAD).
Overview
This crate implements the NLSAT algorithm for solving non-linear real arithmetic (QF_NRA) and non-linear integer arithmetic (QF_NIA) problems. NLSAT is one of the most complex components in Z3 (~180k lines of C++).
Supported Logics
- QF_NRA: Quantifier-free non-linear real arithmetic
- QF_NIA: Quantifier-free non-linear integer arithmetic
- QF_NIRA: Combined non-linear integer/real arithmetic
Key Components
| Module | Description | Z3 Reference |
|---|---|---|
solver |
Main NLSAT solver | nlsat_solver.cpp |
types |
Core type definitions | nlsat_types.h |
clause |
Clause representation | nlsat_clause.h |
assignment |
Variable assignments | nlsat_assignment.h |
interval_set |
Solution intervals | nlsat_interval_set.cpp |
explain |
Conflict explanation | nlsat_explain.cpp |
Algorithm Overview
- Variable Ordering: Choose order for CAD projection
- Constraint Propagation: Evaluate constraints under partial assignment
- Conflict Detection: Find conflicting cells in CAD
- Explanation: Generate lemmas for CDCL integration
- Backtracking: Learn from conflicts and continue search
Dependencies
oxiz-math: Polynomial arithmetic, interval operations
References
- Jovanović, D., & de Moura, L. (2012). Solving Non-linear Arithmetic. IJCAR.
- Collins, G. E. (1975). Quantifier elimination for real closed fields by cylindrical algebraic decomposition.
License
Apache-2.0
Dependencies
~20MB
~290K SLoC