Zelen is a MiniZinc parser and solver that directly translates MiniZinc models to the Selen constraint solver, bypassing FlatZinc compilation. It supports a core subset of MiniZinc including constraint satisfaction and optimization problems.
Variable Types:
- Integer variables with domains:
var <min>..<max>: x - Boolean variables:
var bool: b - Float variables:
var float: f - Variable arrays:
array[1..n] of var int: arr - Parameter arrays with initialization:
array[1..5] of int: costs = [10, 20, 30, 40, 50]
Constraints:
- Arithmetic:
+,-,*,/,%(modulo) - Comparison:
=,!=,<,<=,>,>= - Boolean logic:
not,/\(and),\/(or),->(implication),<-> - Global:
all_different,element,cumulative - Aggregation:
min,max,sum - Aggregation:
forall,exists - Nested forall loops:
forall(i, j in 1..n)(constraint)
Solve Types:
- Satisfaction:
solve satisfy; - Minimize:
solve minimize expr; - Maximize:
solve maximize expr;
Input Formats:
- MiniZinc model files (
.mzn) - Optional data files (
.dzn) - merged with model before parsing
Zelen has minimal dependencies:
| Crate | Purpose | Version |
|---|---|---|
| selen | CSP solver backend | 0.14+ |
| clap | CLI argument parsing | 4.5+ |
Build from source:
git clone https://github.com/radevgit/zelen
cd zelen
cargo build --releaseThe binary will be at target/release/zelen.
Add to your Cargo.toml:
[dependencies]
zelen = "0.5"selen = "0.15"Parse and solve MiniZinc models from Rust:
use zelen;fnmain() -> Result<(),Box<dyn std::error::Error>>{let source = r#" var 1..10: x; var 1..10: y; constraint x + y = 15; solve satisfy; "#;// Parse and translate MiniZinc to Selen modellet model = zelen::build_model(source)?;// Solve the modellet solution = model.solve()?;println!("Solution found!");println!("x = {}", solution.get_int(/* var_id */));Ok(())}Advanced: Access variable information
use zelen::Translator;fnmain() -> Result<(),Box<dyn std::error::Error>>{let source = r#" var 1..10: x; var 1..10: y; constraint x + y = 15; solve satisfy; "#;// Parse the sourcelet ast = zelen::parse(source)?;// Translate to model with variable trackinglet model_data = Translator::translate_with_vars(&ast)?;// Now we have variable names and IDsfor(name, var_id)in&model_data.int_vars{println!("Variable: {} -> {:?}", name, var_id);}// Solvelet solution = model_data.model.solve()?;// Print results with namesfor(name, var_id)in&model_data.int_vars{let value = solution.get_int(*var_id);println!("{} = {}", name, value);}Ok(())}# Solve a MiniZinc model
./target/release/zelen examples/models/test_cli.mzn
# Solve with data file
./target/release/zelen examples/models/test_model.mzn examples/models/test_data.dzn
# With options
./target/release/zelen -v -s examples/models/test_cli.mzn # Verbose + statistics
./target/release/zelen -a examples/models/test_cli.mzn # Find all solutionsUSAGE:
zelen [OPTIONS] <MODEL> [DATA]
ARGS:
<MODEL> MiniZinc model file (.mzn)
<DATA> Optional MiniZinc data file (.dzn)
OPTIONS:
-a, --all-solutions Find all solutions (satisfaction problems)
-n, --num-solutions <N> Stop after N solutions
-i, --intermediate Print intermediate solutions (optimization)
-s, --statistics Print solver statistics
-v, --verbose Verbose output with progress
-t, --time <MS> Time limit in milliseconds
--mem-limit <MB> Memory limit in MB
-h, --help Print help information
-V, --version Print version
Model file (queens.mzn):
var1..4: q1;
var1..4: q2;
var1..4: q3;
var1..4: q4;
constraintq1!=q2;
constraintq1!=q3;
constraintq1!=q4;
constraintq2!=q3;
constraintq2!=q4;
constraintq3!=q4;
constraintq1+1!=q2;
constraintq2+1!=q3;
constraintq3+1!=q4;
solvesatisfy;Run:
./target/release/zelen queens.mznOutput:
q1 = 2;
q2 = 4;
q3 = 1;
q4 = 3;
----------
The repository includes runnable examples:
# Run an example program (with --release for better performance)
cargo run --release --example queens4 # 4-Queens solver
cargo run --release --example solve_nqueens # N-Queens solver
cargo run --release --example bool_float_demo # Boolean and float operationsSee examples/ directory for source code and examples/models/ for test MiniZinc files.
- ✅ Variable declarations and arrays
- ✅ Integer, boolean, and float types
- ✅ Arithmetic and comparison operators
- ✅ Boolean logic operators
- ✅ Global constraints:
all_different,element,cumulative - ✅ Aggregates:
min,max,sum - ✅ Forall loops (single and nested generators)
- ✅ Array initialization with literals
- ✅ Modulo operator
- ✅ Satisfy/Minimize/Maximize
- ✅ Multiple input formats (.mzn and .dzn files)
- ✅ Enumerated types:
enum Color = {Red, Green, Blue};andvar Color: x; - ✅ Array2D and Array3D types with proper flattening
- ✅ If-then-else expressions:
if cond then expr1 else expr2 endif - ✅ String concatenation:
++operator - ✅ Include directives:
include "filename.mzn";(parsed but ignored) - ✅ Cumulative constraint:
cumulative(start, duration, height, capacity)for scheduling - ✅ Table constraint:
table(variables, allowed_tuples)for tuple-based constraints
- ❌ Predicate definitions (
predicate name(...) = ...) - ❌ Set operations
- ❌ Complex comprehensions beyond forall
- ❌ Advanced global constraints (circuit, etc.)
- ❌ Search annotations
- ❌ Some output predicates
⚠️ Cumulative: Capacity must be constant (not variable)⚠️ Table: Second argument must be a named parameter array (not inline expressions); 2D parameter arrays limited to array2d() declarations
MiniZinc Source → Parser → AST → Translator → Selen Model → Selen Solver → Solution
Components:
parser.rs- MiniZinc parser (recursive descent)translator.rs- Converts AST to Selen modelmain.rs- CLI interface with verbose output
Zelen uses Selen v0.14+ as its constraint solver backend. Selen provides the core CSP solving engine, while Zelen adds MiniZinc parsing and direct model translation.
Zelen is part of the open-sourced Nest2D projects collection.