Propositional Logic Directed Acyclic Graph (PL‑DAG)

A PL-DAG is a directed acyclic graph where each leaf defines a discrete integer domain (e.g., x ∈ [-5, 3]) and each internal node defines a linear inequality over its predecessors. The graph therefore represents a structured system of discrete constraints, allowing arbitrary compositions of integer ranges and linear relations while naturally sharing repeated sub-expressions.

PL-DAGs are especially well suited for describing and solving discrete optimization problems—problems where you want to make the best possible choice under a set of rules. Typical examples include:

• Choosing the best product configuration given technical constraints

• Optimizing costs or performance while respecting limits

• Selecting combinations of components that must work together

• Modeling resource limits, capacities, or integer-valued decisions

• Exploring what combinations of values are feasible or optimal

Because the PL-DAG breaks everything into small, reusable pieces, it becomes easy to build complex models from simple parts and to solve them with efficient algorithms.

✨ Key Features

Install

1  — Modelling‑only (MIT licence)

cargo add pldag

This pulls no GPL code; you can ship the resulting binary under any licence compatible with MIT.

2  — Modelling + in‑process GLPK solver (GPL v3+ applies)

cargo add pldag --features glpk

Enabling the glpk feature links to the GNU Linear Programming Kit (GLPK). If you distribute a binary built with this feature you must meet the requirements of the GPL‑3.0‑or‑later.

Heads‑up: Leaving the feature off keeps all code MIT‑licensed. The choice is completely under your control at cargo build time.

Core Routines

Analysis & Propagation

propagate

fn propagate<K>(
    &self,
    assignment: impl IntoIterator<Item = (K, Bound)>
) -> Result<Assignment>
where K: ToString;

Propagates bounds bottom‑up through the DAG and returns a map of node → bound ((min, max)).

propagate_default

fn propagate_default(&self) -> Result<Assignment>;

Convenience method that propagates using default bounds of all primitive variables.

Building the Model

Primitive Variables

fn set_primitive(&mut self, id: &str, bound: Bound);
fn set_primitives<K>(&mut self, ids: impl IntoIterator<Item = K>, bound: Bound)
where K: ToString;

Create primitive (leaf) variables with specified bounds. set_primitives creates multiple variables with the same bounds.

Linear Constraints

fn set_gelineq<K>(
    &mut self,
    coefficient_variables: impl IntoIterator<Item = (K, i32)>,
    bias: i32
) -> ID
where K: ToString;

Creates a general linear inequality: sum(coeff_i * var_i) + bias >= 0.

fn set_atleast<K>(&mut self, references: impl IntoIterator<Item = K>, value: i32) -> ID
where K: ToString;

fn set_atmost<K>(&mut self, references: impl IntoIterator<Item = K>, value: i32) -> ID
where K: ToString;

fn set_equal<K, I>(&mut self, references: I, value: i32) -> ID
where K: ToString, I: IntoIterator<Item = K> + Clone;

set_atleast: Creates sum(variables) >= value set_atmost: Creates sum(variables) <= value set_equal: Creates sum(variables) == value

Logical Constraints

fn set_and<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

fn set_or<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

fn set_not<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

fn set_xor<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

fn set_nand<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

fn set_nor<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

fn set_xnor<K>(&mut self, references: impl IntoIterator<Item = K>) -> ID
where K: ToString;

Standard logical operations:

• set_and: ALL variables must be true
• set_or: AT LEAST ONE variable must be true
• set_not: NONE of the variables can be true
• set_xor: EXACTLY ONE variable must be true
• set_nand: NOT ALL variables can be true
• set_nor: NONE of the variables can be true
• set_xnor: EVEN NUMBER of variables must be true (including zero)

fn set_imply<C, Q>(&mut self, condition: C, consequence: Q) -> ID
where C: ToString, Q: ToString;

fn set_equiv<L, R>(&mut self, lhs: L, rhs: R) -> ID
where L: ToString, R: ToString;

set_imply: Creates condition → consequence (implication) set_equiv: Creates lhs ↔ rhs (equivalence/biconditional)

Export & Solving

to_sparse_polyhedron

fn to_sparse_polyhedron(
    &self,
    roots: Vec<ID>,
    double_binding: bool
) -> SparsePolyhedron;

Emits a sparse polyhedral representation suitable for ILP solvers (GLPK, CPLEX, Gurobi, …). SparsePolyhedron implements serde::Serialize, so you can ship it over HTTP to a remote solver service if you prefer.

solve (Optional GLPK Feature)

#[cfg(feature = "glpk")]
fn solve(
    &self,
    roots: Vec<ID>,
    objectives: Vec<HashMap<&str, f64>>,
    assume: HashMap<&str, Bound>,
    maximize: bool
) -> Vec<Option<Assignment>>;

Solves integer linear programming problems using GLPK. Takes multiple objective functions, fixed variable assumptions, and returns optimal assignments.

Quick Example

use indexmap::IndexMap;
use pldag::{Pldag, Bound};

// Build a simple OR‑of‑three model
let mut pldag = Pldag::new();
pldag.set_primitive("x", (0, 1));
pldag.set_primitive("y", (0, 1));
pldag.set_primitive("z", (0, 1));
let root = pldag.set_or(vec!["x", "y", "z"]);

// Validate a combination
let validated = pldag.propagate_default().unwrap();
println!("root bound = {:?}", validated[&root]);

3. Solving with GLPK (Optional Feature)

When the glpk feature is enabled, you can solve optimization problems directly:

#[cfg(feature = "glpk")]
use std::collections::HashMap;
use pldag::{Pldag, Bound};

// Build a simple problem: maximize x + 2y + 3z subject to x ∨ y ∨ z
let mut pldag = Pldag::new();
pldag.set_primitive("x", (0, 1));
pldag.set_primitive("y", (0, 1));
pldag.set_primitive("z", (0, 1));
let root = pldag.set_or(vec!["x", "y", "z"]);

// Set up the objective function: maximize x + 2y + 3z
let mut objective = HashMap::new();
objective.insert("x", 1.0);
objective.insert("y", 2.0);
objective.insert("z", 3.0);

// Constraints: require that the OR constraint is satisfied
let mut assumptions = HashMap::new();
assumptions.insert(&root, (1, 1)); // root must be true

// Solve the optimization problem
let solutions = pldag.solve(vec![root.clone()], vec![objective], assumptions, true);

if let Some(solution) = &solutions[0] {
    println!("Optimal solution found:");
    println!("x = {:?}", solution.get("x"));
    println!("y = {:?}", solution.get("y"));
    println!("z = {:?}", solution.get("z"));
    println!("root = {:?}", solution.get(&root));
} else {
    println!("No feasible solution found");
}

This example demonstrates:

• Problem setup: Creating boolean variables and logical constraints
• Objective function: Defining what to optimize (maximize x + 2y + 3z)
• Assumptions: Fixing certain variables or constraints (root must be true)
• Solving: Using GLPK to find the optimal solution
• Result interpretation: Extracting variable values from the solution

Notes

• All set_* functions accept any iterable type that can be converted to strings via the ToString trait, providing maximum flexibility.

License

• Library code: MIT (permissive).
• Optional solver: If you build with --features glpk, you link against GLPK, which is GPL‑3.0‑or‑later. Distributing such a binary triggers the GPL’s obligations.

You choose the trade‑off: leave the feature off for a fully permissive dependency tree, or enable it for a batteries‑included ILP solver.

Enjoy building and evaluating logical models with PL‑DAG! 🎉