Ganak — Counter architecture

Below is count_loop(), made of two parts: descend by cutting the formula into independent components and deciding a variable in one of them, then ascend by adding and multiplying sub-counts back up the stack. Conflicts short-circuit the descent. We count on ascending, because it's a LOT cheaper (e.g. we don't have to count if there is a conflict!)

flowchart TD
  START(["Counter::count_loop()"]) --> FIND{"Any component left
to process at this level?"}

  FIND -->|"yes"| DESC["Descend (see Flowchart below)
pick a component, look it up in the cache;
on a miss, decide a variable and propagate"]
  FIND -->|"no — all done here"| ASC["Ascend (see flowchart below)
Counter::backtrack(): add up the two branches,
cache the result, multiply it into the parent"]

  DESC --> CONFL{"conflict?"}
  CONFL -->|"no"| FIND
  CONFL -->|"yes"| ANA["conflict analysis:
learn a clause, backjump"]
  ANA --> ASC

  ASC --> EMPTY{"decision stack empty?"}
  EMPTY -->|"no"| FIND
  EMPTY -->|"yes"| DONE(["EXIT — total count"])

  classDef big  fill:#ffffff,stroke:#0e7490,color:#06333d,font-size:14px
  classDef proc fill:#fdecea,stroke:#dc2626,color:#4a1010
  classDef term fill:#e9f7ef,stroke:#16a34a,color:#0d2e1c
  class DESC,ASC big
  class ANA proc
  class DONE,START term

2. Descending: decide, propagate, analyse conflicts

This is the "CDCL" part of the counter, and it is very close to a normal SAT solver: we pick a variable, recursively propagate it, and on a conflict learn a 1UIP clause and do chronological backtracking. The counting-specific parts are that the branch variables are picked only from the current component, and that a conflict zeroes out the count of the branch(es) it's on.

flowchart TD
  IN(["a component was selected"]) --> DECIDE["Counter::decide_lit()
push a new StackLevel"]
  DECIDE --> SCORE["Counter::find_best_branch() → Counter::score_of(v)
over vars of this component:
td_weight+ VSIDS+ frequency in the component"]
  SCORE --> POLAR["Counter::get_polarity(v)
activity-based, if equal, cached "]
  POLAR --> SATQ{"only non-independent
vars left?"}

  SATQ -->|"yes"| SAT["Counter::run_sat_solver()
plain CDCL — existence is enough,
no need to enumerate"]
  SAT --> OUT2(["fold result into the branch"])

  SATQ -->|"no"| PROP{"Counter::propagate()
two-watch BCP"}
  PROP -->|"no conflict"| OUT(["back to component selection"])
  PROP -->|"CONFLICT"| CHRONO{"Counter::chrono_check()
only one literal from
the top level?"}
  CHRONO -->|"yes"| BACKONE["chronological backtrack
one level"] --> PROP

  CHRONO -->|"no"| RESOLVE["Counter::resolve_conflict()"]
  RESOLVE --> ZERO["StackLevel::zero_out_branch_sol()
this branch counts 0"]
  RESOLVE --> UIP["Counter::create_uip_cl()
walk the trail back to the 1-UIP,
bump activities"]
  UIP --> MIN["minimize: clause shrinking,
recursive self-subsumption,
binary-clause minimization"]
  MIN --> LEARN["Counter::add_uip_confl_cl()
attach, compute LBD, store"]
  LEARN --> BJ["Counter::find_backtrack_level_of_learnt()
Counter::go_back_to()"]
  BJ --> R1(["asserting literal set →
propagate again"])
  BJ --> R2(["backtrack — ascend"])
  ZERO --> POLL["invalidate cached counts
below the backjump point"]

  MAINT["periodic maintenance:
Counter::vivify_all() · Counter::subsume_all()
Counter::reduce_db() on the learnt clauses"]
  LEARN -.-> MAINT

  classDef search fill:#fdecea,stroke:#dc2626,color:#4a1010
  classDef math   fill:#e9f7ef,stroke:#16a34a,color:#0d2e1c
  classDef cache  fill:#fff4e5,stroke:#d97706,color:#432b06
  classDef ghost  fill:#f0f0f0,stroke:#999999,color:#333333
  class DECIDE,SCORE,POLAR,SAT,RESOLVE,UIP,MIN,LEARN,BJ,BACKONE search
  class ZERO math
  class POLL cache
  class MAINT ghost
  class IN,OUT,OUT2,R1,R2 math

3. Ascending: components, cache, and the count arithmetic

The counting part, i.e. what makes this a model counter rather than a SAT solver. When counting, independent components MULTIPLY, and the two polarities of a decision variable ADD. Uses a cache to record and look up component's counts, so we don't do double work.

flowchart TD
  A{"CompManager::
find_next_remain_comp_of()"}
  A -->|"stack empty here —
need to split"| B["CompAnalyzer::explore_comp()
BFS over watches and clauses
→ connected components"]
  B --> C["CompAnalyzer::make_comp_from_archetype()
pack vars + clause ids
into a CacheableComp key"]
  C --> D{"cache lookup
CompCache::
find_comp_and_incorporate_cnt()"}

  D -->|"HIT"| E["StackLevel::include_solution()
multiply into the active branch —
never searched again"]
  D -->|"MISS"| F["push the component
onto the component stack"]
  E --> G["sort: biggest component last"]
  F --> G
  G --> A

  A -->|"a component remains"| H(["descend — see section 2"])
  A -->|"none remain,
branch satisfied"| I["StackLevel::include_one_sol()
branch := 1"]

  I --> J
  H -.->|"branch exhausted"| J

  J["Counter::backtrack()"] --> K["StackLevel::total_model_count()
branch[0] + branch[1]"]
  K --> L["CompCache::store_value() into the cache
keyed on this level's component"]
  L --> M["parent StackLevel::include_solution()
← sibling components MULTIPLY"]
  M --> N["pop the level,
advance to the next component"]
  N --> A

  W["Counter::unset_lit(): multiply in a variable's
weight when it leaves the component"]
  W -.-> K

  classDef decomp fill:#f3ebfd,stroke:#7c3aed,color:#2b1250
  classDef cache  fill:#fff4e5,stroke:#d97706,color:#432b06
  classDef math   fill:#e9f7ef,stroke:#16a34a,color:#0d2e1c
  class A,B,C,F,G decomp
  class D,E,L cache
  class I,J,K,M,N,W,H math

Every count is an FF — a CMSat::Field value produced by the FieldGen fg. Integers, rationals, complex rationals, MPFR complex floats, GF(2) parity, and polynomials over a finite field all flow through the exact same + and × above; the engine never knows which.

4. The cache in a bit more detail

flowchart LR
  A["Component
active vars + clause ids"] --> B["CacheableComp<T>
packed representation"]
  B --> B1["HashedComp
probabilistic"]
  B --> B2["DiffPackedComp
exact, difference-packed"]
  B1 --> H
  B2 --> H
  H["MurmurHash3 → bucket,
linear collision chain,
equals() confirms match"]
  H --> E["the entry CacheableComp<T>
with model count & score"]
  E --> R["evicted: delete_some_entries()"]
  E --> D["invalidated: clean_pollutions_involving()
walks descendants on backjump"]

Aspect	Detail
Key	The packed set of still-active variables and clause ids of the component, hashed with MurmurHash3 (128-bit; the low word picks the bucket, the high word discriminates collisions)
Hit	Count is folded immediately into the current branch via `include_solution`; the component is never pushed on the stack.
Miss	Entry is created but not yet inserted into the hash table — only entries that actually have a count get inserted.
Store	In `backtrack()`, after both branches of the level are done and before the level is popped.
Invalidate	On backjump or a flipped decision literal, every descendant entry of the popped level is purged.

1. The main loop

2. Descending: decide, propagate, analyse conflicts

3. Ascending: components, cache, and the count arithmetic

4. The cache in a bit more detail