illner/bellacompiler

A knowledge compiler for wDNNF and (s)d-DNNF circuits.

Bella

A knowledge compiler for wDNNF and (s)d-DNNF circuits.

Supported operating systems platforms: Linux, macOS (Apple silicon), and Windows.

⚠️ On Windows, hMETIS is significantly slower since communication via files is used. Therefore, we suggest using KaHyPar (the argument -ka).

Running Bella

To run the knowledge compiler:

./Bella -h

./Bella < -w | -d | -sd > < -ph | -ka | -cd > -i input_file [-c] [-e] [-r] [-s statistics_file] [-o output_file] [-t positive_number] 
        [ -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 | -c_ccs ] [ -n_cccs | -s_cccs | -c_cccs ]
        [ -n_hnw | -s_hnw | -cl_hnw ] [ -a_rhc | iup_rhc | -fs_rhc | -ehc_rhc | -iup_fs_rhc ]

Configurations

Circuit types:
     -w - wDNNF circuit
     -d - d-DNNF circuit
     -sd - sd-DNNF circuit

Partitioning hypergraph types:
     -ph - PaToH (Linux, macOS), hMETIS (Windows)
     -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 (default)
     -c_ccs - Cara

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

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
-e - uses the equivalence simplification method (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 decomposable AND node is specified as follows: A c i₁ i₂ ... i_c

Used software

SAT solver

• MiniSat 2.2.0 (d4 version)
• MiniSat 2.2.0 (implemented, not used)

Hash map

• unordered_dense
• robin-hood-hashing
• flat_hash_map (implemented, not used)

Hypergraph partitioning

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

Other

• Boost

Paper

If you use Bella in an academic setting, please cite the following paper describing the knowledge compiler:

@inproceedings{illner2024compiler,
    title     = {A Compiler for Weak Decomposable Negation Normal Form},
    author    = {Illner, Petr and Ku{\v{c}}era, Petr},
    booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
    volume    = {38},
    number    = {9},
    pages     = {10562--10570},
    year      = {2024}
}