SRI-CSL / yices2 / 27077160339

69%

push

github

New Mcsat reduce (#639)

* 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.

* mcsat: protect recently used lemma clauses from deletion

Add a CaDiCaL-style "used" counter to the clause tag (cf. smt_core): a
lemma is protected from deletion while its counter is positive. The
counter is set when the lemma is created and re-armed whenever the
lemma is resolved in conflict analysis (as the conflict clause or as a
propagation reason, where the clause score is already bumped). It is
decremented only on reduce GCs -- the ones this plugin scheduled -- not
on GCs triggered for other reasons (e.g. the GC on every pop), so the
protection lasts for actual reduce rounds.

Binary clauses get a counter of 2 (one extra reduce round), which
subsumes the old keep-binary-clauses-every-other-GC heuristic; the
per-GC toggle is removed. The old rule's removal side is preserved: a
binary clause with a satisfied literal gets no protection (GC runs at
base level, so such a clause is permanently satisfied).

Unlike smt_core, fresh lemmas start protected: the bool plugin has no
creation-time score bump, so a new lemma has score 0 and would
otherwise... (continued)

37 of 37 new or added lines in 4 files covered. (100.0%)

88161 of 127736 relevant lines covered (69.02%)

1762375.4 hits per line