Cara

An isomorphism-aware #SAT solver

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

Important

The source code is available in the Hydra repository.

Note

Bella, a knowledge compiler for wDNNF, pwDNNF, nwDNNF and (smooth) decision-DNNF circuits using the same core, is available in the BellaCompiler repository.

🏆 Competition Results

In its debut at the Model Counting Competition 2025 (MCC 2025), Cara achieved:

• 2nd Place (Track 1, Exact Model Counting)
• Best Newcomer Award

To the best of our knowledge, Cara is the first isomorphism-aware #SAT solver to ever participate in the MCC. Significantly, these results were achieved with isomorphism-aware caching enabled. This demonstrates Cara's high competitiveness despite the inherent overhead of this technique, which can be time-consuming on non-symmetric or less symmetric instances.

Running Cara

To run the #SAT solver:

./Cara -h

./Cara < -ph | -ka | -cd > -i input_file -nsm integer (min: 0, max: 10) 
       [ -mmbf positive_integer (default: 1) ] [ -n | -ndc | -nsc ]

Tip

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

Configurations

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

Preprocessing types of Cara caching scheme:
     -n — none (default)
     -ndc — removes duplicate clauses
     -nsc — removes clauses subsumed by others

-nsm — sets the number of sample moments (min: 0, max: 10)
-mmbf — multiplies the model count by this factor (for example, Arjun's "MUST MULTIPLY BY" factor) (default: 1)

Syntax of output

The output follows the format defined by the model counting competition.

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.

CaraTest

./CaraTest

Note

The test takes around 10 minutes.

Used software

SAT solver

• MiniSat 2.2.0 (d4 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 (used only for Windows)
• KaHyPar v.1.3.3

Other

• Boost

Papers

If you use Cara in an academic setting, please cite the following paper, which describes the caching scheme on which Cara is based:

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