Modelling#
The hermax.model module provides Python modelling for MaxSAT
and SAT-like workflows.
The design goal is to let users model naturally while maintaining an efficient
path from high-level objects to exported CNF/WCNF
and incremental solver calls.
Examples#
Start here if you want runnable modelling examples and outputs:
Core Concepts#
- Modelling Overview
- Modeling Internal Overview
- Boolean and PB Modelling
- Conditionals and Implications
- Enum, Int and Intervals
- Enum Variables
- Enum subset membership
- Enum-Enum Comparisons
- Integer Variables
- Bounded Int comparisons
- Performance notes
- Ladder constraints
- Using
IntVarin PB expressions - Piecewise Step Functions as PB
IntVarin objectiveIntVarscaling (multiplication)- Constant division via
// - Lazy array indexing via
@ - Variable index on
IntVector - Intervals
- References
- Vectors, Matrices and Dicts
Solving And Export#
- Solve, Export, and Decode
- Export to CNF / WCNF
- Soft clauses
- Objective replacement
- Lexicographic objective API
- Soft groups and PB constraints
- Integer objective terms
- Decode solver models
- Convenience Solving
- Incremental Defaults
- Assumptions
- Weight Updates
- Floating objective weights
- Hermax solver integration
- Example
- Manual solver roundtrip
- Modelling Tricks