SRI-CSL / yices2 / 26936586609

69%

master: 69%

Build Type

push

github

Committed by ahmed-irfan

Commit Message

mcsat: conflict-based schedule for learned-clause reduction

Replace the mcsat bool plugin's clause-database reduction trigger, which
fired on the learned-clause count growing past a size limit, with the
conflict-based sqrt schedule used by the CDCL(T) core (cf. context_solver):
reduce when the conflict count reaches a threshold, then set the next
threshold to conflicts + reduce_interval * sqrt(conflicts), starting at
reduce_init_threshold (300, interval 25).

Conflicts are counted cumulatively (incremented on each MCSAT_SOLVER_CONFLICT
notification), so the count matches the core solver's conflict count; only the
threshold is re-anchored per search at conflicts + reduce_init_threshold. The
gc_round counter is removed; the "keep unsatisfied binary clauses one extra
round" behavior is preserved via a per-GC toggle. The deletion policy itself
(score-based, keep ~half) is unchanged.

Coverage Stats

13 of 13 new or added lines in 1 file covered. (100.0%)

1 existing line in 1 file now uncovered.

87499 of 127181 relevant lines covered (68.8%)

1593884.17 hits per line