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
  • Vscode: https://marketplace.visualstudio.com/items?itemName=seanskggo.bule-syntax-highlighting
  • VIM: https://github.com/vale1410/vim-minizinc

Related Tools and Discussions

• https://potassco.org/
• https://pysathq.github.io/
• http://bach.istc.kobe-u.ac.jp/sugar/
• http://picat-lang.org/
• http://www.satlive.org/
• https://accu.org/journals/overload/27/150/horenovsky_2640/
• http://www.cs.utexas.edu/users/vl/tag/SAT-grounders