Skip to content

Add lazy optimized MRV indexing #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
xtraid merged 1 commit into from
Aug 30, 2026
Merged

Add lazy optimized MRV indexing #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ solving remains future work.
| --- | --- |
| Yang–Zhang formula-to-region construction | Implemented and tested |
| Reference serial solver | Implemented |
| Optimized serial path | Implemented with five isolated, measured mechanisms |
| Optimized serial path | Implemented with six isolated, measured mechanisms |
| Independent native verifier | Implemented and required before SAT publication |
| Boolean Z3 oracle | Implemented over the copied immutable `Formula` |
| Wang Z3 oracle | Implemented over copied `Region + TILESET` |
Expand All @@ -81,9 +81,10 @@ solving remains future work.
| `TaskPlan` and native OpenMP solver | Not implemented; only the build scaffold exists |

The optimized path preserves the reference path's Wang semantics and public
contract. Its five retained mechanisms are dynamic DFS storage, omission of
contract. Its six retained mechanisms are dynamic DFS storage, omission of
non-consumable initial-propagation trail entries, SAT-domain ownership
transfer, byte-wise support aggregation, and queue deduplication. The
transfer, byte-wise support aggregation, queue deduplication, and a lazy
private MRV index that preserves the reference path's row-major tie break. The
[optimization methodology](docs/solver_performance_scope.md) defines their
acceptance boundary. Dated reports preserve the measurements and their
host-specific limitations.
Expand Down Expand Up @@ -155,10 +156,11 @@ diagram.

## Next milestones

Planned work remains separated into independently reviewed changes. The new
priority is explainability across the deterministic pipeline:
Planned work remains separated into independently reviewed changes. The next
serial-evidence packets are:

1. resume serial MRV and hard-UNSAT evidence;
1. extend the hard-UNSAT/scaling corpus and record the option matrix now that
the isolated MRV mechanism is measured;
2. define `TaskPlan` only after the serial evidence, then implement and measure
real OpenMP execution.

Expand Down
10 changes: 8 additions & 2 deletions benchmarks/c/bench_solver.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -488,6 +488,8 @@ static bool metrics_equal(
left->support_byte_lookups == right->support_byte_lookups &&
left->support_table_bytes == right->support_table_bytes &&
left->mrv_cells_scanned == right->mrv_cells_scanned &&
left->mrv_index_word_probes == right->mrv_index_word_probes &&
left->mrv_index_bytes == right->mrv_index_bytes &&
left->initial_trail_writes == right->initial_trail_writes &&
left->search_trail_writes == right->search_trail_writes &&
left->initial_trail_rewrites == right->initial_trail_rewrites &&
Expand Down Expand Up @@ -777,7 +779,7 @@ static bool run_benchmark(
);

printf(
"benchmark_version=8 case=%s solver=%s scope=%s expected=%s "
"benchmark_version=9 case=%s solver=%s scope=%s expected=%s "
"iterations=%zu metrics=%u capture_unsat=%u "
"elapsed_ns=%" PRIu64 " ns_per_iteration=%" PRIu64 " "
"process_peak_rss_kib=%ld peak_rss_source=%s "
Expand All @@ -789,6 +791,8 @@ static bool run_benchmark(
"support_byte_lookups=%" PRIu64 " "
"support_table_bytes=%zu "
"mrv_cells_scanned=%" PRIu64 " "
"mrv_index_word_probes=%" PRIu64 " "
"mrv_index_bytes=%zu "
"initial_trail_writes=%" PRIu64 " "
"search_trail_writes=%" PRIu64 " "
"initial_trail_rewrites=%" PRIu64 " "
Expand Down Expand Up @@ -823,6 +827,8 @@ static bool run_benchmark(
reference_metrics.support_byte_lookups,
reference_metrics.support_table_bytes,
reference_metrics.mrv_cells_scanned,
reference_metrics.mrv_index_word_probes,
reference_metrics.mrv_index_bytes,
reference_metrics.initial_trail_writes,
reference_metrics.search_trail_writes,
reference_metrics.initial_trail_rewrites,
Expand Down Expand Up @@ -942,7 +948,7 @@ int main(int argc, char **argv)
print_usage(argv[0]);
return EXIT_FAILURE;
}
printf("benchmark_version=8 ");
printf("benchmark_version=9 ");
#if defined(__clang__)
printf(
"compiler=clang-%d.%d.%d ",
Expand Down
24 changes: 17 additions & 7 deletions docs/serial_solver_implementation_guide.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -294,10 +294,19 @@ domain. Rollback walks entries in reverse to a saved marker and updates
for the same cell are intentional because they reproduce every intermediate
state exactly.

MRV selection scans active cells in row-major order and chooses the smallest
nonsingleton domain. Ties retain the lowest dense index, candidates are tried
in ascending tile-ID order, and propagation visits neighbors in `N`, `E`, `S`,
`W` order. These rules make each path deterministic for a fixed mechanism set.
The reference MRV selection scans active cells in row-major order and chooses
the smallest nonsingleton domain. The optimized path makes the same first
selection linearly, then lazily creates packed membership buckets for domain
sizes 2 through 23 only if search descends below the root. It selects the
smallest nonempty bucket and its lowest dense cell index. Every restriction and
rollback updates this private index while `domains` remains the source of
truth. Root conflicts, complete regions, and searches exhausted at the root
allocate no index.

Both paths therefore retain the lowest dense index on ties. Candidates are
tried in ascending tile-ID order, and propagation visits neighbors in `N`,
`E`, `S`, `W` order. These rules make each path deterministic for a fixed
mechanism set.

DFS uses a heap-allocated stack rather than the process stack. A frame holds
the chosen cell, remaining candidates, and the trail position before the
Expand Down Expand Up @@ -365,6 +374,7 @@ meanings:
| --- | --- |
| `dfs_nodes`, `decisions`, `backtracks`, `failed_leaves`, `max_depth` | Search states, attempted singleton branches, restored failed branches, observed conflicts, and deepest DFS level |
| `domain_reductions`, `propagated_arcs`, `mrv_cells_scanned` | Effective narrowing operations, processed directed neighbor arcs, and active cells inspected by MRV |
| `mrv_index_word_probes`, `mrv_index_bytes` | Packed bucket words inspected by optimized MRV selection and combined bucket/cache storage; zero for the reference path and optimized runs that never build the lazy index |
| `support_tile_visits`, `support_byte_lookups`, `support_table_bytes` | Reference set-tile work, optimized nonzero-byte work, and optimized table storage |
| `initial_trail_writes`, `search_trail_writes` | Undo entries appended in initial propagation and DFS |
| `initial_trail_rewrites`, `search_trail_rewrites` | Repeated entries for a cell within the initial interval or current branch interval |
Expand Down Expand Up @@ -541,9 +551,9 @@ make cachegrind-check
```

The benchmark and profiler paths keep metrics runs separate from timings and
measure MRV scans, queue duplication, trail pressure, domain reductions,
support aggregation, SAT-copy bytes, process peak RSS, and instruction/cache
attribution. Dated reports in the
measure MRV scans and packed-word probes, queue duplication, trail pressure,
domain reductions, support aggregation, SAT-copy bytes, process peak RSS, and
instruction/cache attribution. Dated reports in the
[solver optimization section]({{ '/#solver-optimization' | relative_url }})
record the evidence for each retained optimized mechanism.

Expand Down
Loading