Expand description
§Satisfiability and Optimization Instance Representations
Types representing general satisfiability and optimization instances with functionality to convert them to SAT or MaxSAT instances.
Modules§
- fio
- Module for File IO (Writing and Parsing)
Structs§
- Basic
VarManager - Simple counting variable manager
- Cnf
- Simple type representing a CNF formula. Other than
Instance<VM>, this type only supports clauses and does have an internal variable manager. - Multi
OptInstance multiopt - Type representing a multi-objective optimization instance.
The constraints are represented as a
SatInstancestruct. - Object
VarManager - Manager keeping track of used variables and variables associated with objects
- Objective
optimization - Type representing an optimization objective. This type currently supports soft clauses and soft literals. All objectives are considered minimization objectives.
- OptInstance
optimization - Type representing an optimization instance.
The constraints are represented as a
SatInstancestruct. - Rand
Reind VarManager rand - Manager for randomly re-indexing an instance
- Reindexing
VarManager - Manager for re-indexing an existing instance
- SatInstance
- Type representing a satisfiability instance. Supported constraints are clauses, cardinality constraints and pseudo-boolean constraints.
Traits§
- Manage
Vars - Trait for variable managers keeping track of used variables
- Reindex
Vars - Trait for variable managers re-indexing an existing instance