Zelen - Direct MiniZinc Solver backed by Selen

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.

Features

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

Dependencies

Zelen has minimal dependencies:

Installation

As a Binary

Build from source:

git clone https://github.com/radevgit/zelen
cd zelen
cargo build --release

The binary will be at target/release/zelen.

As a Library

Add to your Cargo.toml:

[dependencies]
zelen = "0.5"
selen = "0.15"

Usage

Using as a Library

Parse and solve MiniZinc models from Rust:

use zelen;

fn main() -> 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 model
    let model = zelen::build_model(source)?;
    
    // Solve the model
    let solution = model.solve()?;
    
    println!("Solution found!");
    println!("x = {}", solution.get_int(/* var_id */));
    
    Ok(())
}

Advanced: Access variable information

use zelen::Translator;

fn main() -> 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 source
    let ast = zelen::parse(source)?;
    
    // Translate to model with variable tracking
    let model_data = Translator::translate_with_vars(&ast)?;
    
    // Now we have variable names and IDs
    for (name, var_id) in &model_data.int_vars {
        println!("Variable: {} -> {:?}", name, var_id);
    }
    
    // Solve
    let solution = model_data.model.solve()?;
    
    // Print results with names
    for (name, var_id) in &model_data.int_vars {
        let value = solution.get_int(*var_id);
        println!("{} = {}", name, value);
    }
    
    Ok(())
}

Command Line

# 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 solutions

Command-Line Options

USAGE:
    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

Example: 4-Queens

Model file (queens.mzn):

var 1..4: q1;
var 1..4: q2;
var 1..4: q3;
var 1..4: q4;

constraint q1 != q2;
constraint q1 != q3;
constraint q1 != q4;
constraint q2 != q3;
constraint q2 != q4;
constraint q3 != q4;

constraint q1 + 1 != q2;
constraint q2 + 1 != q3;
constraint q3 + 1 != q4;

solve satisfy;

Run:

./target/release/zelen queens.mzn

Output:

q1 = 2;
q2 = 4;
q3 = 1;
q4 = 3;
----------

Examples

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 operations

See examples/ directory for source code and examples/models/ for test MiniZinc files.

Implementation Status

Completed Features

• ✅ 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}; and var 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

Not Supported / Limitations

• ❌ 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

Architecture

MiniZinc Source → Parser → AST → Translator → Selen Model → Selen Solver → Solution

Components:

• parser.rs - MiniZinc parser (recursive descent)
• translator.rs - Converts AST to Selen model
• main.rs - CLI interface with verbose output

Relationship with Selen

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.

See Also

• Selen - The underlying CSP solver
• MiniZinc - Constraint modeling language

Related Projects

Zelen is part of the open-sourced Nest2D projects collection.