Skip to content

Commit 05f4d8a

Browse files
committed
mcsat: seed first two l2o runs from cache before cold-starting
Change the cold-start cadence so the first two l2o runs after a recache reuse the cached (target/best) assignment as the hill-climbing start, and only every third run cold-starts. Previously the very first l2o run cold-started, discarding the warm cache already populated during search.
1 parent 9156288 commit 05f4d8a

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/mcsat/solver.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1583,8 +1583,8 @@ void mcsat_process_requests(mcsat_solver_t* mcsat) {
15831583
uint32_t recache_count = *mcsat->solver_stats.recaches;
15841584
bool use_l2o = mcsat->ctx->mcsat_options.l2o && (recache_count % 2 == 0);
15851585
if (use_l2o) {
1586-
// vary cache seeding: every 3rd l2o run cold-starts (ignores cached values)
1587-
bool use_cached_values = (recache_count / 2) % 3 != 0;
1586+
// vary cache seeding: use cache for two l2o runs, then every 3rd cold-starts
1587+
bool use_cached_values = (recache_count / 2) % 3 != 2;
15881588
l2o_run(&mcsat->l2o, mcsat->trail, use_cached_values, NULL);
15891589
trail_clear_extra_cache(mcsat->trail, true); // keep best cache and clear target cache
15901590
} else {

0 commit comments

Comments
 (0)