Bella

A knowledge compiler for:

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

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

Important

The source code is available in the Hydra repository.

Note

Cara, a #SAT solver using the same core, is available in the CaraSolver repository.

Running Bella

To run the knowledge compiler:

./Bella -h

./Bella -v

./Bella < -w | -pw | -nw | -d | -sd > < -ph | -ka | -cd > -i input_file
        [-c] [-e] [-r] [ -s statistics_file ] [ -o output_file ] [ -t positive_integer (default: 86400) ]
        [ -r_dh | -dlcs_dh | -dlis_dh | -dlcs_dlis_dh | -vsids_dh | -vsads_dh | -jwos_dh | -jwts_dh | -eupc_dh | -aupc_dh ]
        [ -n_ccs | -s_ccs | -h_ccs | -b_ccs | -i_ccs | -c_ccs [integer] (min: 0, max: 10, default: 2) ] [ -n_cccs | -s_cccs | -c_cccs ]
        [ -n_hccs | -s_hccs | -h_hccs | -b_hccs | -c_hccs [integer] (min: 0, max: 10, default: 2) ] [ -n_hcccs | -s_hcccs | -c_hcccs ]
        [ -n_hnw | -s_hnw | -cl_hnw ] [ -a_rhc | -iup_rhc | -fs_rhc | -ehc_rhc | -iup_fs_rhc ]

Tip

On Windows, hMETIS is significantly slower because it communicates via files. Therefore, we suggest using KaHyPar instead.

Configurations

Circuit types:
     -w — wDNNF circuit
     -pw — pwDNNF circuit
     -nw — nwDNNF circuit

     -d — d-DNNF circuit
     -sd — sd-DNNF circuit

Partitioning hypergraph types:
     -ph — PaToH (Linux, macOS), hMETIS (Windows) (recommended)
     -ka — KaHyPar (Linux, macOS, Windows)
     -cd — Cara (Linux, macOS)

Files:
     -i — specifies the CNF file name
     -s — specifies the file name where the statistics will be saved
     -o — specifies the file name where the compiled circuit will be saved

Decision heuristics:
     -r_dh — random
     -dlcs_dh — dynamic largest combined sum (DLCS)
     -dlis_dh — dynamic largest individual sum (DLIS)
     -dlcs_dlis_dh — DLCS + DLIS as a tie-breaker (DLCS-DLIS)
     -vsids_dh — variable state independent decaying sum (VSIDS)
     -vsads_dh — variable state aware decaying sum (VSADS) (default)
     -jwos_dh — Jeroslow-Wang (one-sided)
     -jwts_dh — Jeroslow-Wang (two-sided)
     -eupc_dh — exact unit propagation count (EUPC)
     -aupc_dh — approximate unit propagation count (AUPC)

Component caching schemes:
     -n_ccs — none
     -s_ccs — standard
     -h_ccs — hybrid
     -b_ccs — basic
     -i_ccs — i (default)
     -c_ccs — Cara: optionally sets the number of sample moments (min: 0, max: 10, default: 2)

Component cache cleaning strategies:
     -n_cccs — none
     -s_cccs — sharpSAT
     -c_cccs — Cara (default)

Hypergraph cut caching schemes:
     -n_hccs — none (default)
     -s_hccs — standard
     -h_hccs — hybrid
     -b_hccs — basic
     -c_hccs — Cara: optionally sets the number of sample moments (min: 0, max: 10, default: 2)

Hypergraph cut cache cleaning strategies:
     -n_hcccs — none (default)
     -s_hcccs — sharpSAT
     -c_hcccs — Cara

Hypergraph node weight types:
     -n_hnw — none
     -s_hnw — standard
     -cl_hnw — clause length (default)

Recomputing hypergraph cut types:
     -a_rhc — hypergraph cuts are computed at each node
     -iup_rhc — a new hypergraph cut is computed when immense unit propagation is performed (default)
     -fs_rhc — a new hypergraph cut is computed when the current formula is split
     -ehc_rhc — a new hypergraph cut is computed when the current hypergraph cut is empty
     -iup_fs_rhc — a new hypergraph cut is computed when immense unit propagation is performed, or the current formula is split

-h — help
-c — counts the models
-v — print version information
-e — uses the equivalence simplification method (highly recommended)
-t — sets the compilation timeout (default: 86400 s)
-r — the statistics file is in a form readable by a human

Syntax of circuit files

The file format is the same as defined in the user manual (Section C) of the c2d compiler.

• a weak AND node is specified as follows: B c i₁ i₂ ... i_c
• a positive weak AND node is specified as follows: P c i₁ i₂ ... i_c
• a negative weak AND node is specified as follows: N c i₁ i₂ ... i_c
• a (classical) decomposable AND node is specified as follows: A c i₁ i₂ ... i_c

HydraTest

./HydraTest

Warning

Some tests for caching assume that the type "unsigned long long int" has precisely 64 bits.

Note

The test takes around 10 seconds.

BellaTest

./BellaTest

Note

The test takes around one hour.

Used software

SAT solver

• MiniSat 2.2.0 (d4v2 version)
• MiniSat 2.2.0 (implemented, not used)
• CaDiCaL 3.0.0 (TBD)

Hash map

• unordered_dense v4.5.0
• robin-hood-hashing 3.11.5
• flat_hash_map (implemented, not used)

Hypergraph partitioning

• PaToH v3.3 (used for Linux, and macOS)
• hMETIS 1.5.3 (used only for Windows)
• KaHyPar v.1.3.3

Other

• 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} 
}