The QBF and SAT Programming Language
Bule helps you to create beautiful CNF and QBF encodings.
The program bule is a sophisticated grounder for the modeling language Bule that support SAT and QBF Solving.
Features
- Grounding with the declarative modelling language Bule
- satisfiability solving - allowing any number of SAT solvers to be called with the grounded CNF formula
- debugging facilities for CNF formulas, statistics on size and quality
- QBF solving
- Various encodings for cardinality constraints and Pseudo Boolean constaints.
- Multiple cardinality encodings
Tutorial
An introduction to the language can be found in this tutorial encoding graph coloring to SAT.
- Syntax Highlighting