Dissolve (Distributed SAT)

aria.bool.dissolve is a practical implementation of the Dissolve distributed SAT solving framework. It uses asynchronous dilemma-rule splits and clause sharing to parallelise SAT solving across workers.

Directory structure

aria/bool/dissolve/
├── dissolve.py         # Main Dissolve solver class
├── engine.py           # Worker engine logic
├── models.py           # DissolveConfig and DissolveResult data classes
├── scheduler.py        # Work distribution and scheduling
└── ubtree.py           # UBTree-based clause store for subsumption checks

Key classes

  • Dissolve – top-level solver; call solve(cnf) to run

  • DissolveConfig – configuration dataclass controlling solver behaviour:

    • k_split_vars – number of variables used in dilemma splits

    • budget_strategy – "constant" or "luby" sequence

    • distribution_strategy – "dilemma" or "portfolio"

    • clause_sharing – enable / disable cross-worker clause exchange

  • DissolveResult – result container with satisfiability status, model, and runtime

Algorithm overview

  1. Split selection – pick k variables and create dilemma-rule sub-problems that partition the search space.

  2. Worker engines – each worker runs a PySAT-backed CDCL solver on its sub-problem with a configurable budget (constant or Luby).

  3. Clause sharing – learned clauses are shared across workers via a UBTree-based bucket store that supports subsumption checking.

  4. Vote aggregation – variable-picking heuristics aggregate votes from multiple workers to guide branching decisions.

Programmatic usage

from aria.bool.dissolve import Dissolve, DissolveConfig

cfg = DissolveConfig(
    k_split_vars=5,
    budget_strategy="luby",
    distribution_strategy="dilemma",
)
solver = Dissolve(cfg)
result = solver.solve(cnf_clauses)

if result.is_sat:
    print("Model:", result.model)