# eenn — Enlightened Equation Neural Network
**A hybrid neural-symbolic constraint solver with cognitive reasoning capabilities.**
[](https://github.com/ciresnave/eenn)
[](https://crates.io/crates/eenn)
> ⚠️ **Status**: Experimental / Research Prototype
> This project is not yet ready for production use. It's a research platform exploring hybrid neural-symbolic constraint solving.
## Overview
eenn is an experimental constraint solver that combines neural network guidance with symbolic reasoning to solve mathematical constraint problems. It features:
- **🧠 Hybrid Architecture**: Neural hints guide symbolic SMT solving
- **⚡ Lightning Strike**: Cognitive reasoning engine with dynamic strategy selection
- **🔢 Advanced Constraint Solving**: Handles linear systems, non-linear equations, and inequality ranges
- **🎯 Smart Features**: Parentheses support, inequality ranges, multi-variable systems
## Quick Start
### Installation
Add to your `Cargo.toml`:
```toml
[dependencies]
eenn = "0.1"
```
Or install the CLI tool:
```bash
cargo install eenn
```
### Basic Usage
```bash
# Solve a simple equation
eenn-solve solve -p "x + y = 10 and x - y = 4"
# Output: x = 7, y = 3
# Non-linear systems
eenn-solve solve -p "x * y = 12 and x + y = 7"
# Output: x = 3, y = 4
# Parentheses support
eenn-solve solve -p "3 * (2 + 5) = 21"
# Output: (solution found)
# Inequality ranges
eenn-solve solve -p "x > 5 and x < 10"
# Output: 5 < x < 10
```
## Features----------------------
### 1. **Parentheses-Aware Expression Parsing**This project uses rkyv for an optional zero-copy serialization path. The rkyv dependency is intentionally pinned to a specific git commit in `Cargo.toml` to ensure reproducible builds and because certain safe archived-access helpers used by the code require features that were not available in earlier published releases
Handles nested expressions with proper operator precedence:If you need to update rkyv, please do so deliberately: pick a released tag or update the `rev` field in `Cargo.toml` to a new commit and re-run the test suite with `--features rkyv` to confirm behavior.
```rustEnabling rkyv and unchecked fast path
// Correctly parses: 3 * (2 + 5) = 21-------------------------------------
// Evaluates inner expression first
```By default rkyv is optional behind the `rkyv` Cargo feature. Enable it with:
### 2. **Non-Linear System Solving**```sh
cargo test --features rkyv
Uses intelligent brute-force search for small integer domains:```
```bashFor trusted inputs there's an additional (unsafe) unchecked zero-copy path exposed behind the `rkyv_unchecked` feature. This skips validation and performs an unchecked archived pointer conversion; only enable it when you fully trust the input bytes (for maximum speed). To run tests with the unchecked path enabled:
eenn-solve solve -p "x * y = 12 and x + y = 7"
# Finds: x = 3, y = 4 (or x = 4, y = 3)```sh
```cargo test --features "rkyv rkyv_unchecked"
```
### 3. **Inequality Range Solutions**
Benchmarking note
Shows solution ranges instead of arbitrary single values:-----------------
```bashThe repository includes a small benchmark/test that compares the validated and unchecked rehydration paths. If you want to measure performance locally, run the bench (or the provided test) and compare timings. Be sure to pin dependencies and use the same CPU frequency/power settings for reproducible numbers.
eenn-solve solve -p "x >= 0 and x <= 100"
# Output: 0 <= x <= 100
eenn-solve solve -p "x > 5 and x <= 15"
# Output: 5 < x <= 15
```
### 4. **Lightning Strike Cognitive Engine**
Dynamic reasoning strategy selection based on problem characteristics:
- **Linear Algebra** for systems of linear equations
- **Symbolic SMT** for complex constraints
- **Neural Guidance** for pattern recognition
- **Brute Force** for small non-linear systems
## Architecture
### Hybrid Reasoning Pipeline
```
┌─────────────────┐
│ User Constraint│
│ Parser │
└────────┬────────┘
│
▼
┌─────────────────┐
│ Lightning │
│ Strike │◄─── Cognitive branch selection
│ Reasoning │
└────────┬────────┘
│
├─► Neural Surrogate (pattern hints)
│
├─► SMT Backend (symbolic solving)
│ ├─► Linear System Solver
│ ├─► Non-Linear Brute Force
│ └─► Inequality Range Detector
│
└─► Hybrid Verification
```
### Key Components
- **`theory_core`**: Core constraint solving logic, SMT backend, Lightning Strike engine
- **`constraint_parser`**: Expression parsing with parentheses support
- **`smt_stub`**: Linear, non-linear, and inequality solvers
- **`lightning_strike`**: Cognitive reasoning and strategy selection
- **`surrogate`**: Neural network guidance (demo implementation)
## Library Usage
### As a Constraint Solver
```rust
use eenn::constraint_parser::parse_constraints;
use theory_core::{SmtBackend, ConstraintSolver};
// Parse constraints
let (constraints, var_map) = parse_constraints("x + y = 10 and x > 5")?;
// Solve
let backend = SmtBackend::new();
let solution = backend.solve(&constraints)?;
// Access results
if solution.satisfiable {
for (var, value) in &solution.assignment {
println!("{} = {}", var, value);
}
// Check for ranges (inequalities)
if let Some(ranges) = &solution.variable_ranges {
for (var, range) in ranges {
println!("{}", range); // e.g., "5 < x"
}
}
}
```
### As a Neural Network Library
eenn also provides basic neural network building blocks:
```rust
use eenn::{FunctionRegistry, Neuron, Stage, relu, scale};
// Create a function registry
let mut registry = FunctionRegistry::empty();
registry.register_fn("relu", relu, "ReLU activation");
// Build a simple neuron
let neuron = Neuron::new(
vec![Stage::new(scale(2.0))],
Stage::new(relu)
);
// Evaluate
let output = neuron.eval(3.0); // = relu(6.0) = 6.0
```
## Command-Line Interface
### eenn-solve
The `eenn-solve` binary provides an interactive constraint solving interface:
```bash
# Basic solving
eenn-solve solve -p "equation"
# Verbose mode (shows strategy and timing)
eenn-solve solve -p "equation" -v
# Interactive mode
eenn-solve solve
```
### Examples
```bash
# Linear systems
eenn-solve solve -p "2*x + 3*y = 13 and x - y = 1"
# Non-linear
eenn-solve solve -p "x^2 = 16"
# Inequalities
eenn-solve solve -p "x >= 10 and x <= 20"
# Complex expressions with parentheses
eenn-solve solve -p "2 * (x + 3) = 10"
```
## Advanced Features
### Zero-Copy Serialization (Optional)
eenn uses `rkyv` for optional zero-copy serialization of neural network architectures:
```toml
[dependencies]
eenn = { version = "0.1", features = ["rkyv"] }
```
```bash
# Run tests with rkyv
cargo test --features rkyv
# Unsafe fast path (trusted inputs only)
cargo test --features "rkyv rkyv_unchecked"
```
**Note**: The `rkyv` dependency is pinned to a specific git commit for reproducibility. Neural network weights use standard `serde` serialization.
### GPU Acceleration (Experimental)
```toml
[dependencies]
eenn = { version = "0.1", features = ["gpu"] }
```
GPU support is experimental and requires WGPU-compatible hardware.
## Known Limitations
1. **Reversed Comparisons**: `5 < x` must be written as `x > 5`
- Parser currently expects variable on the left side
- Workaround: Rewrite constraints in standard form
2. **Non-Linear Complexity**: Brute-force search limited to small domains
- Default range: -20 to 20
- Maximum combinations: 1,000,000
- Use for small integer problems only
3. **Inequality Mixing**: Mixed equality/inequality constraints may not optimize ranges
- Pure inequality constraints → range output
- Mixed constraints → single value from equality solver
## Development
### Building from Source
```bash
# Clone the repository
git clone https://github.com/ciresnave/eenn.git
cd eenn
# Build
cargo build --release
# Run tests
cargo test
# Run with specific features
cargo test --features rkyv
```
### Project Structure
```
eenn/
├── src/
│ ├── lib.rs # Main library
│ ├── constraint_parser.rs # Expression parsing
│ ├── models.rs # Neural network serialization
│ ├── nn.rs # Neural network training
│ └── bin/
│ └── eenn-solve.rs # CLI application
├── crates/
│ ├── theory_core/ # Core constraint solving
│ │ ├── src/
│ │ │ ├── smt_stub.rs # SMT backend
│ │ │ ├── lightning_strike.rs # Cognitive reasoning
│ │ │ ├── surrogate.rs # Neural guidance
│ │ │ └── ir.rs # Constraint IR
│ │ └── Cargo.toml
│ └── lightning_strike/ # Standalone reasoning crate
├── tests/ # Integration tests
├── examples/ # Example programs
└── benches/ # Benchmarks
```
### Running Benchmarks
```bash
cargo bench
```
## Future Directions
**eenn v2** is planned as a complete rewrite built on:
- **Candle**: Modern Rust tensor library
- **llama.cpp**: Efficient LLM inference
- **vLLM**: Production-grade serving
This will enable true neural constraint solving with real language models.
## Contributing
Contributions are welcome! Please:
1. Fork the repository
2. Create a feature branch
3. Add tests for new functionality
4. Submit a pull request
## License
Licensed under either of:
- Apache License, Version 2.0 ([LICENSE-APACHE-2.0](LICENSE-APACHE-2.0) or <http://www.apache.org/licenses/LICENSE-2.0>)
- MIT License ([LICENSE-MIT](LICENSE-MIT) or <http://opensource.org/licenses/MIT>)
at your option.
## Citation
If you use eenn in your research, please cite:
```bibtex
@software{eenn2025,
author = {Evans, Eric},
title = {eenn: Enlightened Equation Neural Network},
year = {2025},
url = {https://github.com/ciresnave/eenn}
}
```
## Acknowledgments
eenn builds on research in:
- Hybrid neural-symbolic reasoning
- SMT solving and constraint satisfaction
- Cognitive architectures for AI
## Contact
- GitHub: <https://github.com/ciresnave/eenn>
- Issues: <https://github.com/ciresnave/eenn/issues>
---
**Status**: Experimental / Research Prototype
This is a research project exploring hybrid neural-symbolic constraint solving. While functional, it is not recommended for production use without thorough testing for your specific use case.