Hydra

Hydra is the development repository for the Bella knowledge compiler and the Cara #SAT solver.

Supported OS: Linux, macOS (Intel & Apple Silicon), Windows

Bella

A knowledge compiler for:

• (s)d-DNNF circuits,
• wDNNF, pwDNNF, and nwDNNF circuits.

Important

This repository contains the source code. For compiled binaries and the full description, please visit the BellaCompiler repository.

Cara

An isomorphism-aware #SAT solver.

Important

This repository contains the source code. For compiled binaries and the full description, please visit the CaraSolver repository.

Build Instructions

The following tools are required: CMake, Boost, and GMP.

Note

On Windows, Cygwin is needed.

Building Bella

./bella.sh

The compilation takes place in the build_bella directory. The release binary can be found at: build_bella/Release/Bella/

Building Cara

./cara.sh

The compilation takes place in the build_cara directory. The release binary can be found at: build_cara/Release/Cara/

Used software

SAT solver

• MiniSat 2.2.0 (d4 version)
  Hydra/external/satSolvers/MiniSat_d4
• MiniSat 2.2.0
  implemented, not used
  Hydra/external/satSolvers/MiniSat
• CaDiCaL 3.0.0 (TBD)
  Hydra/external/satSolvers/CaDiCaL

Hash map

• unordered_dense v4.5.0
  Hydra/external/hashMaps/unordered_dense
• robin-hood-hashing 3.11.5
  Hydra/external/hashMaps/robin-hood-hashing
• flat_hash_map
  implemented, not used
  Hydra/external/hashMaps/flat_hash_map

Hypergraph partitioning

• PaToH v3.3
  used for Linux, and macOS
  Hydra/external/partitioningHypergraphs/PaToH
• hMETIS 1.5
  used only for Windows
  Hydra/external/partitioningHypergraphs/hMETIS
• KaHyPar v.1.3.3
  Hydra/external/partitioningHypergraphs/KaHyPar

Other

• Boost
  Hydra/external/boost

Papers

If you use Bella for (s)d-DNNF/wDNNF circuits in an academic setting, please cite the following paper describing the knowledge compiler:

@article{Illner_Kucera_2024, 
    author  = {Illner, Petr and Kučera, Petr}, 
    title   = {A Compiler for Weak Decomposable Negation Normal Form}, 
    volume  = {38}, 
    url     = {https://ojs.aaai.org/index.php/AAAI/article/view/28926}, 
    DOI     = {10.1609/aaai.v38i9.28926}, 
    number  = {9}, 
    journal = {Proceedings of the AAAI Conference on Artificial Intelligence},
    year    = {2024}, 
    month   = {Mar.}, 
    pages   = {10562-10570} 
}

If you use Bella for pwDNNF/nwDNNF circuits or Cara in an academic setting, please cite the following paper describing the knowledge compiler and caching scheme:

@article{Illner_2025, 
    author  = {Illner, Petr}, 
    title   = {New Compilation Languages Based on Restricted Weak Decomposability}, 
    volume  = {39}, 
    url     = {https://ojs.aaai.org/index.php/AAAI/article/view/33643}, 
    DOI     = {10.1609/aaai.v39i14.33643}, 
    number  = {14}, 
    journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, 
    year    = {2025}, 
    month   = {Apr.}, 
    pages   = {14987-14996} 
}