diff --git a/MODIFICATIONS.md b/MODIFICATIONS.md index 831e8251..48b8c80f 100644 --- a/MODIFICATIONS.md +++ b/MODIFICATIONS.md @@ -34,6 +34,7 @@ New code, not derived from MaxCDCL. | Stern / Dumer collision mode of the shared finder (GH-146; `-ub-isd=off\|stern\|dumer[:P,L,W,B,R]`, default stern since 2026-10-23, PI; `-ub-isd=off` = previous finder, GH-140) | Applies to the CC `-ub-search` finder and to the MaxSAT `-ub-pre` pre-pass (both use `UbFinder`). Per round: W Canteaut-Chabaud pivot swaps on the stored systematic columns (or a fresh elimination), a random split of the information set into two halves and a random window of L reduced rows; all subsets of size <= P of each half (`dumer`: the window pivot columns are elements too), bucketed by the window part of their column sum; every colliding pair with different detector parities is weighed, kept words go through the unchanged detector check, stabilizer local improvement and the driver's / pre-pass's independent verification. Single systematic words are also tried every round. Defaults from S0: P 2, L automatic (about log2 of the list size), W 32, B 1 round per iteration. `-ub-isd=off` = the GH-140 enumeration byte for byte (identical to GH-144's 6d2b7a1 on tier0+1). Soundness below (GH-146). See `optimization/experiments/GH-146/`. | | Tanner-graph automorphism candidates for the CC engine (GH-152; `-cc-aut=on\|off`, default on since 2026-10-28, PI decision; `-cc-aut=off` = previous CC search; experimental) | CC wrapper `min_distance_css_cc` only. With `-cc-aut=on`, `distcc::find_row_automorphisms` (`src/cc/cc_aut.{h,cc}`) proposes colour-preserving automorphisms of the Tanner graph (qubits, Hx rows, Hz rows) and one map exchanging the Hx and Hz rows. The generators are tried as extra candidates in `find_half_symmetry` after the GH-75 family, under the same two GF(2) checks (new optional arguments, default = old behaviour). The swap map is offered to `verify_dual_perm` (new, the `find_dual_maps` check for one map) only when `find_dual_maps` finds no map. `-v` prints `c cc aut:` lines. With `-cc-aut=off` no line of any log changes (identity verified on tier0+1, both engines); since the default flip (2026-10-28) the default MaxSAT path is still byte-identical, and the default CC path equals `-cc-aut=on`. Test mutants 13/14 (candidates or the swap map used without the GF(2) check). The MaxSAT path is unchanged. Soundness below (GH-152). See `optimization/experiments/GH-152/`. | | Stabilizer-overlap dominance constraints in the MaxSAT split (GH-148; `-stab-overlap=off\|on\|auto`, default auto since the PI's adoption decision; `-stab-overlap=off` = previous search; silently off with -joint/-roundingsat unless given explicitly) | Split MaxSAT path only (an explicit `-stab-overlap=on\|auto` is refused with -joint/-roundingsat/-engine=cc). For every CSS half, the rows g of the same-type stabilizer matrix (X half: Hx; Z half: Hz) that pass a GF(2) check Hpar g = 0 and Glog g = 0 on the input matrices (duplicates removed) give the constraint "at most floor(\|g\|/2) of the qubits of g are 1" in each probe: by default (`-stab-overlap-enc=native`) as a native propagator inside MaxCDCL (`Solver::setOverlapRows`, set by `run_css_half` after `build_css_half`; see the `Solver.h` / `Solver.cc` section), or as clauses (`add_overlap_constraints` at the end of `build_css_half`): `clauses` = binomial clauses for \|g\| <= 9 and Sinz's sequential counter above, `bin` / `seq` = one of them for every row. `on`: every verified row in every probe; `auto`: row g only in probes of cap c >= 2 (floor(\|g\|/2) + 1) (`-stab-overlap-ratio=X` sets the factor). With `-stab-overlap=off` the instance and the `-v` log are those of the search before the adoption byte for byte (main e52d15b; identity verified on tier0+1 x 2 modes). Soundness below (GH-148). See `optimization/experiments/GH-148/`. | +| Dense overlap rows dropped from cap 16 on (GH-218; `-stab-overlap-c4=N\|off` default 11, `-stab-overlap-pilot=N` default 0, `-stab-overlap-pilot-cap=P` default 12; `-stab-overlap-c4=off` = GH-148's search byte for byte) | Split MaxSAT path, with `-stab-overlap=on\|auto`. Rows on more than N Tanner 4-cycles of the stabilizer matrix (every weight-9 TN row; no BB/LP/GB row) are used as in GH-148 until a half's first probe with cap >= P' + 4 (P' = max(P, lb, activation cap); 16 on the TN codes) and dropped from there on; opt-in `-stab-overlap-pilot=N` > 0 decides per half by a pilot instead ("weight <= P'?" with and without them, N seeds, keep iff the median conflict ratio is <= 1). Sparse rows always as in GH-148. Removes the TN_216 regression of GH-148 (Z half). Soundness below (GH-218). See `optimization/experiments/GH-218/`. | | CC engine switch (GH-124 S0, experimental) | `-engine=maxsat` (default) leaves the search above unchanged (byte-identical `-v` logs); `-engine=cc` runs the connected-cluster level search of `src/cc/` on the same CSS split through the same pipe protocol and output; `-engine=auto` is a structural selector (not the default): CC unless a half's parity matrix has a row of weight > 32 or, for n >= 64, a mean row weight > n/4 (pre-S1 rule; every bundled code goes to CC). `-seed=N` (timing seeds): N > 0 sets `random_seed` of every MaxCDCL solver on the MaxSAT path from the application layer (the engine source is unchanged; N = 0 or no flag keeps main's search byte for byte) and equals `-cc-seed=N` with the CC engine. A CC no-answer stop sends `RESULT -1 TRAP` on the pipe, and the parent withdraws the bounds it had received (MaxSAT never sends it). `find_dual_maps` additionally keeps the verified qubit maps (its report output is unchanged). Flags: `-seed`, `-cc-rules`, `-cc-dual`, `-ub-basis`, `-ub-search` and `-cc-ub-*` (GH-140), `-cc-seed`, `-cc-trace`, `-cc-stats`, `-cc-mutant` and `-cc-schedule` (tests only). Conflicting combinations are rejected (exit 1): CC flags without `-engine=cc\|auto`; `-joint`, `-roundingsat`, the dumps and `-native-parity-opb` with `-engine=cc\|auto`; the cardinality flags and `-dualshare-stats` with `-engine=cc` (`-engine=auto` warns about the flags its choice ignores). See `optimization/experiments/GH-124/`. | ### `src/cc/` (GH-124, experimental; new code, not derived from MaxCDCL or any third-party code) @@ -570,6 +571,29 @@ d = 3..5: RESULT = enumeration, every UB >= d, LBs monotone <= d; test mutants ( and 2 (the half's parity rows used as g without the GF(2) check) must give wrong answers. `make test-cc-flags`: values, conflicts, `-v` lines, no output with the flag off. *Evidence.* `optimization/experiments/GH-148/REPORT.md`. +GH-218 (`-stab-overlap-c4=N|off`, `-stab-overlap-pilot=N`, `-stab-overlap-pilot-cap=P`, split MaxSAT path, +`src/core/distqldpc.cc`; defaults 11 / 0 / 12; `-stab-overlap-c4=off` = GH-148's search byte for byte). *What it +changes.* Which of GH-148's verified rows a probe carries. A row g is *dense* if it lies on more than N Tanner 4-cycles +of the same-type stabilizer matrix, c4(g) = sum over the other distinct rows g' of C(|g & g'|, 2). Sparse rows are used +exactly as in GH-148. The dense rows of a half are used as in GH-148 until the half's first probe whose cap is at least +P' + 4, where P' = max(P, the half's lb, the cap from which the -stab-overlap ratio activates every dense row), and are +dropped from that probe on. With `-stab-overlap-pilot=N` > 0 (opt-in) a pilot runs instead, once per half, the probe +"weight <= P'?" (stop at the first solution) with and without the dense rows for N solver seeds (the run's seed + 0, 1, +...), and keeps the dense rows for the rest of the half iff the median of conflicts(with) / conflicts(without) is <= 1. +*Why every probe +answer stays the same.* GH-148's argument holds for any subset of the verified rows (see GH-148 above: each row alone +keeps every minimum-weight element of F_h, so FOUND / NONE / OPT are unchanged and every returned solution is an +element of F_h); the gate only chooses a subset per half and probe (from the 4-cycle counts, the probe's cap, the half's +lb and, with the pilot, conflict counts), and any choice is sound. The pilot probes' own answers are not used: they only +decide. The choice is a deterministic function of the matrices, the flags and the seed. *Tests.* `make test-cc` Part G: five +more driver configurations with dense rows under the pilot (margin and pilot cap lowered by a test-only knob so that +the pilot runs on the small Part B codes; also pilot off and one seed); Part G (c): the selection of sparse rows equals +a brute-force 4-cycle count on every tier0 code and the tier2 / tier4 TN codes for 7 values of N, the dense flags +partition the verified rows, forced with / without dense rows the probe answers agree at caps d - 1 and d on the tier0 +TN halves, and pilot decisions are reproducible; test mutant 3 (overlaps counted instead of qubit pairs) changes +selections and is caught. `make test-cc-flags`: values, conflicts, `-v` lines; on TN_108_2_12 with `-ub-pre=off` (caps up to 16) a +`c OVERLAP-DROP X cap 16` line by default and a pilot line with `-stab-overlap-pilot=3`; with `-ub-pre` no line. *Evidence.* `optimization/experiments/GH-218/` and the PR for issue #218. + Fix round 1 (S0a): the S0 spec's literal mutants 3 ("orbit seeds without forbidding earlier orbits") and 4 ("stop rule without checking the other half's lower bound") are equivalent mutants as built: the first only drops a restriction, so every level verdict stays exact; the second skips a check that the lockstep pick order (lowest @@ -647,6 +671,9 @@ not a change to MaxSAT costs or quantum-code distance semantics. See limit a conflict clause (p's literal and lim other true qubits of the row, all false) is returned; at the limit every unassigned qubit of the row is enqueued false with the reason clause OR ~x over the lim true qubits and the implied one (implied literal at position 0) +- `ovHas` / `ovWatched(p)` (GH-218): the two call sites of `ovPropagate` first test inline that p sets a qubit + variable on at least one row true (the only case in which `ovPropagate` does anything), so the propagation is the + same and literals that cannot tighten a row no longer pay a call - `ovClause(r, mask, impliedPos)`: reason/conflict clauses (OR of ~x over a (lim+1)-subset of row r) are allocated on first use with `ca.alloc(lits, false)` and cached by (row, subset) in an open-addressing table; they belong to no clause list and are never watched; a cached clause is reordered when it becomes a reason diff --git a/README.md b/README.md index 38dc7281..c494e6ee 100644 --- a/README.md +++ b/README.md @@ -157,6 +157,7 @@ The distance definition, Pauli weight and output format are unchanged. | `-ub-pre=off\|on\|S` | **(GH-144; default `on` = 60 s since 2026-10-23; `-ub-pre=off` restores the previous search)** MaxSAT split only: before the bound search, run the randomized low-weight logical finder of GH-140 on both halves for at most S seconds (each half stops earlier after 16 re-hits of its bound or a plateau of max(1000, 4 x the iteration of its last improvement) iterations; tuning `-ub-pre-hits=H`, `-ub-pre-plateau=P`). The lightest verified word weight U0 is printed as the first `c d_ub`; the doubling probes stop below U0 - 1 and the rest of the search only proves that no logical of weight <= U - 1 exists (probes at U - 1). Every word is checked against the half instance before use; `-seed=N` also seeds the finder. Cost: <= 0.3 s on tiers 1-4, U0 = d on every bundled code with a known distance | | `-ub-isd=off\|stern\|dumer[:P,L,W,B,R]` | **(GH-146; default `stern` since 2026-10-23; `-ub-isd=off` restores the previous finder, the GH-140 enumeration)** Collision mode of the randomized finder used by `-ub-search` (CC) and `-ub-pre` (MaxSAT): a Stern step instead of the 1-2-row enumeration. The information set of each random systematic form is split at random into two halves; all subsets of size <= P of each half are bucketed by the sum of their columns on L random redundancy rows, and every colliding pair whose detector parities differ is weighed (words with up to 2P ones on the information set and none on the window). `dumer` also lets the window coordinates take part in the subsets. Between rounds, W Canteaut-Chabaud pivot swaps re-randomise the information set (0: a fresh elimination); B rounds form one finder iteration; R > 0 forces a fresh elimination every R rounds. Defaults P 2, L automatic (about log2 of the list size), W 32, B 1, R 0. Needs `-ub-search=on\|budget:S` or `-ub-pre=S`; every word is still verified before use | | `-stab-overlap=off\|on\|auto` | **(GH-148; default `auto` since the PI's adoption decision; `-stab-overlap=off` restores the previous search; silently off with `-joint` / `-roundingsat` unless given explicitly)** MaxSAT split only: every probe of a half also requires that at most floor(\|g\|/2) qubits of each same-type stabilizer row g are 1 (rows verified with H g = 0 and G g = 0; a minimum-weight logical always satisfies this, otherwise x + g would be lighter, so no probe answer changes). `on`: all rows in every probe; `auto`: row g only in probes with cap >= 2 (floor(\|g\|/2) + 1) (factor `-stab-overlap-ratio=X`); encoding `-stab-overlap-enc=native\|clauses\|bin\|seq` (default `native`: an "at most k" propagator inside MaxCDCL with lazily created reason clauses; `clauses`: binomial clauses up to \|g\| = 9, sequential counter above). `-frontier-stats` adds a `c OVERLAP` line per probe with the native propagator. `-v` prints the rows used per half and the active rows per probe | +| `-stab-overlap-c4=N\|off`, `-stab-overlap-pilot=N`, `-stab-overlap-pilot-cap=P` | **(GH-218; defaults 11, 0, 12; `-stab-overlap-c4=off` restores GH-148's search)** With `-stab-overlap`: rows g on more than N Tanner 4-cycles of the stabilizer matrix (sum over the other rows g' of C(\|g & g'\|, 2); every weight-9 TN row, no BB/LP/GB row) are *dense*. They are used as in GH-148 until a half's first probe with cap >= P' + 4 (P' = max(P, lb, the cap from which the ratio activates every dense row); 16 on the TN codes) and dropped from there on. With `-stab-overlap-pilot=N` > 0 (opt-in) a pilot instead runs "weight <= P'?" with and without the dense rows for N seeds and keeps them iff the median conflict ratio is <= 1. Any row subset is sound, so no answer changes. `-v` / `-frontier-stats` print the decision (`c stab-overlap ... dropped`, `c OVERLAP-DROP`; with a pilot `c stab-overlap pilot`, `c OVERLAP-PILOT`) | | `-cc-rules=excl,pack,orbf,parity,leaf,overlap,charge[,tiebreak][,sparse,sparseov,sparsemrv,xorunit][,mrv]` | **(experimental)** CC pruning rules (default `excl,pack,orbf,parity,leaf,overlap,charge` since GH-157; `none` = plain CC; `excl,pack,orbf` = the GH-124 engine, `excl,pack,orbf,parity,leaf` = the GH-133 engine, `excl,pack,orbf,parity,leaf,overlap` = the engine before GH-157): sibling exclusion, disjoint odd-row packing bound, orbit seeds from the verified per-half automorphisms, even-weight parity shortcut (GH-133), leaf hash lookup (GH-133), stabilizer-overlap rule (GH-138: a minimum logical meets every same-type stabilizer row g in at most floor(\|g\|/2) qubits; the rest of a row that reaches this limit is forbidden), `charge` (GH-157: fractional LP-dual charge node lower bound on the qubits still needed; evaluated at remaining budget >= `-cc-lb-minr=K` (default 3) where the packing is exactly at its limit (`-cc-lb-gap=G`, default 0), switched off per half by `-cc-lb-auto=P` (default 40: after a level with >= 100 000 evaluations of which < P % pruned); `-cc-lb-raise=off` drops the charge's raise step), `tiebreak` (GH-162, opt-in, needs `overlap`: for an even row g the tie \|e & g\| = \|g\|/2 is cut unless the first qubit of g lies in e, in a per-seed order that puts the seed first, then the earlier orbits, then descending label; sound because the lexicographically least minimum logical in that order has no such tie and is reached by the seed rule; the first(g) tie-break idea is from Qubitserf 04b9349, S. Cercelescu, MIT), fewest-candidate branching. GH-181, opt-in: `sparse` adds redundant parity rows (sums of two parity rows that are no heavier than the heavier of the two; every logical satisfies them) to the packing bound, scanned lightest first; `sparseov` adds such sums of two stabilizer rows to the overlap rule; `sparsemrv` uses fewest-candidate branching over the parity and redundant rows on halves where `sparse` added rows (together with `mrv` it adds nothing: `mrv` already branches that way on every half); `xorunit` forbids the last free qubit of an even row and branches first on an odd row with one free qubit (not recommended: few nodes saved, slower). Rows are added only on TN_200, TN_250, TN_496 and a few tier-0 codes; the tokens combine with `charge`, `tiebreak` and every `-cc-roworder`; the idea of redundant pair-XOR checks is from Qubitserf 04b9349 (S. Cercelescu, MIT) | | `-cc-dual=on\|off` | **(experimental)** With a verified XZ-dual map, CC searches only the X half (default `on`; `-dualmode=off` also disables it) | | `-cc-aut=on\|off` | **(experimental, GH-152; default `on` since 2026-10-28, PI; `-cc-aut=off` restores the previous CC search)** CC engine only. Tanner-graph automorphism candidates: individualisation-refinement on the coloured Tanner graph (qubits, Hx rows, Hz rows) proposes extra qubit permutations for the orbit seeds and one map exchanging Hx and Hz for the single-half search. Every candidate must pass the same GF(2) checks as the built-in family before it is used. Gives orbit seeds on TN codes the built-in family misses (e.g. TN_288/324/432/540/576, TN_200, TN_250) and a dual map on the LP codes and TN_496; on every other bundled code the CC search is unchanged (identical node counts). Detection takes at most 11 ms. The MaxSAT path never uses it | diff --git a/optimization/experiments/GH-218/T0/identity_tiers0-4.txt b/optimization/experiments/GH-218/T0/identity_tiers0-4.txt new file mode 100644 index 00000000..f6653fc1 --- /dev/null +++ b/optimization/experiments/GH-218/T0/identity_tiers0-4.txt @@ -0,0 +1,53 @@ +# main = frozen 02879a93; cand = 60fec5b default (tiers 0-3 first pass, -cpu-lim=600) and 66dc5b6 default (TN_250 and the LP_714 reruns); c4off = -stab-overlap-c4=off. +# 'same' = byte-identical stdout and identical per-probe FRONTIER/OVERLAP lines (-frontier-stats). The two LP_714 DIFF lines of the first pass are +# -cpu-lim=600 timeouts of main at the limit; the reruns at -cpu-lim=3000 (lines after them) are identical in both modes. +BB_108_8_10 -no-card answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +BB_108_8_10 -card-mto answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +BB_144_12_12 -no-card answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +BB_144_12_12 -card-mto answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +BB_72_12_6 -no-card answer[o 6 want 6] stdout cand:same c4off:same probes cand:same c4off:same +BB_72_12_6 -card-mto answer[o 6 want 6] stdout cand:same c4off:same probes cand:same c4off:same +BB_90_8_10 -no-card answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +BB_90_8_10 -card-mto answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +GB_144_12_8 -no-card answer[o 8 want 8] stdout cand:same c4off:same probes cand:same c4off:same +GB_144_12_8 -card-mto answer[o 8 want 8] stdout cand:same c4off:same probes cand:same c4off:same +LP_136_32_4 -no-card answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +LP_136_32_4 -card-mto answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +LP_238_44_6 -no-card answer[o 6 want 6] stdout cand:same c4off:same probes cand:same c4off:same +LP_238_44_6 -card-mto answer[o 6 want 6] stdout cand:same c4off:same probes cand:same c4off:same +LP_34_20_2 -no-card answer[o 2 want 2] stdout cand:same c4off:same probes cand:same c4off:same +LP_34_20_2 -card-mto answer[o 2 want 2] stdout cand:same c4off:same probes cand:same c4off:same +TN_36_8_3 -no-card answer[o 3 want 3] stdout cand:same c4off:same probes cand:same c4off:same +TN_36_8_3 -card-mto answer[o 3 want 3] stdout cand:same c4off:same probes cand:same c4off:same +TN_36_8_4 -no-card answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +TN_36_8_4 -card-mto answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +TN_54_11_4 -no-card answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +TN_54_11_4 -card-mto answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +TN_72_14_4 -no-card answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +TN_72_14_4 -card-mto answer[o 4 want 4] stdout cand:same c4off:same probes cand:same c4off:same +TN_72_8_8 -no-card answer[o 8 want 8] stdout cand:same c4off:same probes cand:same c4off:same +TN_72_8_8 -card-mto answer[o 8 want 8] stdout cand:same c4off:same probes cand:same c4off:same +LP_340_56_8 -no-card answer[o 8 want 8] stdout cand:same c4off:same probes cand:same c4off:same +LP_340_56_8 -card-mto answer[o 8 want 8] stdout cand:same c4off:same probes cand:same c4off:same +LP_442_68_10 -no-card answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +LP_442_68_10 -card-mto answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +BB_144_14_14 -no-card answer[o 14 want 14] stdout cand:same c4off:same probes cand:same c4off:same +BB_144_14_14 -card-mto answer[o 14 want 14] stdout cand:same c4off:same probes cand:same c4off:same +BB_288_12_18 -no-card answer[o 18 want 18] stdout cand:same c4off:same probes cand:same c4off:same +BB_288_12_18 -card-mto answer[o 18 want 18] stdout cand:same c4off:same probes cand:same c4off:same +GB_144_12_12 -no-card answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +GB_144_12_12 -card-mto answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +LP_544_80_12 -no-card answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +LP_544_80_12 -card-mto answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +TN_108_2_12 -no-card answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +TN_108_2_12 -card-mto answer[o 12 want 12] stdout cand:same c4off:same probes cand:same c4off:same +TN_200_10_10 -no-card answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +TN_200_10_10 -card-mto answer[o 10 want 10] stdout cand:same c4off:same probes cand:same c4off:same +LP_714_100_16 -no-card answer[o 16 want 16] stdout cand:DIFF c4off:DIFF probes cand:DIFF c4off:DIFF +LP_714_100_16 -card-mto answer[ want 16] stdout cand:DIFF c4off:DIFF probes cand:DIFF c4off:DIFF +TN_144_2_13 -no-card answer[o 13 want 13] stdout cand:same c4off:same probes cand:same c4off:same +TN_144_2_13 -card-mto answer[o 13 want 13] stdout cand:same c4off:same probes cand:same c4off:same +LP_714_100_16 -no-card answer[o 16 want 16] stdout cand:same c4off:same probes cand:same c4off:same +LP_714_100_16 -card-mto answer[o 16 want 16] stdout cand:same c4off:same probes cand:same c4off:same +TN_250_10_15 -no-card answer[o 15 want 15] stdout cand:same c4off:same probes cand:same c4off:same +TN_250_10_15 -card-mto answer[o 15 want 15] stdout cand:same c4off:same probes cand:same c4off:same diff --git a/optimization/experiments/GH-218/T0/test_cc_66dc5b6.txt b/optimization/experiments/GH-218/T0/test_cc_66dc5b6.txt new file mode 100644 index 00000000..ae066d97 --- /dev/null +++ b/optimization/experiments/GH-218/T0/test_cc_66dc5b6.txt @@ -0,0 +1,1301 @@ +g++ -Isrc/solver -Wall -Wno-parentheses -O3 -g -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -DNDEBUG -std=c++17 -o build/test_cc_engine tests/test_cc_engine.cc build/SimpSolver.o build/Solver.o build/Options.o build/System.o build/cc_half.o build/cc_driver.o build/cc_ubsearch.o build/cc_aut.o -lz +In file included from src/solver/Solver.h:55, + from src/solver/SimpSolver.h:37, + from tests/../src/core/distqldpc.cc:47, + from tests/test_cc_engine.cc:100: +src/solver/utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix] + 285 | fprintf(stderr, "%4"PRIi64, range.begin); + | ^ +src/solver/utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix] + 291 | fprintf(stderr, "%4"PRIi64, range.end); + | ^ +src/solver/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix] + 293 | fprintf(stderr, "] (default: %"PRIi64")\n", value); + | ^ +tests/../src/core/distqldpc.cc: In function ‘void cc_sink_trap(void*)’: +tests/../src/core/distqldpc.cc:2026:29: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 2026 | if (pw >= 0) (void)write(pw, "RESULT -1 TRAP\n", 15); + | ~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~ +tests/../src/core/distqldpc.cc: In function ‘void pipe_bound(int, const char*, uint64_t)’: +tests/../src/core/distqldpc.cc:1456:29: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 1456 | if (len > 0) (void)write(pipe_w, buf, (size_t)len); + | ~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~ +tests/../src/core/distqldpc.cc: In function ‘void pipe_write_result(int, int, bool)’: +tests/../src/core/distqldpc.cc:171:20: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 171 | (void)write(pipe_w, buf, (size_t)n); + | ~~~~~^~~~~~~~~~~~~~~~~~~~~~~~ +./build/test_cc_engine +partI(a) (GH-157 charge): 20000 hitting-set instances, 0 bad (charge = tau on 15739; charge > pack on 4780) +partI(a) mutant 15 (charge + 1/D) exceeds tau on 17240 instances +partI(b) (GH-157 charge on the Part A halves): 345600 ladder runs (128 base subsets x 3 configurations x seeds 0..2), 0 bad, 9931487 charge prunes +mutant 15 (charge inflated by 1/D): 3408/38400 half ladders wrong +partA: 300 half instances (151 with verified orbits, 120 with all column weights odd, 113 without any nontrivial element), 115200 ladder runs over 128 rule subsets x 3 seeds, 0 bad +partA K (GH-138): 100 basis, 100 low-weight sets, 55 random sets; 80 instances where a minimum element meets a row of K in floor(|g|/2) qubits +partE (rotated surface codes d = 3, 4, X/Z swapped): 40 canonical checks, 0 bad +partF (MaxSAT -ub-pre): 1600 runs on 200 codes, 0 bad (first UB = d on 1426 runs, > d on 174 runs); mutant 1 200 runs, 0 bad; surface codes d = 3..5: 36 canonical/mutant-1 runs, 0 bad +partF mutant 2 (finder without detector check, words unverified): 4/200 code runs and 9/9 surface runs wrong +partG (a) encodings (binomial, sequential counter, native propagator; w = 1..14): 42 checks, 0 bad +partG (b) MaxSAT -stab-overlap: 4600 runs on 200 codes (178 codes where the rule removes an element of F of weight <= d + 2), 0 bad; surface codes d = 3..5: 24 runs, 0 bad +partG mutant 1 (limit floor(|g|/2) - 1): 110/424 runs failed, 40 with a wrong RESULT d OPTIMAL (0 on surface codes, 20 with the native propagator) +partG mutant 2 (parity rows of the half as g, unverified): 2/424 runs failed, 2 with a wrong RESULT d OPTIMAL (0 on surface codes) +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 4 +c provided LB: 1 (search units 1) +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 386 conflicts with init 9614 + +c UB=4 fails, cnfls=386, hcnfls=228, core 167, tier2 17, local 11, quasiC: 1 (fixed: 19) +c prunedLB 2.00, dev 0.00, succRate 0.97, nbSucc 71, nbHardens 156 (fixed 3136), lk: 73, shorten: 0, pureSo 88, nbFlyRd 38, nbFixedLH 0 +c no feasible solution, hardConflicts: 228 +c nbLK: 73, nbSuccLK: 71(97.26%), nbLKup: 3849(43.51%), hardens 156 (fixed 3136), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 4 +c provided LB: 1 (search units 1) +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 386 conflicts with init 9614 + +c UB=4 fails, cnfls=386, hcnfls=228, core 167, tier2 17, local 11, quasiC: 1 (fixed: 19) +c prunedLB 2.00, dev 0.00, succRate 0.97, nbSucc 71, nbHardens 156 (fixed 3136), lk: 73, shorten: 0, pureSo 88, nbFlyRd 38, nbFixedLH 0 +c no feasible solution, hardConflicts: 228 +c nbLK: 73, nbSuccLK: 71(97.26%), nbLKup: 3849(43.51%), hardens 156 (fixed 3136), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 5 +c provided LB: 1 (search units 1) +c UB=5 succs, confls=30, hconfls=18, core 21, tier2 6, local 11, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 12, nbFlyRd 5, nbFixedLH 0 +c nbHardens 5 (fixed 79), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 30 conflicts with init 9970 + +c UB=4 succ, confls=30 and hconfls=18 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 18 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(12.19%), hardens 5 (fixed 79), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 5 +c provided LB: 1 (search units 1) +c UB=5 succs, confls=30, hconfls=18, core 21, tier2 6, local 11, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 12, nbFlyRd 5, nbFixedLH 0 +c nbHardens 5 (fixed 79), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 30 conflicts with init 9970 + +c UB=4 succ, confls=30 and hconfls=18 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 18 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(12.19%), hardens 5 (fixed 79), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=27, hconfls=25, core 10, tier2 2, local 15, 10 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 2, nbFlyRd 6, nbFixedLH 0 +c nbHardens 2 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 27 conflicts with init 9973 + +c UB=10 succ, confls=27 and hconfls=25 with 10 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 26, hardConflicts: 25 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(11.04%), hardens 2 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=19, hconfls=14, core 13, tier2 3, local 9, 8 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 5, nbFlyRd 3, nbFixedLH 0 +c nbHardens 2 (fixed 28), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 19 conflicts with init 9981 + +c UB=8 succ, confls=19 and hconfls=14 with 8 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 28, hardConflicts: 14 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(12.50%), hardens 2 (fixed 28), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=27, hconfls=25, core 10, tier2 2, local 15, 10 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 2, nbFlyRd 6, nbFixedLH 0 +c nbHardens 2 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 27 conflicts with init 9973 + +c UB=10 succ, confls=27 and hconfls=25 with 10 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 26, hardConflicts: 25 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(11.04%), hardens 2 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=19, hconfls=14, core 13, tier2 3, local 9, 8 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 5, nbFlyRd 3, nbFixedLH 0 +c nbHardens 2 (fixed 28), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 19 conflicts with init 9981 + +c UB=8 succ, confls=19 and hconfls=14 with 8 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 28, hardConflicts: 14 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(12.50%), hardens 2 (fixed 28), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=25, hconfls=22, core 9, tier2 1, local 15, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 1, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 5.50, dev 0.50, succRate 0.67, nbSucc 2, lk: 3, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 25 conflicts with init 9975 + +c UB=4 succ, confls=25 and hconfls=22 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 2, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 22 +c nbLK: 3, nbSuccLK: 2(66.67%), nbLKup: 398(45.96%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=19, hconfls=14, core 13, tier2 3, local 9, 8 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 5, nbFlyRd 3, nbFixedLH 0 +c nbHardens 2 (fixed 28), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 2, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 19 conflicts with init 9981 + +c UB=8 succ, confls=19 and hconfls=14 with 8 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 28, hardConflicts: 14 +c nbLK: 2, nbSuccLK: 0(0.00%), nbLKup: 113(12.50%), hardens 2 (fixed 28), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=27, hconfls=25, core 10, tier2 2, local 15, 10 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 2, nbFlyRd 6, nbFixedLH 0 +c nbHardens 2 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 27 conflicts with init 9973 + +c UB=10 succ, confls=27 and hconfls=25 with 10 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 26, hardConflicts: 25 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(11.04%), hardens 2 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=19, hconfls=14, core 13, tier2 3, local 9, 8 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 5, nbFlyRd 3, nbFixedLH 0 +c nbHardens 2 (fixed 28), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 19 conflicts with init 9981 + +c UB=8 succ, confls=19 and hconfls=14 with 8 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 28, hardConflicts: 14 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(12.50%), hardens 2 (fixed 28), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=27, hconfls=25, core 10, tier2 2, local 15, 10 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 2, nbFlyRd 6, nbFixedLH 0 +c nbHardens 2 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 27 conflicts with init 9973 + +c UB=10 succ, confls=27 and hconfls=25 with 10 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 26, hardConflicts: 25 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(11.04%), hardens 2 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=19, hconfls=14, core 13, tier2 3, local 9, 8 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 5, nbFlyRd 3, nbFixedLH 0 +c nbHardens 2 (fixed 28), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 19 conflicts with init 9981 + +c UB=8 succ, confls=19 and hconfls=14 with 8 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 28, hardConflicts: 14 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 113(12.50%), hardens 2 (fixed 28), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=25, hconfls=22, core 9, tier2 1, local 15, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 1, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 5.50, dev 0.50, succRate 0.67, nbSucc 2, lk: 3, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 25 conflicts with init 9975 + +c UB=4 succ, confls=25 and hconfls=22 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 2, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 22 +c nbLK: 3, nbSuccLK: 2(66.67%), nbLKup: 398(45.96%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 115 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=115, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2268 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=19, hconfls=14, core 13, tier2 3, local 9, 8 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 5, nbFlyRd 3, nbFixedLH 0 +c nbHardens 2 (fixed 28), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 2, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 19 conflicts with init 9981 + +c UB=8 succ, confls=19 and hconfls=14 with 8 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 28, hardConflicts: 14 +c nbLK: 2, nbSuccLK: 0(0.00%), nbLKup: 113(12.50%), hardens 2 (fixed 28), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 4 +c provided LB: 1 (search units 1) +c ***** top quasi confl at level 0***** +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 363 conflicts with init 9637 + +c UB=4 fails, cnfls=363, hcnfls=224, core 130, tier2 16, local 17, quasiC: 12 (fixed: 113) +c prunedLB 2.26, dev 0.44, succRate 0.77, nbSucc 58, nbHardens 149 (fixed 2973), lk: 75, shorten: 0, pureSo 81, nbFlyRd 40, nbFixedLH 3 +c no feasible solution, hardConflicts: 224 +c nbLK: 75, nbSuccLK: 58(77.33%), nbLKup: 5097(61.02%), hardens 149 (fixed 2973), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 4 +c provided LB: 1 (search units 1) +c ***** top quasi confl at level 0***** +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 363 conflicts with init 9637 + +c UB=4 fails, cnfls=363, hcnfls=224, core 130, tier2 16, local 17, quasiC: 12 (fixed: 113) +c prunedLB 2.26, dev 0.44, succRate 0.77, nbSucc 58, nbHardens 149 (fixed 2973), lk: 75, shorten: 0, pureSo 81, nbFlyRd 40, nbFixedLH 3 +c no feasible solution, hardConflicts: 224 +c nbLK: 75, nbSuccLK: 58(77.33%), nbLKup: 5097(61.02%), hardens 149 (fixed 2973), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 5 +c provided LB: 1 (search units 1) +c UB=5 succs, confls=8, hconfls=8, core 3, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 2 (fixed 7), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 8 conflicts with init 9992 + +c UB=4 succ, confls=8 and hconfls=8 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 8 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(51.10%), hardens 2 (fixed 7), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 5 +c provided LB: 1 (search units 1) +c UB=5 succs, confls=8, hconfls=8, core 3, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 2 (fixed 7), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 8 conflicts with init 9992 + +c UB=4 succ, confls=8 and hconfls=8 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 8 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(51.10%), hardens 2 (fixed 7), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 116 vars, 602 cls (c/v ratio==5.2, grow=0) +c No iterative elimination performed. (vars=116, c/v ratio=5.2) +c nb soft clauses: 36, of which 36 unit, 0 nonUnit and 0 empty +c total nb of literals: 2260 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 26 +c 1 conflict sets found with length 20 +c fixedCost 0, nbSatLits 0, totalFixedVars 26, objForSearch: 36 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=9, hconfls=9, core 4, tier2 2, local 3, 4 soft cls unsat (0 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 9 conflicts with init 9991 + +c UB=4 succ, confls=9 and hconfls=9 with 4 soft clauses unsat (0 at level 0) and 26 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 4, maxsat: 32, hardConflicts: 9 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 116(50.00%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 8 +c provided LB: 1 (search units 1) +c nbFailedLits 0, nbI 0, fixedVarsByFL 0, totalFixedVars 44, nbTested: 236, counter 8766 +c nbFailedLits 0, nbI 0, fixedVarsByFL 0, totalFixedVars 44, nbTested: 236, counter 42536 +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 8675 conflicts with init 1325 + +c UB=8 fails, cnfls=8675, hcnfls=795, core 1570, tier2 328, local 1680, quasiC: 1393 (fixed: 23038) +c prunedLB 4.06, dev 0.92, succRate 0.74, nbSucc 7624, nbHardens 195 (fixed 28345), lk: 10241, shorten: 0, pureSo 257, nbFlyRd 142, nbFixedLH 122 +c no feasible solution, hardConflicts: 795 +c nbLK: 10241, nbSuccLK: 7624(74.45%), nbLKup: 1647389(1064.42%), hardens 195 (fixed 28345), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 8 +c provided LB: 1 (search units 1) +c nbFailedLits 0, nbI 0, fixedVarsByFL 0, totalFixedVars 44, nbTested: 236, counter 8766 +c nbFailedLits 0, nbI 0, fixedVarsByFL 0, totalFixedVars 44, nbTested: 236, counter 42536 +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 8675 conflicts with init 1325 + +c UB=8 fails, cnfls=8675, hcnfls=795, core 1570, tier2 328, local 1680, quasiC: 1393 (fixed: 23038) +c prunedLB 4.06, dev 0.92, succRate 0.74, nbSucc 7624, nbHardens 195 (fixed 28345), lk: 10241, shorten: 0, pureSo 257, nbFlyRd 142, nbFixedLH 122 +c no feasible solution, hardConflicts: 795 +c nbLK: 10241, nbSuccLK: 7624(74.45%), nbLKup: 1647389(1064.42%), hardens 195 (fixed 28345), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 9 +c provided LB: 1 (search units 1) +c UB=9 succs, confls=302, hconfls=181, core 244, tier2 34, local 208, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 117, nbFlyRd 42, nbFixedLH 0 +c nbHardens 60 (fixed 1700), shorten: 0, prunedLB 2.00, dev 0.00, succRate 0.67, nbSucc 4, lk: 6, shorten: 0, quasiC: 1 (fixed: 18) + +c ends of initiationization by VSIDS at 302 conflicts with init 9698 + +c UB=8 succ, confls=302 and hconfls=181 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 4, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 181 +c nbLK: 6, nbSuccLK: 4(66.67%), nbLKup: 484(4.88%), hardens 60 (fixed 1700), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 9 +c provided LB: 1 (search units 1) +c UB=9 succs, confls=302, hconfls=181, core 244, tier2 34, local 208, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 117, nbFlyRd 42, nbFixedLH 0 +c nbHardens 60 (fixed 1700), shorten: 0, prunedLB 2.00, dev 0.00, succRate 0.67, nbSucc 4, lk: 6, shorten: 0, quasiC: 1 (fixed: 18) + +c ends of initiationization by VSIDS at 302 conflicts with init 9698 + +c UB=8 succ, confls=302 and hconfls=181 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 4, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 181 +c nbLK: 6, nbSuccLK: 4(66.67%), nbLKup: 484(4.88%), hardens 60 (fixed 1700), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=432, hconfls=328, core 186, tier2 54, local 343, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 43, nbFlyRd 49, nbFixedLH 6 +c nbHardens 47 (fixed 1203), shorten: 0, prunedLB 3.62, dev 1.15, succRate 0.91, nbSucc 61, lk: 67, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 432 conflicts with init 9568 + +c UB=8 succ, confls=432 and hconfls=328 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 61, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 328 +c nbLK: 67, nbSuccLK: 61(91.04%), nbLKup: 4451(29.36%), hardens 47 (fixed 1203), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=286, hconfls=200, core 113, tier2 42, local 209, 10 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 86, nbFlyRd 50, nbFixedLH 0 +c nbHardens 29 (fixed 678), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 3, shorten: 0, quasiC: 1 (fixed: 6) + +c ends of initiationization by VSIDS at 286 conflicts with init 9714 + +c UB=10 succ, confls=286 and hconfls=200 with 10 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 62, hardConflicts: 200 +c nbLK: 3, nbSuccLK: 0(0.00%), nbLKup: 931(8.66%), hardens 29 (fixed 678), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=308, hconfls=250, core 135, tier2 38, local 241, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 36, nbFlyRd 41, nbFixedLH 3 +c nbHardens 35 (fixed 913), shorten: 0, prunedLB 4.27, dev 1.42, succRate 0.71, nbSucc 22, lk: 31, shorten: 0, quasiC: 2 (fixed: 17) + +c ends of initiationization by VSIDS at 308 conflicts with init 9692 + +c UB=8 succ, confls=308 and hconfls=250 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 22, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 250 +c nbLK: 31, nbSuccLK: 22(70.97%), nbLKup: 3490(30.31%), hardens 35 (fixed 913), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=267, hconfls=185, core 99, tier2 37, local 198, 10 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 78, nbFlyRd 48, nbFixedLH 1 +c nbHardens 26 (fixed 608), shorten: 0, prunedLB 5.50, dev 1.12, succRate 0.50, nbSucc 4, lk: 8, shorten: 0, quasiC: 1 (fixed: 4) + +c ends of initiationization by VSIDS at 267 conflicts with init 9733 + +c UB=10 succ, confls=267 and hconfls=185 with 10 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 4, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 62, hardConflicts: 185 +c nbLK: 8, nbSuccLK: 4(50.00%), nbLKup: 1355(13.24%), hardens 26 (fixed 608), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=146, hconfls=69, core 29, tier2 11, local 132, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 3, nbFlyRd 32, nbFixedLH 19 +c nbHardens 0 (fixed 66), shorten: 0, prunedLB 6.15, dev 1.47, succRate 0.64, nbSucc 74, lk: 116, shorten: 0, quasiC: 11 (fixed: 66) + +c ends of initiationization by VSIDS at 146 conflicts with init 9854 + +c UB=8 succ, confls=146 and hconfls=69 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 74, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 69 +c nbLK: 116, nbSuccLK: 74(63.79%), nbLKup: 18671(452.63%), hardens 0 (fixed 66), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=135, hconfls=83, core 22, tier2 20, local 113, 10 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 26, nbFlyRd 22, nbFixedLH 8 +c nbHardens 6 (fixed 110), shorten: 0, prunedLB 3.04, dev 0.81, succRate 0.74, nbSucc 26, lk: 35, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 135 conflicts with init 9865 + +c UB=10 succ, confls=135 and hconfls=83 with 10 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 26, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 62, hardConflicts: 83 +c nbLK: 35, nbSuccLK: 26(74.29%), nbLKup: 2152(44.03%), hardens 6 (fixed 110), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=432, hconfls=328, core 186, tier2 54, local 343, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 43, nbFlyRd 49, nbFixedLH 6 +c nbHardens 47 (fixed 1203), shorten: 0, prunedLB 3.62, dev 1.15, succRate 0.91, nbSucc 61, lk: 67, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 432 conflicts with init 9568 + +c UB=8 succ, confls=432 and hconfls=328 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 61, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 328 +c nbLK: 67, nbSuccLK: 61(91.04%), nbLKup: 4451(29.36%), hardens 47 (fixed 1203), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=286, hconfls=200, core 113, tier2 42, local 209, 10 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 86, nbFlyRd 50, nbFixedLH 0 +c nbHardens 29 (fixed 678), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 3, shorten: 0, quasiC: 1 (fixed: 6) + +c ends of initiationization by VSIDS at 286 conflicts with init 9714 + +c UB=10 succ, confls=286 and hconfls=200 with 10 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 62, hardConflicts: 200 +c nbLK: 3, nbSuccLK: 0(0.00%), nbLKup: 931(8.66%), hardens 29 (fixed 678), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=308, hconfls=250, core 135, tier2 38, local 241, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 36, nbFlyRd 41, nbFixedLH 3 +c nbHardens 35 (fixed 913), shorten: 0, prunedLB 4.27, dev 1.42, succRate 0.71, nbSucc 22, lk: 31, shorten: 0, quasiC: 2 (fixed: 17) + +c ends of initiationization by VSIDS at 308 conflicts with init 9692 + +c UB=8 succ, confls=308 and hconfls=250 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 22, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 250 +c nbLK: 31, nbSuccLK: 22(70.97%), nbLKup: 3490(30.31%), hardens 35 (fixed 913), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=267, hconfls=185, core 99, tier2 37, local 198, 10 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 78, nbFlyRd 48, nbFixedLH 1 +c nbHardens 26 (fixed 608), shorten: 0, prunedLB 5.50, dev 1.12, succRate 0.50, nbSucc 4, lk: 8, shorten: 0, quasiC: 1 (fixed: 4) + +c ends of initiationization by VSIDS at 267 conflicts with init 9733 + +c UB=10 succ, confls=267 and hconfls=185 with 10 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 4, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 62, hardConflicts: 185 +c nbLK: 8, nbSuccLK: 4(50.00%), nbLKup: 1355(13.24%), hardens 26 (fixed 608), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=146, hconfls=69, core 29, tier2 11, local 132, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 3, nbFlyRd 32, nbFixedLH 19 +c nbHardens 0 (fixed 66), shorten: 0, prunedLB 6.15, dev 1.47, succRate 0.64, nbSucc 74, lk: 116, shorten: 0, quasiC: 11 (fixed: 66) + +c ends of initiationization by VSIDS at 146 conflicts with init 9854 + +c UB=8 succ, confls=146 and hconfls=69 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 74, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 69 +c nbLK: 116, nbSuccLK: 74(63.79%), nbLKup: 18671(452.63%), hardens 0 (fixed 66), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 236 vars, 1266 cls (c/v ratio==5.4, grow=0) +c No iterative elimination performed. (vars=236, c/v ratio=5.4) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4800 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=135, hconfls=83, core 22, tier2 20, local 113, 10 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 26, nbFlyRd 22, nbFixedLH 8 +c nbHardens 6 (fixed 110), shorten: 0, prunedLB 3.04, dev 0.81, succRate 0.74, nbSucc 26, lk: 35, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 135 conflicts with init 9865 + +c UB=10 succ, confls=135 and hconfls=83 with 10 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 26, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 10, maxsat: 62, hardConflicts: 83 +c nbLK: 35, nbSuccLK: 26(74.29%), nbLKup: 2152(44.03%), hardens 6 (fixed 110), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 8 +c provided LB: 1 (search units 1) +c nbFailedLits 0, nbI 0, fixedVarsByFL 0, totalFixedVars 44, nbTested: 237, counter 10184 +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 5827 conflicts with init 4173 + +c UB=8 fails, cnfls=5827, hcnfls=638, core 3198, tier2 1697, local 2811, quasiC: 1033 (fixed: 17558) +c prunedLB 4.25, dev 1.02, succRate 0.71, nbSucc 5017, nbHardens 228 (fixed 26578), lk: 7043, shorten: 0, pureSo 173, nbFlyRd 148, nbFixedLH 119 +c no feasible solution, hardConflicts: 638 +c nbLK: 7043, nbSuccLK: 5017(71.23%), nbLKup: 1204732(1043.96%), hardens 228 (fixed 26578), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 8 +c provided LB: 1 (search units 1) +c nbFailedLits 0, nbI 0, fixedVarsByFL 0, totalFixedVars 44, nbTested: 237, counter 10184 +c ***** top quasi confl at level 0***** +c ends of initiationization by VSIDS at 5827 conflicts with init 4173 + +c UB=8 fails, cnfls=5827, hcnfls=638, core 3198, tier2 1697, local 2811, quasiC: 1033 (fixed: 17558) +c prunedLB 4.25, dev 1.02, succRate 0.71, nbSucc 5017, nbHardens 228 (fixed 26578), lk: 7043, shorten: 0, pureSo 173, nbFlyRd 148, nbFixedLH 119 +c no feasible solution, hardConflicts: 638 +c nbLK: 7043, nbSuccLK: 5017(71.23%), nbLKup: 1204732(1043.96%), hardens 228 (fixed 26578), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 9 +c provided LB: 1 (search units 1) +c UB=9 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 5, nbFixedLH 0 +c nbHardens 2 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 2 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 9 +c provided LB: 1 (search units 1) +c UB=9 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 5, nbFixedLH 0 +c nbHardens 2 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 2 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=15, core 6, tier2 4, local 5, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 0, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=15 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 15 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(43.91%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=15, core 6, tier2 4, local 5, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 0, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=15 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 15 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(43.91%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=15, core 6, tier2 4, local 5, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 0, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=15 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 15 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(43.91%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=15, core 6, tier2 4, local 5, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 0, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=15 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 15 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(43.91%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=15, core 6, tier2 4, local 5, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 0, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=15 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 15 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(43.91%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=15, core 6, tier2 4, local 5, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 0, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=15 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 15 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(43.91%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +c Mono: 0, fixed: 0 +c Reduced to 237 vars, 1266 cls (c/v ratio==5.3, grow=0) +c No iterative elimination performed. (vars=237, c/v ratio=5.3) +c nb soft clauses: 72, of which 72 unit, 0 nonUnit and 0 empty +c total nb of literals: 4792 +c conflLits 0, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 44 +c 1 conflict sets found with length 32 +c fixedCost 0, nbSatLits 0, totalFixedVars 44, objForSearch: 72 + +c provided UB: 11 +c provided LB: 1 (search units 1) +c UB=11 succs, confls=15, hconfls=13, core 6, tier2 3, local 6, 8 soft cls unsat (0 at L0), 44 fixed vars at L0, softCnfl 2, nbFlyRd 4, nbFixedLH 0 +c nbHardens 0 (fixed 0), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 1, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 15 conflicts with init 9985 + +c UB=8 succ, confls=15 and hconfls=13 with 8 soft clauses unsat (0 at level 0) and 44 fixed vars at level 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, shortened : 0 +c initCost: 0, fixedBySearch: 0, optimal: 8, maxsat: 64, hardConflicts: 13 +c nbLK: 1, nbSuccLK: 0(0.00%), nbLKup: 238(40.20%), hardens 0 (fixed 0), dynVars 0, shorten: 0 +partG (c) GH-218 dense flags: 32 checks, 0 bad; forced dense on/off probe answers on tier0 TN halves: 8 checks, 0 bad; pilot decisions: 8 runs, 0 not reproducible (kept on 2) +partG (c) GH-218 4-cycle row gate: 224 selections on 16 codes x 2 halves, 0 bad (gated 3964, kept 6224 rows over K >= 0); mutant 3 (overlaps counted instead of pairs) changes 78 selections +partB: 200 CSS codes (52 with a verified dual map, 51 with X-half orbits, 76 with dX != dZ, 54 with all-odd Hz), 8000 driver runs, 0 bad, 0 RESULT -1 +partD (MaxSAT split, -oddcap-skip off/on): 400 runs on 200 codes (56 with an all-odd half), 0 bad +partE (ub-search finder): 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +partE (driver with ub-search): 1600 runs, 0 bad, 39 levels abandoned (U <= w) +GH-146 finder stern2 : 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +GH-146 finder stern1 : 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +GH-146 finder dumer2 : 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +GH-146 finder stern2-l0-fresh : 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +GH-146 finder dumer1-l2-w1-b3-r5 : 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +GH-146 finder stern2-l3-w32-b2 : 400 halves x 300 iterations, 0 bad, 0 nondeterministic, reached d_h on 400/400 halves +GH-146 finder mutant 11 (collision mode, no detector check): trivial word returned on 41/41 halves +GH-146 CC driver in collision mode: 600 runs, 0 bad; mutant 11 8/8 runs stopped or wrong; mutant 12 8/8 failed, 8 with a wrong RESULT d OPTIMAL +GH-146 MaxSAT pre-pass in collision mode: 400 runs, 0 bad; mutant 1 200 runs, 0 bad; mutant 2 13/209 runs wrong (codes + surface) +GH-152 partG: 300 relabeled half instances, 365 Tanner generators (235 complete groups), 55 instances with coarser orbits than the GH-75 family, 115200 ladder runs (128 rule subsets x 3 seeds), 0 bad; generators violating the row classes 0; planted map preserved the row sets on 250 (185 with a complete group), missed 0 +GH-152 partH: 150 relabeled codes (100 hypergraph products, 34 with dX != dZ), 100 gain a verified dual map only through -cc-aut, 150 gain coarser X-half orbits; 2700 driver runs with -cc-aut=on, 0 bad; swap maps violating the classes 0 +mutant 13 (Tanner candidates and the cyclic shift i -> i+1 mod n kept without the GF(2) checks): half level 1408/19200 ladders wrong; driver 182/300 runs wrong or stopped +mutant 14 (Tanner swap map, or the identity, used as dual map without the GF(2) check): driver 49/150 runs wrong or stopped +GH-162 partT: 300 half instances (200 with orbits, 100 of them hidden -cc-aut orbits; 118 all-odd; 55 with a weight-2 row in K), 49 where the cut removes a minimum element (8 with orbits), 76800 ladder runs (64 rule subsets with overlap,tiebreak x 4 seeds; charge on seeds 1 and 3), 0 bad +mutant 17 (tiebreak without the first(g) exemption: naive tie cut): 5152/76800 half ladders wrong +mutant 18 (tiebreak order without the seed first: orbit-incompatible): 160/76800 half ladders wrong (160 with orbit seeds) +GH-183 partR: 300 half instances (197 with orbits, 89 with rows unreachable from qubit 0), 384000 ladder runs (64 rule subsets x {-, overlap, overlap+tiebreak} x 4 seeds with roworder bfs, charge on seeds 1 and 3; tiebreak also tbbase asc under bfs and index), 0 bad; bfs orders not using every row 0; instances where bfs changes the node count 66 +mutant 19 (bfs order drops a row): 9088/28800 half ladders wrong +mutant 20 (bfs without restart: unreachable rows dropped): 4656/28800 half ladders wrong +GH-181 partX: 300 half instances (262 with sparse rows, 98 with sparseov rows), 576000 ladder runs (128 base subsets x 15 token subsets; charge, tiebreak and bfs mixed in), 0 bad; runs where the rule acted: spack 62833, sprune 57784, ovtightx 22208, xuforbid 154831, xuforced 135021, xudead 148662 +mutant 22 (GH-181 sparse redundant row with one qubit flipped): 33092/268800 half ladders wrong +mutant 23 (GH-181 xorunit branches on an even unit row): 30919/307200 half ladders wrong +mutant 24 (GH-181 sparseov pair sums of H instead of K): 18602/153600 half ladders wrong +GH-206 auto probe (Part B): 1800 driver runs (forced switch / stay / by time, finder on and off, tbbase asc), 0 bad +mutant 21 (auto probe of level w + 1, an aborted probe taken as refuted): 18/400 driver runs wrong or stopped +mutant 1 (forbidden set not restored): 988/19200 half ladders wrong +mutant 2 (packing prune >=): 4112/19200 half ladders wrong +mutant 3 (orbit seed rule off by one, instances with orbits): 1856/9664 half ladders wrong +mutant 4 (stop rule without other half's lb, forces sequential): schedule requested 58/200 runs wrong; default options 58/200 wrong +mutant 5 (parity rule forced on halves with an even column weight): 6976/11520 half ladders wrong +mutant 6 (leaf budget off by one): 2112/19200 half ladders wrong +mutant 7 (leaf closure without the detector check): 1760/19200 half ladders wrong +mutant 8 (overlap limit off by one): 2880/19200 half ladders wrong +mutant 9 (overlap with the parity checks H as K): 3776/19200 half ladders wrong +mutant 10 (overlap even-|g| tie cut): 2112/19200 half ladders wrong +mutant 11 (ub-search without the detector check; halves/codes where a trivial word is lighter than d): finder returned a trivial word on 33/33 halves; driver 8/8 runs stopped or wrong +mutant 12 (mutant 11 + words reported without verification): 8/8 driver runs failed, 8 of them with a wrong RESULT d OPTIMAL +CC_ENGINE_TESTS PASS +rc 0 diff --git a/optimization/experiments/GH-218/T0/test_cc_flags_66dc5b6.txt b/optimization/experiments/GH-218/T0/test_cc_flags_66dc5b6.txt new file mode 100644 index 00000000..4988bdec --- /dev/null +++ b/optimization/experiments/GH-218/T0/test_cc_flags_66dc5b6.txt @@ -0,0 +1,3 @@ +test_cc_flags: 579 checks, 0 failed +CC_FLAG_TESTS PASS +rc 0 diff --git a/optimization/experiments/GH-218/T0/u0_caps_tier2-4_5seeds.txt b/optimization/experiments/GH-218/T0/u0_caps_tier2-4_5seeds.txt new file mode 100644 index 00000000..95559722 --- /dev/null +++ b/optimization/experiments/GH-218/T0/u0_caps_tier2-4_5seeds.txt @@ -0,0 +1,41 @@ +tier2/TN_108_2_12 -no-card s0 | c ub-pre: U0 after 0.006s (both halves converged; iterations X 17 Z 19, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -no-card s1 | c ub-pre: U0 after 0.005s (both halves converged; iterations X 19 Z 18, words X 1 Z 1): 12 (X 13, Z 12) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -no-card s2 | c ub-pre: U0 after 0.009s (both halves converged; iterations X 19 Z 18, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -no-card s3 | c ub-pre: U0 after 0.011s (both halves converged; iterations X 20 Z 16, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -no-card s4 | c ub-pre: U0 after 0.013s (both halves converged; iterations X 18 Z 17, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -card-mto s0 | c ub-pre: U0 after 0.006s (both halves converged; iterations X 17 Z 19, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -card-mto s1 | c ub-pre: U0 after 0.009s (both halves converged; iterations X 19 Z 18, words X 1 Z 1): 12 (X 13, Z 12) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -card-mto s2 | c ub-pre: U0 after 0.006s (both halves converged; iterations X 19 Z 18, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -card-mto s3 | c ub-pre: U0 after 0.009s (both halves converged; iterations X 20 Z 16, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_108_2_12 -card-mto s4 | c ub-pre: U0 after 0.003s (both halves converged; iterations X 18 Z 17, words X 1 Z 0): 12 (X 12, Z -1) | caps 1,1,2,2,4,4,8,8,11,11, | pilot_lines 0 +tier2/TN_200_10_10 -no-card s0 | c ub-pre: U0 after 0.175s (both halves converged; iterations X 1001 Z 17, words X 1 Z 1): 10 (X 15, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -no-card s1 | c ub-pre: U0 after 0.180s (both halves converged; iterations X 1001 Z 18, words X 1 Z 1): 10 (X 14, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -no-card s2 | c ub-pre: U0 after 0.176s (both halves converged; iterations X 1001 Z 18, words X 1 Z 1): 10 (X 15, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -no-card s3 | c ub-pre: U0 after 0.180s (both halves converged; iterations X 1001 Z 17, words X 1 Z 1): 10 (X 16, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -no-card s4 | c ub-pre: U0 after 0.177s (both halves converged; iterations X 1001 Z 17, words X 1 Z 1): 10 (X 16, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -card-mto s0 | c ub-pre: U0 after 0.163s (both halves converged; iterations X 1001 Z 17, words X 1 Z 1): 10 (X 15, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -card-mto s1 | c ub-pre: U0 after 0.161s (both halves converged; iterations X 1001 Z 18, words X 1 Z 1): 10 (X 14, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -card-mto s2 | c ub-pre: U0 after 0.161s (both halves converged; iterations X 1001 Z 18, words X 1 Z 1): 10 (X 15, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -card-mto s3 | c ub-pre: U0 after 0.165s (both halves converged; iterations X 1001 Z 17, words X 1 Z 1): 10 (X 16, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier2/TN_200_10_10 -card-mto s4 | c ub-pre: U0 after 0.161s (both halves converged; iterations X 1001 Z 17, words X 1 Z 1): 10 (X 16, Z 10) | caps 1,1,2,2,4,4,8,8,9,9, | pilot_lines 0 +tier3/TN_144_2_13 -no-card s0 | c ub-pre: U0 after 0.013s (both halves converged; iterations X 71 Z 87, words X 2 Z 0): 13 (X 13, Z -1) | caps 1,1,2,2,4,4,8,8,12, | pilot_lines 0 +tier3/TN_144_2_13 -no-card s1 | c ub-pre: U0 after 0.017s (both halves converged; iterations X 126 Z 84, words X 1 Z 2): 13 (X 15, Z 13) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier3/TN_144_2_13 -no-card s2 | c ub-pre: U0 after 0.013s (both halves converged; iterations X 70 Z 89, words X 1 Z 0): 13 (X 13, Z -1) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier3/TN_144_2_13 -no-card s3 | c ub-pre: U0 after 0.012s (both halves converged; iterations X 60 Z 82, words X 1 Z 0): 13 (X 13, Z -1) | caps 1,1,2,2,4,4,8,8,12, | pilot_lines 0 +tier3/TN_144_2_13 -no-card s4 | c ub-pre: U0 after 0.019s (both halves converged; iterations X 99 Z 135, words X 2 Z 1): 13 (X 13, Z 14) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier3/TN_144_2_13 -card-mto s0 | c ub-pre: U0 after 0.014s (both halves converged; iterations X 64 Z 105, words X 1 Z 1): 13 (X 15, Z 13) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier3/TN_144_2_13 -card-mto s1 | c ub-pre: U0 after 0.017s (both halves converged; iterations X 126 Z 84, words X 1 Z 2): 13 (X 15, Z 13) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier3/TN_144_2_13 -card-mto s2 | c ub-pre: U0 after 0.013s (both halves converged; iterations X 70 Z 89, words X 1 Z 0): 13 (X 13, Z -1) | caps 1,1,2,2,4,4,8,8,12, | pilot_lines 0 +tier3/TN_144_2_13 -card-mto s3 | c ub-pre: U0 after 0.012s (both halves converged; iterations X 60 Z 82, words X 1 Z 0): 13 (X 13, Z -1) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier3/TN_144_2_13 -card-mto s4 | c ub-pre: U0 after 0.019s (both halves converged; iterations X 99 Z 135, words X 2 Z 1): 13 (X 13, Z 14) | caps 1,1,2,2,4,4,8,8,12,12, | pilot_lines 0 +tier4/TN_250_10_15 -no-card s0 | c ub-pre: U0 after 0.148s (both halves converged; iterations X 258 Z 345, words X 1 Z 1): 15 (X 19, Z 15) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -no-card s1 | c ub-pre: U0 after 0.184s (both halves converged; iterations X 280 Z 467, words X 2 Z 1): 15 (X 15, Z 16) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -no-card s2 | c ub-pre: U0 after 0.194s (both halves converged; iterations X 325 Z 478, words X 2 Z 0): 15 (X 15, Z -1) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -no-card s3 | c ub-pre: U0 after 0.163s (both halves converged; iterations X 235 Z 444, words X 2 Z 2): 15 (X 15, Z 16) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -no-card s4 | c ub-pre: U0 after 0.173s (both halves converged; iterations X 311 Z 392, words X 2 Z 0): 15 (X 15, Z -1) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -card-mto s0 | c ub-pre: U0 after 0.148s (both halves converged; iterations X 258 Z 345, words X 1 Z 1): 15 (X 19, Z 15) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -card-mto s1 | c ub-pre: U0 after 0.182s (both halves converged; iterations X 280 Z 467, words X 2 Z 1): 15 (X 15, Z 16) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -card-mto s2 | c ub-pre: U0 after 0.196s (both halves converged; iterations X 325 Z 478, words X 2 Z 0): 15 (X 15, Z -1) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -card-mto s3 | c ub-pre: U0 after 0.164s (both halves converged; iterations X 235 Z 444, words X 2 Z 2): 15 (X 15, Z 16) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +tier4/TN_250_10_15 -card-mto s4 | c ub-pre: U0 after 0.173s (both halves converged; iterations X 311 Z 392, words X 2 Z 0): 15 (X 15, Z -1) | caps 1,1,2,2,4,4,8,8, | pilot_lines 0 +DONE diff --git a/optimization/experiments/GH-218/T5/t5_logs.tgz b/optimization/experiments/GH-218/T5/t5_logs.tgz new file mode 100644 index 00000000..b5a595be Binary files /dev/null and b/optimization/experiments/GH-218/T5/t5_logs.tgz differ diff --git a/optimization/experiments/GH-218/T5/t5_table.txt b/optimization/experiments/GH-218/T5/t5_table.txt new file mode 100644 index 00000000..a5ca5d5f --- /dev/null +++ b/optimization/experiments/GH-218/T5/t5_table.txt @@ -0,0 +1,24 @@ +BB_360_12_24.card-mto.cand.s0 done d=24 lb=24 wall=8075 | X16:0.03M X22:10.41M +BB_360_12_24.no-card.cand.s0 done d=24 lb=24 wall=7775 | X16:0.03M X22:10.31M +LP_1020_136_16.card-mto.cand.s0 done d=16 lb=16 wall=466 | X14:0.10M Z14:0.28M +LP_1020_136_16.no-card.cand.s0 done d=16 lb=16 wall=664 | X14:0.10M Z14:0.28M +LP_1122_148_20.card-mto.cand.s0 done d=20 lb=20 wall=14023 | X16:0.49M Z16:1.13M X18:2.32M Z18:3.98M +LP_1122_148_20.no-card.cand.s0 done d=20 lb=20 wall=13590 | X16:0.49M Z16:1.13M X18:2.32M Z18:3.98M +TN_180_2_17.card-mto.cand.s0 done d=17 lb=17 wall=10554 | X16:13.30M Z16:5.77M +TN_180_2_17.card-mto.main.s0 done d=17 lb=17 wall=6703 | X16:6.92M Z16:6.08M +TN_180_2_17.no-card.cand.s0 done d=17 lb=17 wall=6314 | X16:7.98M Z16:5.15M +TN_180_2_17.no-card.main.s0 done d=17 lb=17 wall=5919 | X16:6.47M Z16:5.22M +TN_216_4_18.card-mto.b12b.s0 done d=18 lb=18 wall=11090 | X16:3.13M Z16:4.44M X17:5.14M Z17:7.76M +TN_216_4_18.card-mto.cand.s0 done d=18 lb=18 wall=11284 | X16:3.13M Z16:4.44M X17:5.14M Z17:7.76M +TN_216_4_18.card-mto.cand.s1 done d=18 lb=18 wall=12018 | X16:2.84M Z16:4.67M X17:5.56M Z17:8.49M +TN_216_4_18.card-mto.cand.s2 done d=18 lb=18 wall=11577 | X16:2.96M Z16:4.84M X17:5.17M Z17:7.91M +TN_216_4_18.card-mto.cand.s3 done d=18 lb=18 wall=13210 | X16:2.72M Z16:5.19M X17:5.36M Z17:10.11M +TN_216_4_18.card-mto.cand.s4 done d=18 lb=18 wall=9272 | X16:2.98M Z16:2.66M X17:4.41M Z17:7.94M +TN_216_4_18.card-mto.main.s0 done d=18 lb=18 wall=11225 | X16:3.11M Z16:4.53M X17:4.25M Z17:8.00M +TN_216_4_18.no-card.b12b.s0 done d=18 lb=18 wall=10359 | X16:2.80M Z16:3.97M X17:6.12M Z17:6.80M +TN_216_4_18.no-card.cand.s0 done d=18 lb=18 wall=10485 | X16:2.80M Z16:3.97M X17:6.12M Z17:6.80M +TN_216_4_18.no-card.cand.s1 done d=18 lb=18 wall=9515 | X16:2.60M Z16:3.68M X17:4.89M Z17:7.16M +TN_216_4_18.no-card.cand.s2 done d=18 lb=18 wall=11596 | X16:2.94M Z16:4.84M X17:4.94M Z17:8.33M +TN_216_4_18.no-card.cand.s3 done d=18 lb=18 wall=13349 | X16:3.97M Z16:4.55M X17:5.55M Z17:9.49M +TN_216_4_18.no-card.cand.s4 done d=18 lb=18 wall=9945 | X16:2.80M Z16:4.42M X17:5.41M Z17:6.03M +TN_216_4_18.no-card.main.s0 done d=18 lb=18 wall=14697 | X16:2.64M Z16:5.27M X17:6.25M Z17:9.35M diff --git a/optimization/experiments/GH-218/diag/diag_counters.patch b/optimization/experiments/GH-218/diag/diag_counters.patch new file mode 100644 index 00000000..e9433e62 --- /dev/null +++ b/optimization/experiments/GH-218/diag/diag_counters.patch @@ -0,0 +1,223 @@ +diff --git a/src/core/distqldpc.cc b/src/core/distqldpc.cc +index a308a959..09a3a0d7 100644 +--- a/src/core/distqldpc.cc ++++ b/src/core/distqldpc.cc +@@ -1240,8 +1240,14 @@ static HalfStatus run_css_half(CssHalf& h, uint64_t cap, bool first_only, int ve + OvlRows ovl_active; /* GH-148: rows active in this probe (any subset of the verified rows is sound) */ + if (!h.ovl.empty()) { + for (size_t r = 0; r < h.ovl.size(); r++) +- if (g_stab_overlap_ratio <= 0.0 || (double)cap >= g_stab_overlap_ratio * (double)(h.ovl[r].size() / 2 + 1)) ++ if (g_stab_overlap_ratio <= 0.0 || (double)cap >= g_stab_overlap_ratio * (double)(h.ovl[r].size() / 2 + 1)) { ++ const int w = (int)h.ovl[r].size(); ++ if (getenv("DQ_OV_MINW") && w < atoi(getenv("DQ_OV_MINW"))) continue; ++ if (getenv("DQ_OV_MAXW") && w > atoi(getenv("DQ_OV_MAXW"))) continue; ++ if (getenv("DQ_OV_EVEN") && (w & 1)) continue; ++ if (getenv("DQ_OV_ODD") && !(w & 1)) continue; + ovl_active.push_back(h.ovl[r]); ++ } + if (verb > 0) { + printf("c stab-overlap %s cap %llu: %zu of %zu rows active (ratio %.2f)\n", h.tag, (unsigned long long)cap, + ovl_active.size(), h.ovl.size(), g_stab_overlap_ratio); +@@ -1275,7 +1281,24 @@ static HalfStatus run_css_half(CssHalf& h, uint64_t cap, bool first_only, int ve + S.frontierCheck = g_frontier_check; + } + vec dummy; ++ if (getenv("DQ_OV_VARIANT")) S.dgVariant = atoi(getenv("DQ_OV_VARIANT")); ++ const double dg_t0 = cpuTime(); + lbool ret = S.solveLimited(dummy); ++ if (getenv("DQ_DIAG")) { ++ const double dg_ticks_scale = 1.0 / 2.25e9; /* EPYC 7742 base clock (rdtsc rate) */ ++ fprintf(stderr, "c DIAG %s cap %llu %s: cpu %.3f conflicts %llu decisions %llu props %llu lkprops %llu lookahead %llu lksucc %llu " ++ "rows %zu ovcallsM %llu ovcallsL %llu ovrows %llu ovprops %llu ovpropsL %llu ovconfl %llu ovconflL %llu ovfalseL %llu " ++ "anares %llu anaov %llu learntlits %llu tM %.3f tL %.3f cached %zu redcalls %llu\n", h.tag, (unsigned long long)cap, ++ first_only ? "feasibility" : "optimize", cpuTime() - dg_t0, (unsigned long long)S.conflicts, ++ (unsigned long long)S.decisions, (unsigned long long)S.propagations, (unsigned long long)S.lk_propagations, ++ (unsigned long long)S.LOOKAHEAD, (unsigned long long)S.nbLKsuccess, ovl_active.size(), ++ (unsigned long long)S.dgCallsM, (unsigned long long)S.dgCallsL, (unsigned long long)S.dgRows, ++ (unsigned long long)S.ovProps, (unsigned long long)S.dgPropsL, (unsigned long long)S.ovConfls, ++ (unsigned long long)S.dgConflL, (unsigned long long)S.dgFalseL, (unsigned long long)S.dgAnaRes, ++ (unsigned long long)S.dgAnaOv, (unsigned long long)S.dgLearntLits, S.dgTicksM * dg_ticks_scale, ++ S.dgTicksL * dg_ticks_scale, S.ovCacheList.size(), (unsigned long long)S.dgRedCalls); ++ fflush(stderr); ++ } + if (g_frontier_stats || (h.frontier && g_frontier_check)) { /* stats also with -frontier=off (main's search) */ + fprintf(stderr, "c FRONTIER %s cap %llu %s: conflicts %llu decisions %llu frontier_picks %llu fallbacks %llu " + "no_eligible %llu mean_odd_rows %.2f check_fails %llu\n", h.tag, (unsigned long long)cap, +@@ -1682,6 +1705,17 @@ static int min_distance_css_interleaved( + } + } + uint64_t U = INF, v = 0, lastLB = 0; ++ if (getenv("DQ_DIAG_PROBE")) { /* DIAG: HALF:CAP:LB, one feasibility probe, then exit */ ++ char hc = 'X'; unsigned long long dcap = 0, dlb = 0; ++ if (sscanf(getenv("DQ_DIAG_PROBE"), "%c:%llu:%llu", &hc, &dcap, &dlb) != 3) die("DQ_DIAG_PROBE=HALF:CAP:LB"); ++ CssHalf& h = hs[hc == 'Z' ? 1 : 0]; ++ h.lb = dlb; ++ HalfStatus st = run_css_half(h, dcap, true, verb, card_mode, pipe_w, INF, INF, true, v); ++ fprintf(stderr, "c DIAGPROBE %c cap %llu -> %s\n", hc, dcap, st == HALF_FOUND ? "FOUND" : st == HALF_NONE ? "NONE" : "OTHER"); ++ fflush(stderr); ++ pipe_write_result(pipe_w, -1, false); ++ return -1; ++ } + bool seeded = false; /* GH-144: U holds a verified -ub-pre word (never without -ub-pre) */ + if (g_ub_pre >= 0) { + const Matrix* Ss[2] = { &Hx, &Hz }; /* same-type stabilizers: X half Hx, Z half Hz */ +diff --git a/src/solver/Solver.cc b/src/solver/Solver.cc +index 54446a84..d12b4586 100644 +--- a/src/solver/Solver.cc ++++ b/src/solver/Solver.cc +@@ -1,3 +1,6 @@ ++#ifdef OVDIAG_TIME ++#include ++#endif + /***************************************************************************************[Solver.cc] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + Copyright (c) 2007-2010, Niklas Sorensson +@@ -456,7 +459,7 @@ bool Solver::removed(CRef cr) { + } + + void Solver::simplereduceClause(CRef cr, int pathC) { +- if (ovIsClause(cr)) return; // GH-148: cached overlap reasons are shared and unwatched: never reduced ++ dgRedCalls++; if (ovIsClause(cr)) return; // GH-148: cached overlap reasons are shared and unwatched: never reduced + nbFlyReduced++; + Clause& c=ca[cr]; + assert(value(c[0]) == l_True); +@@ -1582,7 +1585,7 @@ Lit Solver::pickBranchLit() + } + + void Solver::reduceClause(CRef cr, int pathC) { +- if (ovIsClause(cr)) return; // GH-148: cached overlap reasons are shared and unwatched: never reduced ++ dgRedCalls++; if (ovIsClause(cr)) return; // GH-148: cached overlap reasons are shared and unwatched: never reduced + nbFlyReduced++; + Clause& c=ca[cr]; + assert(value(c[0]) == l_True); +@@ -1694,12 +1697,12 @@ void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel, int& ou + // printf("c bin bin...\n"); + } + else { +- updateClauseUse(confl); ++ updateClauseUse(confl); const bool dgNB0 = (dgVariant & 4) && ovIsClause(confl); + Clause& c = ca[confl]; + for(int i= 0; i 0) { + Var v=var(c[i]); +- if (VSIDS){ ++ if (dgNB0) {} else if (VSIDS){ + varBumpActivity(v, .5); + add_tmp.push(c[i]); + }else +@@ -1721,6 +1724,7 @@ void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel, int& ou + assert(confl != CRef_Undef); // (otherwise should be UIP) + else + break; ++ if ((dgVariant & 8) && !ovRows.empty()) { dgAnaRes++; if (confl != CRef_Bin && ovIsClause(confl)) dgAnaOv++; } const bool dgNB = (dgVariant & 4) && confl != CRef_Bin && ovIsClause(confl); + Clause& c = ca[confl]; + // For binary clauses, we don't rearrange literals in propagate(), so check and make sure the first is an implied lit. + if (c.size() == 2 && value(c[0]) == l_False){ +@@ -1739,7 +1743,7 @@ void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel, int& ou + nbSeen++; + else /*if (!redundantLit(q))*/ { + nbNotSeen++; +- if (VSIDS){ ++ if (dgNB) {} else if (VSIDS){ + varBumpActivity(v, .5); + add_tmp.push(q); + }else +@@ -1758,6 +1762,7 @@ void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel, int& ou + reduceClause(confl, pathC); //printf("a\n"); + } + out_learnt[0] = ~p; ++ dgLearntLits += out_learnt.size(); + + simplifyConflictClause(out_learnt, out_btlevel, out_lbd); + +@@ -2067,8 +2072,14 @@ CRef Solver::propagate() + NextClause:; + } + ws.shrink(i - j); +- if (!ovRows.empty() && confl == CRef_Undef) { // GH-148 native overlap rows (inactive when empty) ++ if (!ovRows.empty() && confl == CRef_Undef && !(dgVariant & 2)) { // GH-148 native overlap rows (inactive when empty) ++#ifdef OVDIAG_TIME ++ uint64_t t0 = __rdtsc(); ++#endif + CRef oc = ovPropagate(p, false); ++#ifdef OVDIAG_TIME ++ dgTicksM += __rdtsc() - t0; ++#endif + if (oc != CRef_Undef) { confl = oc; qhead = trail.size(); } + } + // if (confl == CRef_Undef) +@@ -2372,7 +2383,7 @@ void Solver::analyzeSoftConflict(vec& out_learnt, int& out_btlevel, int& ou + // c.setUsed(1); + // } + // } +- int nbSeen=0, nbNotSeen = 0; ++ int nbSeen=0, nbNotSeen = 0; const bool dgNB = (dgVariant & 4) && confl != CRef_Bin && ovIsClause(confl); + int resolventSize=pathC + out_learnt.size() - 1; + for (int j = 1; j < c.size(); j++){ + Lit q = c[j]; Var v = var(q); +@@ -2382,7 +2393,7 @@ void Solver::analyzeSoftConflict(vec& out_learnt, int& out_btlevel, int& ou + else { + // if (level(v) > 0 && !seen[v] && !redundantLit(q)) { + nbNotSeen++; +- if (VSIDS){ ++ if (dgNB) {} else if (VSIDS){ + varBumpActivity(v, .5); + add_tmp.push(q); + }else +@@ -4053,8 +4064,14 @@ CRef Solver::propagateForLK() { + NextClause:; + } + ws.shrink(i - j); +- if (!ovRows.empty() && confl == CRef_Undef && falseVar == var_Undef) { // GH-148 (inactive when empty) ++ if (!ovRows.empty() && confl == CRef_Undef && falseVar == var_Undef && !(dgVariant & 1)) { // GH-148 (inactive when empty) ++#ifdef OVDIAG_TIME ++ uint64_t t0 = __rdtsc(); ++#endif + CRef oc = ovPropagate(p, true); ++#ifdef OVDIAG_TIME ++ dgTicksL += __rdtsc() - t0; ++#endif + if (oc != CRef_Undef) { confl = oc; qhead = trail.size(); } + else if (falseVar != var_Undef) qhead = trail.size(); + } +@@ -7424,6 +7441,8 @@ CRef Solver::ovPropagate(Lit p, bool lk) + const Var v = var(p); + if ((size_t)v >= ovColRows.size()) return CRef_Undef; + const std::vector& rs = ovColRows[(size_t)v]; ++ if (lk) dgCallsL++; else dgCallsM++; ++ dgRows += rs.size(); + for (size_t a = 0; a < rs.size(); a++) { + const int r = rs[a]; + const std::vector& row = ovRows[(size_t)r]; +@@ -7438,15 +7457,15 @@ CRef Solver::ovPropagate(Lit p, bool lk) + uint32_t m = 0; int c = 1; + for (size_t t = 0; t < row.size(); t++) if (row[t] == v) m |= 1u << t; + for (size_t t = 0; t < row.size() && c <= lim; t++) if (((tmask & ~m) >> t) & 1) { m |= 1u << t; c++; } +- ovConfls++; ++ ovConfls++; if (lk) dgConflL++; + return ovClause(r, m, -1); + } + if (cnt == lim && umask) { + for (size_t t = 0; t < row.size(); t++) { + if (!((umask >> t) & 1) || value(row[t]) != l_Undef) continue; + CRef cr = ovClause(r, tmask | (1u << t), (int)t); +- ovProps++; +- if (lk) { if (!uncheckedEnqueueForLK(~mkLit(row[t]), cr)) { falseVar = row[t]; return CRef_Undef; } } ++ ovProps++; if (lk) dgPropsL++; ++ if (lk) { if (!uncheckedEnqueueForLK(~mkLit(row[t]), cr)) { dgFalseL++; falseVar = row[t]; return CRef_Undef; } } + else uncheckedEnqueue(~mkLit(row[t]), cr); + } + } +diff --git a/src/solver/Solver.h b/src/solver/Solver.h +index d6a3e7e8..76c8e79e 100644 +--- a/src/solver/Solver.h ++++ b/src/solver/Solver.h +@@ -600,6 +600,8 @@ public: + std::vector > ovCacheList; // (key, cref) for relocation + std::vector ovCacheIdx; // open addressing table into ovCacheList (-1 empty) + uint64_t ovProps = 0, ovConfls = 0; ++ uint64_t dgCallsM = 0, dgCallsL = 0, dgRows = 0, dgPropsL = 0, dgConflL = 0, dgFalseL = 0, dgTicksM = 0, dgTicksL = 0, dgAnaOv = 0, dgAnaRes = 0, dgLearntLits = 0; ++ int dgVariant = 0; uint64_t dgRedCalls = 0; // DIAG: bit0 skip ov in LK, bit1 skip ov in main propagate + std::unordered_set ovCrefs; // the cached crefs: on-the-fly clause reduction skips them + bool ovIsClause(CRef cr) const { return !ovRows.empty() && ovCrefs.count((uint32_t)cr) > 0; } + void setOverlapRows(const std::vector >& rows, const std::vector& lims, int nQubits); diff --git a/optimization/experiments/GH-218/diag/diag_logs.tgz b/optimization/experiments/GH-218/diag/diag_logs.tgz new file mode 100644 index 00000000..67af4efa Binary files /dev/null and b/optimization/experiments/GH-218/diag/diag_logs.tgz differ diff --git a/optimization/experiments/GH-218/diag/diag_table.txt b/optimization/experiments/GH-218/diag/diag_table.txt new file mode 100644 index 00000000..836e144f --- /dev/null +++ b/optimization/experiments/GH-218/diag/diag_table.txt @@ -0,0 +1,62 @@ +BB288_X16_auto.log X16 cpu 8.8 confl 42240 us/cf 209.1 lkp/cf 1565 p/cf 75 look/cf 1.73 ovp/cf 0.449 ovpL/cf 1.275 ovcf% 0.89 anaov% 1.15 lrn/cf 0.31 tM 0.0 tL 0.0 +BB288_X16_off.log X16 cpu 48.5 confl 207421 us/cf 234.0 lkp/cf 1357 p/cf 59 look/cf 1.56 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 4.18 tM 0.0 tL 0.0 +LP544_X10_auto.log X10 cpu 6.2 confl 9238 us/cf 669.3 lkp/cf 4856 p/cf 147 look/cf 1.71 ovp/cf 0.014 ovpL/cf 0.121 ovcf% 0.39 anaov% 0.05 lrn/cf 0.72 tM 0.0 tL 0.0 +LP544_X10_off.log X10 cpu 9.5 confl 14757 us/cf 643.8 lkp/cf 4408 p/cf 138 look/cf 1.63 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 2.51 tM 0.0 tL 0.0 +TN144_X12_auto.log X12 cpu 46.1 confl 280391 us/cf 164.3 lkp/cf 530 p/cf 25 look/cf 1.38 ovp/cf 0.057 ovpL/cf 0.287 ovcf% 0.26 anaov% 0.98 lrn/cf 0.89 tM 0.0 tL 0.0 +TN144_X12_off.log X12 cpu 41.5 confl 263131 us/cf 157.7 lkp/cf 523 p/cf 25 look/cf 1.38 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.86 tM 0.0 tL 0.0 +TN144_Z12_auto.log Z12 cpu 39.5 confl 258558 us/cf 152.8 lkp/cf 524 p/cf 24 look/cf 1.38 ovp/cf 0.055 ovpL/cf 0.294 ovcf% 0.28 anaov% 1.16 lrn/cf 0.87 tM 0.0 tL 0.0 +TN144_Z12_off.log Z12 cpu 32.5 confl 223833 us/cf 145.3 lkp/cf 508 p/cf 24 look/cf 1.38 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.88 tM 0.0 tL 0.0 +TN180_X16_mto_auto.log X16 cpu 3951.1 confl 6924113 us/cf 570.6 lkp/cf 661 p/cf 25 look/cf 1.40 ovp/cf 0.167 ovpL/cf 0.455 ovcf% 0.39 anaov% 2.24 lrn/cf 0.84 tM 0.0 tL 0.0 +TN180_X16_mto_off.log X16 cpu 9061.8 confl 13295888 us/cf 681.6 lkp/cf 664 p/cf 23 look/cf 1.39 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.54 tM 0.0 tL 0.0 +TN180_X16_mto_s1_auto.log X16 cpu 3031.7 confl 5724700 us/cf 529.6 lkp/cf 663 p/cf 25 look/cf 1.40 ovp/cf 0.166 ovpL/cf 0.453 ovcf% 0.39 anaov% 2.15 lrn/cf 0.81 tM 0.0 tL 0.0 +TN180_X16_mto_s1_off.log X16 cpu 7576.8 confl 12027889 us/cf 629.9 lkp/cf 675 p/cf 24 look/cf 1.39 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.55 tM 0.0 tL 0.0 +TN180_X16_mto_s2_auto.log X16 cpu 3305.1 confl 6272505 us/cf 526.9 lkp/cf 657 p/cf 25 look/cf 1.40 ovp/cf 0.158 ovpL/cf 0.444 ovcf% 0.41 anaov% 2.10 lrn/cf 0.79 tM 0.0 tL 0.0 +TN180_X16_mto_s2_off.log X16 cpu 5609.2 confl 9499484 us/cf 590.5 lkp/cf 671 p/cf 24 look/cf 1.39 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.58 tM 0.0 tL 0.0 +TN180_X16_mto_v1.log X16 cpu 3476.6 confl 6544783 us/cf 531.2 lkp/cf 652 p/cf 25 look/cf 1.40 ovp/cf 0.177 ovpL/cf 0.000 ovcf% 0.14 anaov% 2.43 lrn/cf 0.83 tM 0.0 tL 0.0 +TN180_Z16_auto.log Z16 cpu 2657.6 confl 5223943 us/cf 508.7 lkp/cf 716 p/cf 26 look/cf 1.40 ovp/cf 0.095 ovpL/cf 0.506 ovcf% 0.44 anaov% 1.90 lrn/cf 0.62 tM 0.0 tL 0.0 +TN180_Z16_off.log Z16 cpu 2452.6 confl 5145682 us/cf 476.6 lkp/cf 720 p/cf 25 look/cf 1.40 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.45 tM 0.0 tL 0.0 +TN216_X16_auto.log X16 cpu 1176.7 confl 2644995 us/cf 444.9 lkp/cf 897 p/cf 27 look/cf 1.35 ovp/cf 0.107 ovpL/cf 0.481 ovcf% 0.51 anaov% 1.72 lrn/cf 0.59 tM 0.0 tL 0.0 +TN216_X16_off.log X16 cpu 1259.6 confl 2801124 us/cf 449.7 lkp/cf 897 p/cf 27 look/cf 1.36 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.61 tM 0.0 tL 0.0 +TN216_Z16_auto.log Z16 cpu 3149.0 confl 5272857 us/cf 597.2 lkp/cf 849 p/cf 26 look/cf 1.35 ovp/cf 0.101 ovpL/cf 0.375 ovcf% 0.37 anaov% 1.65 lrn/cf 0.60 tM 0.0 tL 0.0 +TN216_Z16_off.log Z16 cpu 1983.6 confl 3969629 us/cf 499.7 lkp/cf 835 p/cf 26 look/cf 1.35 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.60 tM 0.0 tL 0.0 +TN216_Z16_v1.log Z16 cpu 2803.3 confl 4690900 us/cf 597.6 lkp/cf 868 p/cf 27 look/cf 1.34 ovp/cf 0.094 ovpL/cf 0.000 ovcf% 0.11 anaov% 1.86 lrn/cf 0.70 tM 0.0 tL 0.0 +TN216_Z16_v2.log Z16 cpu 2890.4 confl 4746245 us/cf 609.0 lkp/cf 856 p/cf 26 look/cf 1.34 ovp/cf 0.000 ovpL/cf 0.201 ovcf% 0.27 anaov% 0.00 lrn/cf 0.60 tM 0.0 tL 0.0 +TN216_Z17_auto.log Z17 cpu 7716.9 confl 9352254 us/cf 825.1 lkp/cf 854 p/cf 27 look/cf 1.35 ovp/cf 0.128 ovpL/cf 0.446 ovcf% 0.48 anaov% 2.03 lrn/cf 0.76 tM 0.0 tL 0.0 +TN216_Z17_off.log Z17 cpu 4202.8 confl 6795658 us/cf 618.5 lkp/cf 846 p/cf 26 look/cf 1.36 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.57 tM 0.0 tL 0.0 +TN250_X14_auto.log X14 cpu 544.8 confl 1461048 us/cf 372.8 lkp/cf 1076 p/cf 32 look/cf 1.32 ovp/cf 0.098 ovpL/cf 0.555 ovcf% 0.57 anaov% 1.12 lrn/cf 0.69 tM 0.0 tL 0.0 +TN250_X14_off.log X14 cpu 662.4 confl 1802470 us/cf 367.5 lkp/cf 1047 p/cf 30 look/cf 1.32 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.60 tM 0.0 tL 0.0 +BB288_X16_v1.log X16 cpu 11.6 confl 44944 us/cf 258.5 lkp/cf 1561 p/cf 75 look/cf 1.74 ovp/cf 0.479 ovpL/cf 0.000 ovcf% 0.16 anaov% 1.53 lrn/cf 0.30 tM 0.0 tL 0.0 +BB288_X16_v2.log X16 cpu 11.5 confl 44028 us/cf 262.0 lkp/cf 1551 p/cf 73 look/cf 1.72 ovp/cf 0.000 ovpL/cf 0.656 ovcf% 2.82 anaov% 0.00 lrn/cf 0.24 tM 0.0 tL 0.0 +LP544_X10_v1.log X10 cpu 4.5 confl 6545 us/cf 693.0 lkp/cf 5205 p/cf 150 look/cf 1.72 ovp/cf 0.018 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.01 lrn/cf 0.76 tM 0.0 tL 0.0 +LP544_X10_v2.log X10 cpu 5.0 confl 7666 us/cf 650.3 lkp/cf 4544 p/cf 141 look/cf 1.69 ovp/cf 0.000 ovpL/cf 0.077 ovcf% 0.34 anaov% 0.00 lrn/cf 0.83 tM 0.0 tL 0.0 +TN144_X12_v1.log X12 cpu 49.4 confl 287631 us/cf 171.6 lkp/cf 535 p/cf 25 look/cf 1.37 ovp/cf 0.064 ovpL/cf 0.000 ovcf% 0.09 anaov% 1.02 lrn/cf 0.87 tM 0.0 tL 0.0 +TN144_X12_v2.log X12 cpu 47.7 confl 279209 us/cf 171.0 lkp/cf 530 p/cf 25 look/cf 1.38 ovp/cf 0.000 ovpL/cf 0.254 ovcf% 0.41 anaov% 0.00 lrn/cf 0.82 tM 0.0 tL 0.0 +TN144_Z12_v1.log Z12 cpu 37.8 confl 238696 us/cf 158.3 lkp/cf 509 p/cf 24 look/cf 1.38 ovp/cf 0.070 ovpL/cf 0.000 ovcf% 0.07 anaov% 1.13 lrn/cf 0.99 tM 0.0 tL 0.0 +TN144_Z12_v2.log Z12 cpu 37.0 confl 239405 us/cf 154.4 lkp/cf 514 p/cf 24 look/cf 1.38 ovp/cf 0.000 ovpL/cf 0.242 ovcf% 0.36 anaov% 0.00 lrn/cf 0.86 tM 0.0 tL 0.0 +TN250_X14_even.log X14 cpu 587.9 confl 1567270 us/cf 375.1 lkp/cf 1060 p/cf 30 look/cf 1.32 ovp/cf 0.045 ovpL/cf 0.249 ovcf% 0.23 anaov% 0.41 lrn/cf 0.59 tM 0.0 tL 0.0 +TN250_X14_odd.log X14 cpu 710.9 confl 1813275 us/cf 392.1 lkp/cf 1057 p/cf 30 look/cf 1.31 ovp/cf 0.042 ovpL/cf 0.306 ovcf% 0.33 anaov% 0.59 lrn/cf 0.65 tM 0.0 tL 0.0 +TN250_Z14_auto.log Z14 cpu 908.6 confl 2156967 us/cf 421.2 lkp/cf 1006 p/cf 28 look/cf 1.32 ovp/cf 0.067 ovpL/cf 0.415 ovcf% 0.47 anaov% 0.98 lrn/cf 0.62 tM 0.0 tL 0.0 +TN250_Z14_even.log Z14 cpu 779.5 confl 1912573 us/cf 407.6 lkp/cf 1010 p/cf 30 look/cf 1.33 ovp/cf 0.064 ovpL/cf 0.374 ovcf% 0.40 anaov% 0.81 lrn/cf 0.63 tM 0.0 tL 0.0 +TN250_Z14_odd.log Z14 cpu 976.7 confl 2393795 us/cf 408.0 lkp/cf 1010 p/cf 28 look/cf 1.32 ovp/cf 0.011 ovpL/cf 0.090 ovcf% 0.11 anaov% 0.23 lrn/cf 0.52 tM 0.0 tL 0.0 +TN250_Z14_off.log Z14 cpu 854.2 confl 2229994 us/cf 383.1 lkp/cf 995 p/cf 29 look/cf 1.33 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.56 tM 0.0 tL 0.0 +TN144_X12_nosb_auto.log X12 cpu 101.0 confl 534147 us/cf 189.1 lkp/cf 519 p/cf 23 look/cf 1.38 ovp/cf 0.077 ovpL/cf 0.321 ovcf% 0.34 anaov% 1.28 lrn/cf 0.99 tM 0.0 tL 0.0 +TN144_X12_nosb_off.log X12 cpu 90.7 confl 516142 us/cf 175.8 lkp/cf 527 p/cf 23 look/cf 1.39 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.80 tM 0.0 tL 0.0 +TN144_Z12_nosb_auto.log Z12 cpu 94.2 confl 516403 us/cf 182.4 lkp/cf 511 p/cf 22 look/cf 1.38 ovp/cf 0.068 ovpL/cf 0.319 ovcf% 0.28 anaov% 1.24 lrn/cf 0.95 tM 0.0 tL 0.0 +TN144_Z12_nosb_off.log Z12 cpu 88.7 confl 536317 us/cf 165.4 lkp/cf 519 p/cf 22 look/cf 1.38 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.77 tM 0.0 tL 0.0 +BB288_X16_v4.log X16 cpu 11.5 confl 41850 us/cf 274.7 lkp/cf 1585 p/cf 76 look/cf 1.75 ovp/cf 0.450 ovpL/cf 1.287 ovcf% 0.79 anaov% 1.36 lrn/cf 0.30 tM 0.0 tL 0.0 +TN144_X12_v4.log X12 cpu 60.8 confl 316859 us/cf 191.9 lkp/cf 539 p/cf 25 look/cf 1.38 ovp/cf 0.057 ovpL/cf 0.277 ovcf% 0.26 anaov% 1.04 lrn/cf 0.92 tM 0.0 tL 0.0 +TN144_Z12_v4.log Z12 cpu 52.5 confl 285469 us/cf 183.8 lkp/cf 522 p/cf 24 look/cf 1.38 ovp/cf 0.061 ovpL/cf 0.307 ovcf% 0.28 anaov% 1.15 lrn/cf 0.98 tM 0.0 tL 0.0 +TN_180_2_17_X12_card-mto_aut X12 cpu 48.8 confl 214230 us/cf 227.6 lkp/cf 670 p/cf 28 look/cf 1.35 ovp/cf 0.103 ovpL/cf 0.334 ovcf% 0.36 anaov% 1.19 lrn/cf 0.96 tM 0.0 tL 0.0 +TN_180_2_17_X12_card-mto_off X12 cpu 48.1 confl 241933 us/cf 199.0 lkp/cf 678 p/cf 27 look/cf 1.34 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.87 tM 0.0 tL 0.0 +TN_180_2_17_Z12_card-mto_aut Z12 cpu 31.4 confl 162350 us/cf 193.6 lkp/cf 668 p/cf 28 look/cf 1.33 ovp/cf 0.083 ovpL/cf 0.358 ovcf% 0.28 anaov% 0.85 lrn/cf 1.01 tM 0.0 tL 0.0 +TN_180_2_17_Z12_card-mto_off Z12 cpu 30.6 confl 169319 us/cf 180.6 lkp/cf 673 p/cf 29 look/cf 1.34 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 1.20 tM 0.0 tL 0.0 +TN_216_4_18_X12_no-card_auto X12 cpu 42.1 confl 175205 us/cf 240.1 lkp/cf 856 p/cf 32 look/cf 1.31 ovp/cf 0.064 ovpL/cf 0.330 ovcf% 0.34 anaov% 0.79 lrn/cf 0.95 tM 0.0 tL 0.0 +TN_216_4_18_X12_no-card_off. X12 cpu 49.9 confl 211134 us/cf 236.4 lkp/cf 856 p/cf 31 look/cf 1.31 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.94 tM 0.0 tL 0.0 +TN_216_4_18_Z12_no-card_auto Z12 cpu 31.5 confl 136347 us/cf 231.0 lkp/cf 825 p/cf 30 look/cf 1.30 ovp/cf 0.083 ovpL/cf 0.343 ovcf% 0.36 anaov% 0.86 lrn/cf 1.16 tM 0.0 tL 0.0 +TN_216_4_18_Z12_no-card_off. Z12 cpu 29.8 confl 138731 us/cf 215.1 lkp/cf 823 p/cf 30 look/cf 1.30 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.91 tM 0.0 tL 0.0 +TN180_X16_mto_nosb_auto.log X16 cpu 10296.3 confl 15888426 us/cf 648.0 lkp/cf 620 p/cf 24 look/cf 1.39 ovp/cf 0.146 ovpL/cf 0.418 ovcf% 0.40 anaov% 2.14 lrn/cf 0.85 tM 0.0 tL 0.0 +TN216_X16_v1.log X16 cpu 1440.9 confl 2930061 us/cf 491.8 lkp/cf 888 p/cf 27 look/cf 1.35 ovp/cf 0.109 ovpL/cf 0.000 ovcf% 0.13 anaov% 2.06 lrn/cf 0.63 tM 0.0 tL 0.0 +TN216_X17_v1.log X17 cpu 2495.6 confl 4169661 us/cf 598.5 lkp/cf 936 p/cf 27 look/cf 1.36 ovp/cf 0.087 ovpL/cf 0.000 ovcf% 0.14 anaov% 2.30 lrn/cf 0.70 tM 0.0 tL 0.0 +TN216_Z16_nosb_auto.log Z16 cpu 4682.5 confl 7220572 us/cf 648.5 lkp/cf 866 p/cf 25 look/cf 1.34 ovp/cf 0.093 ovpL/cf 0.464 ovcf% 0.62 anaov% 2.16 lrn/cf 0.85 tM 0.0 tL 0.0 +TN216_Z16_nosb_off.log Z16 cpu 3944.8 confl 6598390 us/cf 597.8 lkp/cf 897 p/cf 25 look/cf 1.34 ovp/cf 0.000 ovpL/cf 0.000 ovcf% 0.00 anaov% 0.00 lrn/cf 0.61 tM 0.0 tL 0.0 +TN216_Z17_v1.log Z17 cpu 7920.7 confl 9924089 us/cf 798.1 lkp/cf 841 p/cf 27 look/cf 1.37 ovp/cf 0.148 ovpL/cf 0.000 ovcf% 0.14 anaov% 2.02 lrn/cf 0.86 tM 0.0 tL 0.0 diff --git a/optimization/experiments/GH-218/diag/pilot_cap_panel.txt b/optimization/experiments/GH-218/diag/pilot_cap_panel.txt new file mode 100644 index 00000000..d808d940 --- /dev/null +++ b/optimization/experiments/GH-218/diag/pilot_cap_panel.txt @@ -0,0 +1,26 @@ +== cap 12 +TN_180_2_17_X12_card-mto n=3 confl ratios 0.89 0.97 0.89 median 0.886 | cpu median 0.912 +TN_180_2_17_X12_no-card n=3 confl ratios 1.02 0.96 0.90 median 0.957 | cpu median 1.023 +TN_180_2_17_Z12_card-mto n=3 confl ratios 0.96 0.95 1.02 median 0.959 | cpu median 0.970 +TN_180_2_17_Z12_no-card n=3 confl ratios 1.03 0.97 0.95 median 0.967 | cpu median 1.023 +TN_216_4_18_X12_card-mto n=5 confl ratios 0.90 0.96 0.94 0.98 0.96 median 0.956 | cpu median 0.951 +TN_216_4_18_X12_no-card n=5 confl ratios 0.83 0.84 1.01 0.90 0.86 median 0.863 | cpu median 0.898 +TN_216_4_18_Z12_card-mto n=5 confl ratios 1.00 1.06 1.09 1.19 0.86 median 1.057 | cpu median 1.120 +TN_216_4_18_Z12_no-card n=5 confl ratios 0.98 1.13 1.05 0.91 1.09 median 1.055 | cpu median 1.102 +== cap 10/11 +TN_180_2_17_X10_card-mto n=3 confl ratios 0.91 0.87 0.99 median 0.906 | cpu median 0.929 +TN_180_2_17_X10_no-card n=3 confl ratios 0.92 1.10 1.05 median 1.055 | cpu median 1.132 +TN_180_2_17_X11_card-mto n=3 confl ratios 0.97 1.00 0.92 median 0.969 | cpu median 1.028 +TN_180_2_17_X11_no-card n=3 confl ratios 0.93 0.96 1.06 median 0.959 | cpu median 1.006 +TN_180_2_17_Z10_card-mto n=3 confl ratios 1.03 1.20 1.05 median 1.050 | cpu median 1.178 +TN_180_2_17_Z10_no-card n=3 confl ratios 0.97 0.98 1.00 median 0.979 | cpu median 1.010 +TN_180_2_17_Z11_card-mto n=3 confl ratios 0.97 0.92 0.95 median 0.953 | cpu median 1.004 +TN_180_2_17_Z11_no-card n=3 confl ratios 0.93 0.83 1.10 median 0.926 | cpu median 0.951 +TN_216_4_18_X10_card-mto n=5 confl ratios 0.94 0.96 0.91 1.13 0.94 median 0.941 | cpu median 0.993 +TN_216_4_18_X10_no-card n=5 confl ratios 0.98 0.97 0.93 1.23 0.89 median 0.966 | cpu median 0.979 +TN_216_4_18_X11_card-mto n=5 confl ratios 0.86 0.97 1.06 1.06 0.92 median 0.974 | cpu median 0.978 +TN_216_4_18_X11_no-card n=5 confl ratios 0.97 1.10 0.91 1.09 0.86 median 0.973 | cpu median 1.032 +TN_216_4_18_Z10_card-mto n=5 confl ratios 0.89 0.99 1.16 0.76 0.88 median 0.890 | cpu median 0.982 +TN_216_4_18_Z10_no-card n=5 confl ratios 1.23 0.79 0.99 1.11 0.98 median 0.992 | cpu median 1.067 +TN_216_4_18_Z11_card-mto n=5 confl ratios 0.89 0.90 1.06 1.12 1.02 median 1.021 | cpu median 1.104 +TN_216_4_18_Z11_no-card n=5 confl ratios 1.20 1.06 0.74 0.88 1.02 median 1.023 | cpu median 1.067 diff --git a/optimization/experiments/GH-218/diag/pilot_seed_panel_d7.txt b/optimization/experiments/GH-218/diag/pilot_seed_panel_d7.txt new file mode 100644 index 00000000..766e3e58 --- /dev/null +++ b/optimization/experiments/GH-218/diag/pilot_seed_panel_d7.txt @@ -0,0 +1,4 @@ +TN108_X11 n=5 confl ratios 0.92 0.81 0.84 0.96 1.11 median 0.924 | cpu median 1.009 +TN108_Z11 n=5 confl ratios 0.88 0.80 0.95 0.97 1.09 median 0.953 | cpu median 0.988 +TN144_X12 n=4 confl ratios 0.91 1.01 0.99 0.88 median 0.950 | cpu median 0.981 +TN144_Z12 n=4 confl ratios 1.03 0.97 0.97 0.85 median 0.969 | cpu median 0.981 diff --git a/optimization/experiments/GH-218/runner/c4dist.py b/optimization/experiments/GH-218/runner/c4dist.py new file mode 100644 index 00000000..1d08d665 --- /dev/null +++ b/optimization/experiments/GH-218/runner/c4dist.py @@ -0,0 +1,13 @@ +import sys,glob,collections,os +def load(p): return [[int(x) for x in l.split()] for l in open(p) if l.strip() and l.strip()[0] in "01"] +for hx in sorted(glob.glob('gh-stabov/data/matrices/tier[1-5]/*_Hx.txt')): + stem=os.path.basename(hx)[:-7]; p=hx[:-7] + out=[] + for H in ('Hx','Hz'): + S=[frozenset(j for j,v in enumerate(r) if v) for r in load(p+'_'+H+'.txt') if any(r)] + d=collections.Counter() + for i,s in enumerate(S): + c4=sum((lambda o: o*(o-1)//2)(len(s&t)) for k,t in enumerate(S) if k!=i) + d[(len(s),c4)]+=1 + out.append(H+' '+' '.join('w%d:c%d x%d'%(w,c,n) for (w,c),n in sorted(d.items()))) + print(stem,' | '.join(out)) diff --git a/optimization/experiments/GH-218/runner/diagtab.py b/optimization/experiments/GH-218/runner/diagtab.py new file mode 100644 index 00000000..8b49b2a0 --- /dev/null +++ b/optimization/experiments/GH-218/runner/diagtab.py @@ -0,0 +1,12 @@ +import sys,re,glob,os +for f in sorted(sum([glob.glob(a) for a in sys.argv[1:]],[])): + for line in open(f,errors='replace'): + if 'c DIAG ' not in line or 'DIAGPROBE' in line: continue + m=re.search(r'c DIAG (\w) cap (\d+) (\w+): (.*)',line) + if not m: continue + kv=dict(zip(m.group(4).split()[0::2],m.group(4).split()[1::2])) + g=lambda k: float(kv.get(k,0)) + c=max(g('conflicts'),1) + print('%-28s %s%-3s cpu %8.1f confl %9d us/cf %6.1f lkp/cf %6.0f p/cf %5.0f look/cf %4.2f ovp/cf %5.3f ovpL/cf %5.3f ovcf%% %5.2f anaov%% %5.2f lrn/cf %5.2f tM %6.1f tL %6.1f' % ( + os.path.basename(f)[:28], m.group(1), m.group(2), g('cpu'), c, 1e6*g('cpu')/c, g('lkprops')/c, g('props')/c, g('lookahead')/c, + (g('ovprops')-g('ovpropsL'))/c, g('ovpropsL')/c, 100*g('ovconfl')/c, 100*g('anaov')/max(g('anares'),1), g('learntlits')/c, g('tM'), g('tL'))) diff --git a/optimization/experiments/GH-218/runner/ident.sh b/optimization/experiments/GH-218/runner/ident.sh new file mode 100644 index 00000000..8350b53b --- /dev/null +++ b/optimization/experiments/GH-218/runner/ident.sh @@ -0,0 +1,18 @@ +#!/bin/bash +# ident.sh CORE TIERGLOB...: answers + identity (stdout and FRONTIER stderr) main vs cand default vs cand -stab-overlap-c4=off +core=$1; shift +cd ~/mac-agent-20261009/gh218-60fec5b +M=~/mac-agent-20261009/frozen/server-main-02879a93/distqldpc; C=~/mac-agent-20261009/frozen/server-gh218-60fec5b/distqldpc +O=~/mac-agent-20261009/gh218-runs/ident; mkdir -p $O +for t in "$@"; do for hx in data/matrices/$t/*_Hx.txt; do stem=${hx%_Hx.txt}; b=$(basename $stem); for md in -no-card -card-mto; do + for arm in main cand c4off; do + bin=$C; extra=""; [ $arm = main ] && bin=$M; [ $arm = c4off ] && extra="-stab-overlap-c4=off" + taskset -c $core prlimit --as=4294967296 -- $bin $md $extra -frontier-stats -cpu-lim=600 $stem > $O/$b$md.$arm.out 2> $O/$b$md.$arm.err < /dev/null + grep -E "FRONTIER|OVERLAP" $O/$b$md.$arm.err > $O/$b$md.$arm.fr + done + ans=$(grep "^o " $O/$b$md.cand.out); want=${b##*_} + s1=$(cmp -s $O/$b$md.main.out $O/$b$md.cand.out && echo same || echo DIFF); s2=$(cmp -s $O/$b$md.main.out $O/$b$md.c4off.out && echo same || echo DIFF) + f1=$(cmp -s $O/$b$md.main.fr $O/$b$md.cand.fr && echo same || echo DIFF); f2=$(cmp -s $O/$b$md.main.fr $O/$b$md.c4off.fr && echo same || echo DIFF) + echo "$b $md answer[$ans want $want] stdout cand:$s1 c4off:$s2 probes cand:$f1 c4off:$f2" +done; done; done +echo DONE diff --git a/optimization/experiments/GH-218/runner/mkp3.sh b/optimization/experiments/GH-218/runner/mkp3.sh new file mode 100644 index 00000000..e2f24daf --- /dev/null +++ b/optimization/experiments/GH-218/runner/mkp3.sh @@ -0,0 +1,13 @@ +#!/bin/bash +# build pilot-cap panel jobs (cap 10 and 11) on cores given as args +cd ~/mac-agent-20261009/gh218-runs && mkdir -p p3 +B=~/mac-agent-20261009/frozen/server-gh218-diag3/distqldpc; T5=data/matrices/tier5 +cores=("$@"); nc=${#cores[@]}; i=0 +for c in "${cores[@]}"; do rm -f jp3_$c.txt; done +for cap in 10 11; do for st in TN_216_4_18 TN_180_2_17; do for md in no-card card-mto; do for s in 0 1 2 3 4; do for h in X Z; do for a in auto off; do + [ $st = TN_180_2_17 ] && [ $s -ge 3 ] && continue + c=${cores[$((i % nc))]}; i=$((i+1)); o=""; [ $a = off ] && o="-stab-overlap=off" + echo "$c p3/${st}_${h}${cap}_${md}_s${s}_$a.log $B DQ_DIAG=1|DQ_DIAG_PROBE=$h:$cap:9 -$md -seed=$s $o -frontier-stats -cpu-lim=3600 $T5/$st" >> jp3_$c.txt +done; done; done; done; done; done +for c in "${cores[@]}"; do setsid nohup ./seq.sh jp3_$c.txt >/dev/null 2>&1 < /dev/null & done +echo jobs $i diff --git a/optimization/experiments/GH-218/runner/nbr.py b/optimization/experiments/GH-218/runner/nbr.py new file mode 100644 index 00000000..1512ae02 --- /dev/null +++ b/optimization/experiments/GH-218/runner/nbr.py @@ -0,0 +1,13 @@ +import sys,glob,collections,os +def load(p): return [[int(x) for x in l.split()] for l in open(p) if l.strip() and l.strip()[0] in "01"] +for stem in sys.argv[1:]: + p=glob.glob('gh-stabov/data/matrices/tier*/'+stem+'_Hx.txt')[0][:-7] + out=[] + for H in ('Hx','Hz'): + S=[frozenset(j for j,v in enumerate(r) if v) for r in load(p+'_'+H+'.txt') if any(r)] + d=collections.Counter() + for i,s in enumerate(S): + ov=collections.Counter(len(s&t) for k,t in enumerate(S) if k!=i and len(s&t)>=2) + d[(len(s),tuple(sorted(ov.items())))]+=1 + out.append(H+' '+' '.join('w%d:%s x%d'%(w,dict(o),n) for (w,o),n in sorted(d.items()))) + print(stem,' | '.join(out)) diff --git a/optimization/experiments/GH-218/runner/pair.py b/optimization/experiments/GH-218/runner/pair.py new file mode 100644 index 00000000..6f737525 --- /dev/null +++ b/optimization/experiments/GH-218/runner/pair.py @@ -0,0 +1,15 @@ +import sys,re,glob,os,collections,statistics as st +R={} +for f in glob.glob(sys.argv[1]): + b=os.path.basename(f)[:-4] + for l in open(f,errors='replace'): + m=re.search(r'c DIAG \w cap \d+ \w+: cpu ([\d.]+) conflicts (\d+)',l) + if m: R[b]=(float(m.group(1)),int(m.group(2))) +g=collections.defaultdict(list) +for b,(cpu,c) in sorted(R.items()): + if b.endswith('_auto'): + o=b[:-5]+'_off' + if o in R: + key=re.sub(r'_s\d+','',b[:-5]); g[key].append((c/R[o][1], cpu/R[o][0], b)) +for k,v in sorted(g.items()): + print(k, 'n=%d'%len(v), 'confl ratios', ' '.join('%.2f'%x[0] for x in v), 'median %.3f'%st.median(x[0] for x in v), '| cpu median %.3f'%st.median(x[1] for x in v)) diff --git a/optimization/experiments/GH-218/runner/rowstats.py b/optimization/experiments/GH-218/runner/rowstats.py new file mode 100644 index 00000000..e91efa19 --- /dev/null +++ b/optimization/experiments/GH-218/runner/rowstats.py @@ -0,0 +1,27 @@ +import sys,glob,os,collections +def load(p): + rows=[] + for line in open(p): + line=line.strip() + if not line or line[0] in '#c%': continue + t=line.replace(',',' ').split() + if len(t)==1 and len(t[0])>1 and set(t[0])<=set('01'): t=list(t[0]) + rows.append([int(x) for x in t]) + return rows +for d in sorted(glob.glob(sys.argv[1]+'/tier*')): + for hx in sorted(glob.glob(d+'/*_Hx.txt')): + stem=os.path.basename(hx)[:-7] + out=[os.path.basename(d),stem] + for H in ('Hx','Hz'): + M=load(d+'/'+stem+'_'+H+'.txt') + M=[r for r in M if any(r)] + rw=collections.Counter(sum(r) for r in M) + n=len(M[0]); cw=collections.Counter(sum(M[i][j] for i in range(len(M))) for j in range(n)) + # 4-cycles per row: pairs of rows sharing >=2 cols + S=[set(j for j,v in enumerate(r) if v) for r in M] + c4=0 + for i in range(len(S)): + for k in range(i+1,len(S)): + s=len(S[i]&S[k]); c4+=s*(s-1)//2 + out.append('%s rw%s cw%s c4/row%.2f'%(H,dict(rw),dict(cw),2*c4/len(S))) + print(' | '.join(out)) diff --git a/optimization/experiments/GH-218/runner/run1.sh b/optimization/experiments/GH-218/runner/run1.sh new file mode 100755 index 00000000..ebac1108 --- /dev/null +++ b/optimization/experiments/GH-218/runner/run1.sh @@ -0,0 +1,8 @@ +#!/bin/bash +# usage: run1.sh CORE OUTNAME BIN "ENV" ARGS... ; runs in gh218-diag worktree (data path) +core=$1; out=$(readlink -f $2); bin=$3; envs=$4; shift 4 +cd ~/mac-agent-20261009/gh218-diag +start=$(date +%s.%N) +echo "# start $start core $core env $envs cmd $bin $*" > $out +env $envs taskset -c $core prlimit --as=4294967296 -- /usr/bin/time -f "TIME %e %U %M" $bin "$@" < /dev/null >> $out 2>&1 +echo "# rc $? end $(date +%s.%N)" >> $out diff --git a/optimization/experiments/GH-218/runner/seq.sh b/optimization/experiments/GH-218/runner/seq.sh new file mode 100755 index 00000000..67b9b521 --- /dev/null +++ b/optimization/experiments/GH-218/runner/seq.sh @@ -0,0 +1,6 @@ +#!/bin/bash +# seq.sh JOBFILE : each line "CORE OUT BIN ENV ARGS..." with ENV quoted as one token using | for spaces +while read -r core out bin envs rest; do + [ -z "$core" ] && continue + ./run1.sh $core $out $bin "${envs//|/ }" $rest +done < $1 diff --git a/optimization/experiments/GH-218/runner/t5tab.py b/optimization/experiments/GH-218/runner/t5tab.py new file mode 100644 index 00000000..4ebeb5b5 --- /dev/null +++ b/optimization/experiments/GH-218/runner/t5tab.py @@ -0,0 +1,11 @@ +import sys,re,glob,os +rows=[] +for f in sorted(glob.glob(sys.argv[1])): + b=os.path.basename(f)[:-4]; L=open(f,errors='replace').read() + done='# rc' in L + m=re.search(r'TIME ([\d.]+) ([\d.]+) (\d+)',L); wall=float(m.group(1)) if m else None + d=re.findall(r'c d : (\S+)',L); d=d[-1] if d else '-' + lb=re.findall(r'c d_lb: (\d+)',L); lb=lb[-1] if lb else '-' + pil=' '.join('%s:%s(%s)'%(x[0],x[2],x[1]) for x in re.findall(r'OVERLAP-PILOT (\w) cap \d+: .* median ([\d.]+) -> (\w+)',L)) + probes=' '.join('%s%s:%.2fM'%(x[0],x[1],int(x[2])/1e6) for x in re.findall(r'FRONTIER (\w) cap (\d+) \w+: conflicts (\d+)',L) if int(x[1])>=12) + print('%-38s %-4s d=%-3s lb=%-3s wall=%-8s %s | %s'%(b,'done' if done else 'run',d,lb,'%.0f'%wall if wall else '-',pil,probes)) diff --git a/optimization/experiments/GH-218/runner/u0check.sh b/optimization/experiments/GH-218/runner/u0check.sh new file mode 100644 index 00000000..4ef6ecf1 --- /dev/null +++ b/optimization/experiments/GH-218/runner/u0check.sh @@ -0,0 +1,11 @@ +#!/bin/bash +# u0check.sh CORE: ub-pre U0 per seed/mode for the Tier 1-4 TN codes (no probe reaches cap 16 iff U0 <= 16... checked: U0 = d) +core=$1; cd ~/mac-agent-20261009/gh218-60fec5b +C=~/mac-agent-20261009/frozen/server-gh218-60fec5b/distqldpc +for p in tier2/TN_108_2_12 tier2/TN_200_10_10 tier3/TN_144_2_13 tier4/TN_250_10_15; do for md in -no-card -card-mto; do for s in 0 1 2 3 4; do + out=$(taskset -c $core prlimit --as=4294967296 -- $C $md -seed=$s -v -cpu-lim=75 data/matrices/$p 2>&1 < /dev/null | grep -E "^c ub-pre: |c CSS interleave: . half cap|OVERLAP-PILOT|stab-overlap pilot" | head -12) + u0=$(grep -o "^c ub-pre: U0 after [^)]*); [0-9]*\|^c ub-pre: .*" <<<"$out" | head -1 | cut -c1-120) + caps=$(grep -o "half cap [0-9]*" <<<"$out" | awk '{print $3}' | tr '\n' ',') + pil=$(grep -c "pilot" <<<"$out") + echo "$p $md s$s | $u0 | caps $caps | pilot_lines $pil" +done; done; done; echo DONE diff --git a/src/core/distqldpc.cc b/src/core/distqldpc.cc index a308a959..9f835b53 100644 --- a/src/core/distqldpc.cc +++ b/src/core/distqldpc.cc @@ -934,6 +934,29 @@ static int g_stab_overlap_enc = 3; /* -stab-overlap-enc=native|bin|seq|cla static int g_stab_overlap_mutant = 0; /* test only (no flag): 1 = limit floor(|g|/2) - 1 (cuts minimum logicals); 2 = the half's parity rows (Hpar) used as g without the GF(2) check */ static const double STAB_OVL_BIN_MAX = 126.0; /* auto: binomial up to |g| = 9 (C(9,5) = 126), counter above */ +/* GH-218: dense overlap rows. A verified row g is "dense" if it lies on more than g_stab_overlap_c4 Tanner-graph 4-cycles + * of the same-type stabilizer matrix, c4(g) = sum over the other distinct rows g' of C(|g & g'|, 2) (the 4-cycles through + * g's check node). Sparse rows are always used (as in GH-148). The dense rows of a half are used as in GH-148 until the + * half's first probe with cap >= P' + 4, P' = max(pilot cap, the half's lb, the cap from which the -stab-overlap ratio + * activates every dense row: 10 for weight 9 under auto); from that probe on they are dropped (default), or, with + * -stab-overlap-pilot=N > 0 (opt-in), a pilot decides once per half: the probe "weight <= P'?" (first solution stops it) + * is run with and without the dense rows for N solver seeds (the run's seed + 0, 1, ...) and the dense rows stay iff the + * median of conflicts(with) / conflicts(without) is <= 1 (deterministic for a given seed). Every subset of the verified + * rows is sound (each row alone keeps every minimum-weight element of F), so neither rule changes a probe answer; pilot + * probes only decide. Measured in GH-218: BB / LP / GB rows have c4 <= 4 (never dense: GH-148's search); every weight-9 TN + * row has c4 >= 12. On them the rows' effect at caps 16-17 is systematic per code and half (TN_216 Z half 1.03-1.54x the + * conflicts on all 10 seed/mode pairs, the GH-148 regression; TN_180 X half 0.48-0.66x on 3 seeds), while at caps 10-12 + * it is near neutral and does not predict it (TN_216 Z at cap 12 over 10 seeds: median 0.97 / 0.92), so the default + * drops them and the pilot stays opt-in. Below cap 16 (all TN codes of tiers 1-4) the search is GH-148's. -1 = no + * classification (every verified row in every probe: GH-148's search, byte for byte). */ +static const int STAB_OVL_C4_DEFAULT = 11; +static int g_stab_overlap_c4 = STAB_OVL_C4_DEFAULT; /* -stab-overlap-c4=N|off (default 11) */ +static int g_stab_overlap_pilot = 0; /* -stab-overlap-pilot=N seed pairs (default 0 = the dense rows are + dropped from that probe on, without a pilot; N > 0 opt-in) */ +static uint64_t g_stab_overlap_pilot_cap = 12; /* -stab-overlap-pilot-cap=P (default 12); the pilot asks + "weight <= max(P, lb)?" */ +static uint64_t g_stab_overlap_pilot_margin = 4; /* pilot before the first probe with cap >= pilot cap + margin + (no flag; tests lower it to reach the pilot on small codes) */ typedef std::vector > OvlRows; @@ -944,6 +967,7 @@ struct OvlInfo { int duplicates; long long clauses, auxvars; /* per probe */ int bin_rows, seq_rows, native_rows; + int c4_gated; /* GH-218: dense verified rows (more than g_stab_overlap_c4 4-cycles) */ std::map weights; /* |g| -> rows */ }; @@ -966,11 +990,16 @@ static bool ovl_use_binomial(int w, int k) { return binom_d(w, k + 1) <= STAB_OVL_BIN_MAX; } -/* Rows g of Smat with Hpar g = 0 and Glog g = 0 (GF(2), via the column incidence of Hpar and Glog). */ -static OvlRows stab_overlap_rows(const Matrix& Hpar, const Matrix& Glog, const Matrix& Smat, OvlInfo& info) +/* Rows g of Smat with Hpar g = 0 and Glog g = 0 (GF(2), via the column incidence of Hpar and Glog). + * GH-218 (g_stab_overlap_c4 >= 0): with dense == NULL only the sparse rows are returned; otherwise every row is returned + * and (*dense)[i] = 1 marks the dense ones. */ +static OvlRows stab_overlap_rows(const Matrix& Hpar, const Matrix& Glog, const Matrix& Smat, OvlInfo& info, + std::vector* dense = NULL) { + if (dense) dense->clear(); info = OvlInfo(); info.candidates = info.kept = info.rejected = info.duplicates = info.bin_rows = info.seq_rows = info.native_rows = 0; + info.c4_gated = 0; info.clauses = info.auxvars = 0; OvlRows out; const int n = Hpar.cols; @@ -981,6 +1010,20 @@ static OvlRows stab_overlap_rows(const Matrix& Hpar, const Matrix& Glog, const M for (int r = 0; r < Glog.rows; r++) for (int c = 0; c < n; c++) if (getm(Glog, r, c)) colG[c].push_back(r); std::vector parH((size_t)Hpar.rows, 0), parG((size_t)Glog.rows, 0); std::set > seen; + /* GH-218: distinct nonzero rows of Src and their column incidence, for the 4-cycle gate */ + std::vector > srows; + std::vector > scol; + if (g_stab_overlap_c4 >= 0) { + std::set > distinct; + for (int r = 0; r < Src.rows; r++) { + std::vector g; + for (int c = 0; c < n; c++) if (getm(Src, r, c)) g.push_back(c); + if (!g.empty() && distinct.insert(g).second) srows.push_back(g); + } + scol.assign((size_t)n, std::vector()); + for (size_t r = 0; r < srows.size(); r++) for (size_t t = 0; t < srows[r].size(); t++) scol[(size_t)srows[r][t]].push_back((int)r); + } + std::vector shared(srows.size(), 0); for (int r = 0; r < Src.rows; r++) { std::vector g; for (int c = 0; c < n; c++) if (getm(Src, r, c)) g.push_back(c); @@ -1000,8 +1043,28 @@ static OvlRows stab_overlap_rows(const Matrix& Hpar, const Matrix& Glog, const M } if (!ok) { info.rejected++; continue; } if (!seen.insert(g).second) { info.duplicates++; continue; } + bool is_dense = false; + if (g_stab_overlap_c4 >= 0) { /* GH-218: c4(g) = sum over the other distinct rows of C(|g & g'|, 2) */ + std::vector touched; + for (size_t t = 0; t < g.size(); t++) + for (size_t u = 0; u < scol[(size_t)g[t]].size(); u++) { + const int q = scol[(size_t)g[t]][u]; + if (shared[(size_t)q]++ == 0) touched.push_back(q); + } + long long c4 = 0; + for (size_t u = 0; u < touched.size(); u++) { + const long long o = shared[(size_t)touched[u]]; + c4 += g_stab_overlap_mutant == 3 ? o : o * (o - 1) / 2; /* mutant 3 (test only): overlaps, not pairs */ + shared[(size_t)touched[u]] = 0; + } + const long long self = (long long)g.size(); /* g itself is one of the distinct rows: remove its own term */ + c4 -= g_stab_overlap_mutant == 3 ? self : self * (self - 1) / 2; + is_dense = c4 > g_stab_overlap_c4; + if (is_dense) { info.c4_gated++; if (!dense) continue; } + } const int w = (int)g.size(), k = ovl_limit(w); if (k >= w) continue; /* no constraint (cannot happen for w >= 1 with the true limit) */ + if (dense) dense->push_back(is_dense ? 1 : 0); info.kept++; info.weights[w]++; if (g_stab_overlap_enc == 3) { info.native_rows++; } @@ -1226,13 +1289,90 @@ struct CssHalf { bool par; /* GH-133: -oddcap-skip in force (all column weights of H odd): odd caps skipped */ bool pre; /* GH-144: ub is a verified -ub-pre finder word (not a solver solution); false without -ub-pre */ OvlRows ovl; /* GH-148: verified stabilizer rows for -stab-overlap (empty: no constraint, main's instance) */ + std::vector ovl_dense; /* GH-218: ovl_dense[r] = 1: row r is dense (pilot-controlled); empty: none */ + int ovl_dense_mode; /* GH-218: -1 undecided (dense rows used, GH-148), 1 kept by the pilot, 0 dropped */ }; +static HalfStatus run_css_half(CssHalf& h, uint64_t cap, bool first_only, int verb, int card_mode, + int pipe_w, uint64_t lb_cap, uint64_t ub_cap, bool hide_lb, uint64_t& value, + int dense_force = -2, uint64_t* conflicts_out = NULL); + +/* GH-218: the pilot cap of half h: max(-stab-overlap-pilot-cap, lb, the smallest cap at which every dense row is active + * under the -stab-overlap ratio), so that the two pilot probes differ exactly by the dense rows. */ +static uint64_t ovl_pilot_cap(const CssHalf& h) +{ + uint64_t P = g_stab_overlap_pilot_cap > h.lb ? g_stab_overlap_pilot_cap : h.lb; + for (size_t r = 0; r < h.ovl.size() && r < h.ovl_dense.size(); r++) { + if (!h.ovl_dense[r] || g_stab_overlap_ratio <= 0.0) continue; + const double need = g_stab_overlap_ratio * (double)(h.ovl[r].size() / 2 + 1); + uint64_t c = (uint64_t)need; + if ((double)c < need) c++; + if (c > P) P = c; + } + return P; +} + +/* GH-218: the pilot of half h (see g_stab_overlap_c4). Sets h.ovl_dense_mode to 0 or 1. */ +static void ovl_pilot(CssHalf& h, int verb, int card_mode) +{ + const uint64_t P = ovl_pilot_cap(h); + const uint64_t saved_seed = g_seed, saved_probes = h.probes, saved_conf = h.conflicts; + std::vector ratio; + std::string detail; + for (int i = 0; i < g_stab_overlap_pilot; i++) { + g_seed = saved_seed + (uint64_t)i; + uint64_t c[2] = {0, 0}, v = 0; + for (int with = 1; with >= 0; with--) + (void)run_css_half(h, P, true, 0, card_mode, -1, UINT64_MAX, UINT64_MAX, true, v, with, &c[with]); + ratio.push_back((double)c[1] / (double)(c[0] > 0 ? c[0] : 1)); + char buf[96]; + snprintf(buf, sizeof(buf), "%s seed %llu %llu/%llu", i ? "," : "", (unsigned long long)g_seed, (unsigned long long)c[1], + (unsigned long long)c[0]); + detail += buf; + } + g_seed = saved_seed; h.probes = saved_probes; h.conflicts = saved_conf; /* pilot work is not search work (GH-107 counters) */ + double med = 0.0; + if (!ratio.empty()) { + std::sort(ratio.begin(), ratio.end()); + const size_t m = ratio.size(); + med = m % 2 ? ratio[m / 2] : 0.5 * (ratio[m / 2 - 1] + ratio[m / 2]); + } + h.ovl_dense_mode = (!ratio.empty() && med <= 1.0) ? 1 : 0; + size_t nd = 0; + for (size_t r = 0; r < h.ovl_dense.size(); r++) nd += h.ovl_dense[r] ? 1 : 0; + if (verb > 0) { + printf("c stab-overlap pilot %s cap %llu (conflicts with/without %zu dense rows:%s): median ratio %.3f -> dense rows %s\n", + h.tag, (unsigned long long)P, nd, detail.c_str(), med, h.ovl_dense_mode ? "kept" : "dropped"); + fflush(stdout); + } + if (g_frontier_stats) { + fprintf(stderr, "c OVERLAP-PILOT %s cap %llu: dense_rows %zu%s median %.3f -> %s\n", h.tag, (unsigned long long)P, nd, + detail.c_str(), med, h.ovl_dense_mode ? "kept" : "dropped"); + fflush(stderr); + } +} + /* One oracle call on a half. cap: only solutions of weight <= cap are sought (strict). * first_only: stop at the first solution. Emitted bounds are capped/hidden as requested. */ static HalfStatus run_css_half(CssHalf& h, uint64_t cap, bool first_only, int verb, int card_mode, - int pipe_w, uint64_t lb_cap, uint64_t ub_cap, bool hide_lb, uint64_t& value) + int pipe_w, uint64_t lb_cap, uint64_t ub_cap, bool hide_lb, uint64_t& value, + int dense_force, uint64_t* conflicts_out) { + /* GH-218: dense_force -2 = a search probe (may trigger the half's pilot), 1 / 0 = pilot probe with / without the + * dense rows (no output, no pipe) */ + const bool pilot_probe = dense_force >= 0; + if (!pilot_probe && h.ovl_dense_mode < 0 && !h.ovl_dense.empty() && + cap >= ovl_pilot_cap(h) + g_stab_overlap_pilot_margin) { + if (g_stab_overlap_pilot > 0) ovl_pilot(h, verb, card_mode); + else { + h.ovl_dense_mode = 0; + size_t nd = 0; + for (size_t r = 0; r < h.ovl_dense.size(); r++) nd += h.ovl_dense[r] ? 1 : 0; + if (verb > 0) { printf("c stab-overlap %s: %zu dense rows dropped from cap %llu on\n", h.tag, nd, (unsigned long long)cap); fflush(stdout); } + if (g_frontier_stats) { fprintf(stderr, "c OVERLAP-DROP %s cap %llu: dense_rows %zu\n", h.tag, (unsigned long long)cap, nd); fflush(stderr); } + } + } + const bool use_dense = pilot_probe ? dense_force == 1 : h.ovl_dense_mode != 0; SimpSolver S; apply_maxsat_seed(S); /* GH-124: -seed=N (no-op for N = 0) */ std::vector aux; @@ -1240,7 +1380,8 @@ static HalfStatus run_css_half(CssHalf& h, uint64_t cap, bool first_only, int ve OvlRows ovl_active; /* GH-148: rows active in this probe (any subset of the verified rows is sound) */ if (!h.ovl.empty()) { for (size_t r = 0; r < h.ovl.size(); r++) - if (g_stab_overlap_ratio <= 0.0 || (double)cap >= g_stab_overlap_ratio * (double)(h.ovl[r].size() / 2 + 1)) + if ((g_stab_overlap_ratio <= 0.0 || (double)cap >= g_stab_overlap_ratio * (double)(h.ovl[r].size() / 2 + 1)) && + (use_dense || h.ovl_dense.empty() || !h.ovl_dense[r])) /* GH-218: dense rows only while kept/undecided */ ovl_active.push_back(h.ovl[r]); if (verb > 0) { printf("c stab-overlap %s cap %llu: %zu of %zu rows active (ratio %.2f)\n", h.tag, (unsigned long long)cap, @@ -1276,6 +1417,12 @@ static HalfStatus run_css_half(CssHalf& h, uint64_t cap, bool first_only, int ve } vec dummy; lbool ret = S.solveLimited(dummy); + if (conflicts_out) *conflicts_out = S.conflicts; /* GH-218 pilot */ + if (pilot_probe) { /* GH-218: a pilot probe only reports its conflicts */ + uint64_t opt = S.getLastOptimalCost(); + if (ret == l_True) return HALF_FOUND; + return (ret == l_False && opt == UINT64_MAX) ? HALF_NONE : HALF_UNKNOWN; + } if (g_frontier_stats || (h.frontier && g_frontier_check)) { /* stats also with -frontier=off (main's search) */ fprintf(stderr, "c FRONTIER %s cap %llu %s: conflicts %llu decisions %llu frontier_picks %llu fallbacks %llu " "no_eligible %llu mean_odd_rows %.2f check_fails %llu\n", h.tag, (unsigned long long)cap, @@ -1585,6 +1732,7 @@ static int min_distance_css_interleaved( if (Hx.cols != Hz.cols || Gx.cols != Hx.cols || Gz.cols != Hx.cols) die("matrix column mismatch"); const uint64_t n = (uint64_t)Hx.cols, INF = UINT64_MAX; CssHalf hs[2] = { {"X", &Hz, &Gx, Gx.rows > 0, 1, INF}, {"Z", &Hx, &Gz, Gz.rows > 0, 1, INF} }; + hs[0].ovl_dense_mode = hs[1].ovl_dense_mode = -1; /* GH-218: no pilot decision yet */ hs[0].own_lb = hs[1].own_lb = 1; for (int k = 0; k < 2; k++) { /* GH-130: per-half frontier mode (-frontier=auto decides from structure) */ hs[k].frontier = g_frontier_mode == 4 ? 0 : g_frontier_mode; @@ -1666,13 +1814,27 @@ static int min_distance_css_interleaved( for (int k = 0; g_stab_overlap && k < 2; k++) { if (!hs[k].exists) continue; OvlInfo oi; - hs[k].ovl = stab_overlap_rows(*hs[k].H, *hs[k].G, k == 0 ? Hx : Hz, oi); + hs[k].ovl = stab_overlap_rows(*hs[k].H, *hs[k].G, k == 0 ? Hx : Hz, oi, &hs[k].ovl_dense); + if (oi.c4_gated == 0) hs[k].ovl_dense.clear(); /* GH-218: no dense row, no pilot */ if (oi.rejected > 0) fprintf(stderr, "warning: stab-overlap: %s half: %d of %d stabilizer rows fail H g = 0 or G g = 0 (not used)\n", hs[k].tag, oi.rejected, oi.candidates); if (verb > 0) { - printf("c stab-overlap %s: %d of %d rows used (%d rejected: H g != 0 or G g != 0; %d duplicates); |g| -> rows:", - hs[k].tag, oi.kept, oi.candidates, oi.rejected, oi.duplicates); + printf("c stab-overlap %s: %d of %d rows used (%d rejected: H g != 0 or G g != 0; %d duplicates", hs[k].tag, oi.kept, + oi.candidates, oi.rejected, oi.duplicates); + if (g_stab_overlap_c4 >= 0) /* GH-218 */ + { + if (oi.c4_gated == 0) printf("; 0 dense (more than %d Tanner 4-cycles)", g_stab_overlap_c4); + else if (g_stab_overlap_pilot > 0) + printf("; %d dense (more than %d Tanner 4-cycles): pilot (%d seeds) at cap P' = max(%llu, lb, activation) before " + "the first probe with cap >= P' + %llu", oi.c4_gated, g_stab_overlap_c4, g_stab_overlap_pilot, + (unsigned long long)g_stab_overlap_pilot_cap, (unsigned long long)g_stab_overlap_pilot_margin); + else + printf("; %d dense (more than %d Tanner 4-cycles): dropped from the first probe with cap >= P' + %llu, " + "P' = max(%llu, lb, activation)", oi.c4_gated, g_stab_overlap_c4, (unsigned long long)g_stab_overlap_pilot_margin, + (unsigned long long)g_stab_overlap_pilot_cap); + } + printf("); |g| -> rows:"); for (std::map::const_iterator it = oi.weights.begin(); it != oi.weights.end(); ++it) printf(" %d:%d (<= %d)", it->first, it->second, ovl_limit(it->first)); if (g_stab_overlap_enc == 3) printf("; native propagator rows %d (no clauses)%s\n", oi.native_rows, g_stab_overlap_mutant ? " [TEST MUTANT]" : ""); @@ -2477,6 +2639,26 @@ int main(int argc, char** argv) { if (!cc_parse_seconds(argv[i] + 20, &v) || v < 0 || v > 1000) die("invalid -stab-overlap-ratio (0..1000)"); g_stab_overlap_ratio = v; stab_ratio_given = true; } + else if (!strncmp(argv[i], "-stab-overlap-c4=", 17)) { /* GH-218 */ + const char* v = argv[i] + 17; + char* end = NULL; + long k = strtol(v, &end, 10); + if (!strcmp(v, "off")) g_stab_overlap_c4 = -1; + else if (*v && end && !*end && k >= 0 && k <= 1000000) g_stab_overlap_c4 = (int)k; + else die("invalid -stab-overlap-c4 (N = 0..1000000 | off)"); + } + else if (!strncmp(argv[i], "-stab-overlap-pilot-cap=", 24)) { /* GH-218 */ + char* end = NULL; + long k = strtol(argv[i] + 24, &end, 10); + if (!argv[i][24] || !end || *end || k < 1 || k > 100000) die("invalid -stab-overlap-pilot-cap (P = 1..100000)"); + g_stab_overlap_pilot_cap = (uint64_t)k; + } + else if (!strncmp(argv[i], "-stab-overlap-pilot=", 20)) { /* GH-218 */ + char* end = NULL; + long k = strtol(argv[i] + 20, &end, 10); + if (!argv[i][20] || !end || *end || k < 0 || k > 15) die("invalid -stab-overlap-pilot (N = 0..15)"); + g_stab_overlap_pilot = (int)k; + } else if (!strcmp(argv[i], "-stab-overlap-enc=clauses")) g_stab_overlap_enc = 0; else if (!strcmp(argv[i], "-stab-overlap-enc=bin")) @@ -2755,6 +2937,11 @@ int main(int argc, char** argv) { printf(" probes of a half also require |x & g| <= floor(|g|/2) for same-type stabilizer rows g (verified\n"); printf(" H g = 0, G g = 0; a minimum-weight logical always satisfies it, else x + g is lighter); on: every\n"); printf(" row in every probe; auto: row g only in probes with cap >= 2 (floor(|g|/2) + 1) (-stab-overlap-ratio=X);\n"); + printf(" -stab-overlap-c4=N|off (GH-218, default 11): rows g on more than N Tanner 4-cycles of the stabilizer\n"); + printf(" matrix (sum over the other rows g' of C(|g & g'|, 2)) are dense; from a half's first probe with cap >= P' + 4,\n"); + printf(" P' = max(P, lb, row activation cap), they are dropped (default), or with -stab-overlap-pilot=N > 0 (opt-in)\n"); + printf(" a pilot runs \"weight <= P'?\" with and without them for N seeds and keeps them iff the median conflict\n"); + printf(" ratio is <= 1 (-stab-overlap-pilot-cap=P, default 12); off = every verified row in every probe (GH-148)\n"); printf(" -stab-overlap-enc=native|clauses|bin|seq (default native: a propagator inside MaxCDCL; clauses: binomial\n"); printf(" clauses up to |g| = 9, sequential counter above; bin / seq: one of them for every row)\n"); printf(" Output (default): live c trying d / c d_lb / c d_ub, then c d / o d\n"); diff --git a/src/solver/Solver.cc b/src/solver/Solver.cc index 54446a84..0cd25502 100644 --- a/src/solver/Solver.cc +++ b/src/solver/Solver.cc @@ -2067,7 +2067,7 @@ CRef Solver::propagate() NextClause:; } ws.shrink(i - j); - if (!ovRows.empty() && confl == CRef_Undef) { // GH-148 native overlap rows (inactive when empty) + if (!ovRows.empty() && confl == CRef_Undef && ovWatched(p)) { // GH-148 native overlap rows (inactive when empty) CRef oc = ovPropagate(p, false); if (oc != CRef_Undef) { confl = oc; qhead = trail.size(); } } @@ -4053,7 +4053,7 @@ CRef Solver::propagateForLK() { NextClause:; } ws.shrink(i - j); - if (!ovRows.empty() && confl == CRef_Undef && falseVar == var_Undef) { // GH-148 (inactive when empty) + if (!ovRows.empty() && confl == CRef_Undef && falseVar == var_Undef && ovWatched(p)) { // GH-148 (inactive when empty) CRef oc = ovPropagate(p, true); if (oc != CRef_Undef) { confl = oc; qhead = trail.size(); } else if (falseVar != var_Undef) qhead = trail.size(); @@ -7379,6 +7379,8 @@ void Solver::setOverlapRows(const std::vector >& rows, const st ovLim.push_back(lims[r] < 0 ? 0 : lims[r]); for (size_t t = 0; t < rows[r].size(); t++) ovColRows[(size_t)rows[r][t]].push_back(id); } + ovHas.assign((size_t)nQubits, 0); // GH-218: qubits on at least one row (call-site filter) + for (int q = 0; q < nQubits; q++) ovHas[(size_t)q] = !ovColRows[(size_t)q].empty(); ovCacheIdx.assign(1024, -1); } diff --git a/src/solver/Solver.h b/src/solver/Solver.h index d6a3e7e8..4a4308f3 100644 --- a/src/solver/Solver.h +++ b/src/solver/Solver.h @@ -603,6 +603,10 @@ class Solver { std::unordered_set ovCrefs; // the cached crefs: on-the-fly clause reduction skips them bool ovIsClause(CRef cr) const { return !ovRows.empty() && ovCrefs.count((uint32_t)cr) > 0; } void setOverlapRows(const std::vector >& rows, const std::vector& lims, int nQubits); + // DistQLDPC GH-218: ovPropagate acts only on a qubit var becoming true that lies on a row; the call sites test this + // first (same propagation, no call per literal). + std::vector ovHas; + bool ovWatched(Lit p) const { return !sign(p) && (size_t)var(p) < ovHas.size() && ovHas[(size_t)var(p)]; } CRef ovClause(int r, uint32_t mask, int impliedPos); CRef ovPropagate(Lit p, bool lk); // Former function-local statics, now per instance (identical for single-instance runs). diff --git a/tests/test_cc_engine.cc b/tests/test_cc_engine.cc index 09f0ff05..ced631b0 100644 --- a/tests/test_cc_engine.cc +++ b/tests/test_cc_engine.cc @@ -320,7 +320,9 @@ static RunOut run_driver(const Matrix& Hx, const Matrix& Hz, const Matrix& Gx, c // GH-133 Part D: the production MaxSAT split driver (fresh solver per probe, -no-card) with -oddcap-skip off/on struct PreCfg { const char* name; double pre; uint64_t iters; bool oddcap; uint64_t seed; int dualmode; bool symbreak; int card; int mutant; int ovl; int ovl_enc; int ovl_mutant; double ovl_ratio; /* GH-148 (0 = -stab-overlap off) */ - int isd = 0; int isd_p = 2; }; // GH-146: collision mode of the pre-pass finder + int isd = 0; int isd_p = 2; // GH-146: collision mode of the pre-pass finder + int ovl_c4 = -1; // GH-218: -stab-overlap-c4 (-1 = no classification, the GH-148 search) + int ovl_pilot = 3; int ovl_pilot_cap = 12; int ovl_margin = 4; }; // GH-218 pilot (seeds, cap, margin) static RunOut run_maxsat(const Matrix& Hx, const Matrix& Hz, const Matrix& Gx, const Matrix& Gz, bool oddcap, const PreCfg* pc = NULL) { RunOut r; r.ok = false; r.d = -2; int fd[2]; @@ -337,6 +339,9 @@ static RunOut run_maxsat(const Matrix& Hx, const Matrix& Hz, const Matrix& Gx, c g_ub_pre = pc->pre; g_ub_pre_max_iters = pc->iters; g_seed = pc->seed; g_ub_pre_mutant = pc->mutant; g_ub_isd.isd = pc->isd; g_ub_isd.isd_p = pc->isd_p; // GH-146 (child process only) g_stab_overlap = pc->ovl != 0; g_stab_overlap_enc = pc->ovl_enc; g_stab_overlap_mutant = pc->ovl_mutant; g_stab_overlap_ratio = pc->ovl_ratio; // GH-148 + g_stab_overlap_c4 = pc->ovl_c4; // GH-218 + g_stab_overlap_pilot = pc->ovl_pilot; g_stab_overlap_pilot_cap = (uint64_t)pc->ovl_pilot_cap; + g_stab_overlap_pilot_margin = (uint64_t)pc->ovl_margin; (void)min_distance_css_interleaved(Hx, Hz, Gx, Gz, 0, fd[1], pc->card, pc->symbreak, pc->dualmode, false); } else (void)min_distance_css_interleaved(Hx, Hz, Gx, Gz, 0, fd[1], 0, true, DUALMODE_SHARE, false); @@ -1014,6 +1019,13 @@ int main(int argc, char** argv) { {"ovl-ratio1-pre-iter1-mto", 1.0, 1, true, 1, DUALMODE_SHARE, true, 3, 0, 1, 0, 0, 1.0}, {"ovl-mutant1", -1.0, 0, true, 0, DUALMODE_SHARE, true, 0, 0, 1, 0, 1}, {"ovl-mutant2", -1.0, 0, true, 0, DUALMODE_SHARE, true, 0, 0, 1, 0, 2}, + // GH-218: dense rows (4-cycle classification) under the pilot; margin 1 / pilot cap 1 reach the pilot on + // these small codes (answers must not change: every row subset is sound) + {"ovl-native-auto-c4-11", -1.0, 0, true, 0, DUALMODE_SHARE, true, 0, 0, 1, 3, 0, 2.0, 0, 2, 11}, + {"ovl-native-c4-0-pilot-m1", -1.0, 0, true, 1, DUALMODE_SHARE, true, 3, 0, 1, 3, 0, 0.0, 0, 2, 0, 3, 1, 1}, + {"ovl-native-c4-0-pilot1-m1-pre", 1.0, 1, true, 2, DUALMODE_SKIP, true, 0, 0, 1, 3, 0, 0.0, 0, 2, 0, 1, 1, 1}, + {"ovl-native-c4-2-nopilot-m1", -1.0, 0, true, 0, DUALMODE_SHARE, true, 0, 0, 1, 3, 0, 0.0, 0, 2, 2, 0, 1, 1}, + {"ovl-seq-c4-0-pilot-m1-nosymbreak", -1.0, 0, false, 0, DUALMODE_OFF, false, 0, 0, 1, 2, 0, 0.0, 0, 2, 0, 2, 1, 1}, }; for (const PreCfg& c : gcfg) { RunOut r = run_maxsat(mHx, mHz, mGx, mGz, c.oddcap, &c); @@ -1175,6 +1187,130 @@ int main(int argc, char** argv) { g_m_failed[2], g_m_runs[2], g_m_wrong[2], g_surf_mwrong[2]); if (g_codes_removing == 0 || g_m_wrong[1] == 0 || g_m_wrong[2] == 0 || g_m_wrong_nat[1] == 0) { fprintf(stderr, "CC_FAIL GH-148 mutant/coverage expectations not met\n"); fails++; } } + { // GH-218 Part G (c): the 4-cycle row gate selects exactly the verified distinct rows with c4(g) <= K, where + // c4(g) = sum over the other distinct rows g' of the same-type stabilizer matrix of C(|g & g'|, 2), recomputed + // here by brute force over row pairs. Codes: every tier0 code (both halves) and the tier2 / tier4 TN codes + // (weight-6..12 rows with 7..33 4-cycles); K = -1 (no gate), 0, 2, 7, 11, 12, 1000. Mutant 3 (test only) + // counts overlaps instead of qubit pairs and must change some selection. + static const char* stems[] = {"tier0/BB_72_12_6", "tier0/BB_90_8_10", "tier0/BB_108_8_10", "tier0/BB_144_12_12", + "tier0/GB_144_12_8", "tier0/LP_34_20_2", "tier0/LP_136_32_4", "tier0/LP_238_44_6", "tier0/TN_36_8_3", + "tier0/TN_36_8_4", "tier0/TN_54_11_4", "tier0/TN_72_14_4", "tier0/TN_72_8_8", "tier2/TN_108_2_12", + "tier2/TN_200_10_10", "tier4/TN_250_10_15"}; + static const int Ks[] = {-1, 0, 2, 7, 11, 12, 1000}; + long c_checks = 0, c_bad = 0, c_gated = 0, c_kept = 0, c_m3_diff = 0; + const int saved_c4 = g_stab_overlap_c4, saved_mut = g_stab_overlap_mutant; + for (const char* st : stems) { + const std::string base = std::string("data/matrices/") + st; + FILE* probe = fopen((base + "_Hx.txt").c_str(), "r"); + if (!probe) { fprintf(stderr, "CC_FAIL GH-218 partG (c): missing %s_Hx.txt (run from the repository root)\n", base.c_str()); fails++; continue; } + fclose(probe); + const Matrix Hx = load_matrix((base + "_Hx.txt").c_str()), Hz = load_matrix((base + "_Hz.txt").c_str()); + const Matrix Gx = load_matrix((base + "_Gx.txt").c_str()), Gz = load_matrix((base + "_Gz.txt").c_str()); + for (int half = 0; half < 2; half++) { + const Matrix& Hp = half == 0 ? Hz : Hx; const Matrix& Gl = half == 0 ? Gx : Gz; const Matrix& Sm = half == 0 ? Hx : Hz; + g_stab_overlap_mutant = 0; g_stab_overlap_c4 = -1; + OvlInfo all_info; + const OvlRows all = stab_overlap_rows(Hp, Gl, Sm, all_info); // verified distinct rows, no gate + std::vector > dist; // distinct nonzero rows of the stabilizer matrix + { + std::set > seen; + for (int r = 0; r < Sm.rows; r++) { + std::vector g; + for (int c = 0; c < Sm.cols; c++) if (getm(Sm, r, c)) g.push_back(c); + if (!g.empty() && seen.insert(g).second) dist.push_back(std::set(g.begin(), g.end())); + } + } + std::vector c4(all.size(), 0); + for (size_t i = 0; i < all.size(); i++) { + const std::set gi(all[i].begin(), all[i].end()); + for (size_t j = 0; j < dist.size(); j++) { + if (dist[j] == gi) continue; + long long o = 0; + for (int q : dist[j]) o += gi.count(q); + c4[i] += o * (o - 1) / 2; + } + } + for (int K : Ks) { + std::set > want; + for (size_t i = 0; i < all.size(); i++) if (K < 0 || c4[i] <= K) want.insert(all[i]); + g_stab_overlap_c4 = K; g_stab_overlap_mutant = 0; + OvlInfo info; + const OvlRows got = stab_overlap_rows(Hp, Gl, Sm, info); + const std::set > gotset(got.begin(), got.end()); + c_checks++; + if (gotset != want || (int)got.size() + info.c4_gated != (int)all.size()) { + c_bad++; fails++; + fprintf(stderr, "CC_FAIL GH-218 partG (c) %s half %d K=%d: %zu rows selected, want %zu (gated %d of %zu)\n", + st, half, K, got.size(), want.size(), info.c4_gated, all.size()); + } + if (K >= 0) { c_gated += info.c4_gated; c_kept += (long)got.size(); } + if (K >= 0) { // mutant 3 must select differently on some (code, half, K) + g_stab_overlap_mutant = 3; + OvlInfo mi; + const OvlRows m3 = stab_overlap_rows(Hp, Gl, Sm, mi); + if (std::set >(m3.begin(), m3.end()) != want) c_m3_diff++; + } + } + } + } + // dense flags: with the output vector every verified row is returned, flagged iff c4 > K + long dense_checks = 0, dense_bad = 0, pilot_runs = 0, pilot_bad = 0, pilot_kept = 0, force_checks = 0, force_bad = 0; + for (const char* st : stems) { + const std::string base = std::string("data/matrices/") + st; + FILE* probe = fopen((base + "_Hx.txt").c_str(), "r"); + if (!probe) continue; + fclose(probe); + const Matrix Hx = load_matrix((base + "_Hx.txt").c_str()), Hz = load_matrix((base + "_Hz.txt").c_str()); + const Matrix Gx = load_matrix((base + "_Gx.txt").c_str()), Gz = load_matrix((base + "_Gz.txt").c_str()); + for (int half = 0; half < 2; half++) { + const Matrix& Hp = half == 0 ? Hz : Hx; const Matrix& Gl = half == 0 ? Gx : Gz; const Matrix& Sm = half == 0 ? Hx : Hz; + g_stab_overlap_mutant = 0; g_stab_overlap_c4 = -1; + OvlInfo ai; const OvlRows all = stab_overlap_rows(Hp, Gl, Sm, ai); + g_stab_overlap_c4 = 11; + OvlInfo si; const OvlRows sparse = stab_overlap_rows(Hp, Gl, Sm, si); + OvlInfo di; std::vector dense; const OvlRows withd = stab_overlap_rows(Hp, Gl, Sm, di, &dense); + dense_checks++; + OvlRows sp2; + for (size_t i = 0; i < withd.size() && i < dense.size(); i++) if (!dense[i]) sp2.push_back(withd[i]); + long nd = 0; for (char c : dense) nd += c; + if (withd != all || dense.size() != withd.size() || sp2 != sparse || nd != di.c4_gated) { + dense_bad++; fails++; + fprintf(stderr, "CC_FAIL GH-218 partG (c) dense flags %s half %d\n", st, half); + } + // pilot unit check on the TN codes of tier0 (small d): forced with/without dense rows the probe answers + // agree at caps d - 1 and d (NONE / FOUND), and the pilot decision is reproducible + if (strncmp(st, "tier0/TN_", 9) || nd == 0) continue; + CssHalf h = { half == 0 ? "X" : "Z", &Hp, &Gl, Gl.rows > 0, 1, UINT64_MAX }; + h.ovl_dense_mode = -1; h.ovl = withd; h.ovl_dense = dense; h.frontier = 0; h.par = false; h.pre = false; + const int d = atoi(strrchr(st, '_') + 1); + for (int cap = d - 1; cap <= d; cap++) { + uint64_t v = 0, c1 = 0, c0 = 0; + const HalfStatus s1 = run_css_half(h, (uint64_t)cap, true, 0, 0, -1, UINT64_MAX, UINT64_MAX, true, v, 1, &c1); + const HalfStatus s0 = run_css_half(h, (uint64_t)cap, true, 0, 0, -1, UINT64_MAX, UINT64_MAX, true, v, 0, &c0); + force_checks++; + // the half's own minimum may exceed d (d = min over both halves): only agreement is required + if (s1 != s0 || (s1 != HALF_FOUND && s1 != HALF_NONE)) { + force_bad++; fails++; + fprintf(stderr, "CC_FAIL GH-218 partG (c) forced dense %s half %d cap %d: %d vs %d\n", st, half, cap, (int)s1, (int)s0); + } + } + g_stab_overlap_pilot_cap = 1; g_stab_overlap_pilot = 3; + int dec[2]; + for (int rep2 = 0; rep2 < 2; rep2++) { h.ovl_dense_mode = -1; ovl_pilot(h, 0, 0); dec[rep2] = h.ovl_dense_mode; pilot_runs++; } + if (dec[0] != dec[1] || dec[0] < 0) { pilot_bad++; fails++; fprintf(stderr, "CC_FAIL GH-218 partG (c) pilot %s half %d: %d / %d\n", st, half, dec[0], dec[1]); } + pilot_kept += dec[0] == 1; + g_stab_overlap_pilot_cap = 12; g_stab_overlap_pilot = 0; + } + } + g_stab_overlap_c4 = saved_c4; g_stab_overlap_mutant = saved_mut; + printf("partG (c) GH-218 dense flags: %ld checks, %ld bad; forced dense on/off probe answers on tier0 TN halves: %ld checks, %ld bad; " + "pilot decisions: %ld runs, %ld not reproducible (kept on %ld)\n", dense_checks, dense_bad, force_checks, force_bad, pilot_runs, pilot_bad, pilot_kept); + if (force_checks == 0 || pilot_runs == 0) { fprintf(stderr, "CC_FAIL GH-218 partG (c) pilot coverage\n"); fails++; } + printf("partG (c) GH-218 4-cycle row gate: %ld selections on %zu codes x 2 halves, %ld bad (gated %ld, kept %ld rows over K >= 0); " + "mutant 3 (overlaps counted instead of pairs) changes %ld selections\n", + c_checks, sizeof(stems) / sizeof(stems[0]), c_bad, c_gated, c_kept, c_m3_diff); + if (c_gated == 0 || c_kept == 0 || c_m3_diff == 0) { fprintf(stderr, "CC_FAIL GH-218 partG (c) coverage/mutant expectations not met\n"); fails++; } + } printf("partB: %ld CSS codes (%ld with a verified dual map, %ld with X-half orbits, %ld with dX != dZ, %ld with all-odd Hz), %ld driver runs, %ld bad, %ld RESULT -1\n", b_inst, b_dual, b_xorb, b_dxdz, b_odd, b_runs, b_bad, b_traps); printf("partD (MaxSAT split, -oddcap-skip off/on): %ld runs on %ld codes (%ld with an all-odd half), %ld bad\n", d_runs, b_inst, d_odd, d_bad); diff --git a/tests/test_cc_flags.sh b/tests/test_cc_flags.sh index aa40f0e7..8ed3de70 100755 --- a/tests/test_cc_flags.sh +++ b/tests/test_cc_flags.sh @@ -405,8 +405,8 @@ runs=$((runs + 1)); run -frontier-stats -stab-overlap=on -stab-overlap-enc=bin $ if grep -q "^c OVERLAP" <<<"$err"; then echo "FAIL (no c OVERLAP line with clause encodings)" >&2; fails=$((fails + 1)); fi accept 2 "" -engine=auto -stab-overlap=on $L $D1 # auto -> maxsat: applies accept 2 "selected cc .*ignoring -stab-overlap=on" -engine=auto -stab-overlap=on $L $C -vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates); |g| -> rows: 6:45 (<= 3); binomial rows 45, counter rows 0; per probe 675 clauses, 0 aux vars$" -v -stab-overlap=on -stab-overlap-enc=clauses $L BB_90_8_10 -vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates); |g| -> rows: 6:45 (<= 3); native propagator rows 45 (no clauses)$" -v -stab-overlap=on $L BB_90_8_10 +vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates; 0 dense (more than 11 Tanner 4-cycles)); |g| -> rows: 6:45 (<= 3); binomial rows 45, counter rows 0; per probe 675 clauses, 0 aux vars$" -v -stab-overlap=on -stab-overlap-enc=clauses $L BB_90_8_10 +vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates; 0 dense (more than 11 Tanner 4-cycles)); |g| -> rows: 6:45 (<= 3); native propagator rows 45 (no clauses)$" -v -stab-overlap=on $L BB_90_8_10 vgrep 10 "^c stab-overlap X: 45 of 45 rows used .* binomial rows 45, counter rows 0" -v -stab-overlap=auto -stab-overlap-enc=bin $L BB_90_8_10 vgrep 10 "^c stab-overlap Z: 45 of 45 rows used .* binomial rows 0, counter rows 45; per probe 1440 clauses, 675 aux vars$" -v -stab-overlap=on -stab-overlap-enc=seq $L BB_90_8_10 vgrep 10 "^c stab-overlap X cap 8: 45 of 45 rows active (ratio 2.00)$" -v -stab-overlap=auto $L BB_90_8_10 @@ -415,7 +415,7 @@ vgrep 10 "^c stab-overlap X cap 4: 45 of 45 rows active (ratio 0.00)$" -v -stab- runs=$((runs + 1)); run -v -stab-overlap=off $L BB_90_8_10 if grep -q "stab-overlap" <<<"$out$err"; then echo "FAIL (-stab-overlap=off must not print stab-overlap lines)" >&2; fails=$((fails + 1)); fi # default (auto since the PI's adoption decision): the same lines as -stab-overlap=auto -vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates); |g| -> rows: 6:45 (<= 3); native propagator rows 45 (no clauses)$" -v $L BB_90_8_10 +vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates; 0 dense (more than 11 Tanner 4-cycles)); |g| -> rows: 6:45 (<= 3); native propagator rows 45 (no clauses)$" -v $L BB_90_8_10 vgrep 10 "^c stab-overlap X cap 8: 45 of 45 rows active (ratio 2.00)$" -v $L BB_90_8_10 vgrep 10 "^c stab-overlap X cap 4: 0 of 45 rows active (ratio 2.00)$" -v $L BB_90_8_10 runs=$((runs + 1)); run -frontier-stats $L BB_90_8_10 @@ -423,6 +423,42 @@ if [[ $rc -ne 0 ]] || ! grep -q "^c OVERLAP X cap 8: rows 45 props [0-9]* confli runs=$((runs + 1)); run -v -joint $L $M if grep -q "stab-overlap" <<<"$out$err"; then echo "FAIL (default auto is silently off with -joint: no stab-overlap lines expected)" >&2; fails=$((fails + 1)); fi +# 7g. GH-218 dense rows and the per-half pilot: -stab-overlap-c4=N|off (default 11), -stab-overlap-pilot=N (default 0 = +# drop the dense rows at the first probe with cap >= P' + 4), -stab-overlap-pilot-cap=P (default 12); -stab-overlap-c4=off = GH-148's search +for f in -stab-overlap-c4= -stab-overlap-c4=x -stab-overlap-c4=-1 -stab-overlap-c4=1.5 -stab-overlap-c4=OFF -stab-overlap-c4=2000000; do + reject "invalid -stab-overlap-c4" $f $L $M +done +for f in -stab-overlap-pilot= -stab-overlap-pilot=x -stab-overlap-pilot=-1 -stab-overlap-pilot=16; do reject "invalid -stab-overlap-pilot " $f $L $M; done +for f in -stab-overlap-pilot-cap= -stab-overlap-pilot-cap=0 -stab-overlap-pilot-cap=y -stab-overlap-pilot-cap=100001; do reject "invalid -stab-overlap-pilot-cap" $f $L $M; done +reject "needs -stab-overlap=on or -stab-overlap=auto" -stab-overlap=off -stab-overlap-c4=3 $L $M +reject "needs -stab-overlap=on or -stab-overlap=auto" -stab-overlap=off -stab-overlap-pilot=1 $L $M +reject "no effect with -engine=cc" -engine=cc -stab-overlap-c4=3 $L $C +reject "no effect with -engine=cc" -engine=cc -stab-overlap-pilot-cap=5 $L $C +accept 3 "" -stab-overlap-c4=0 $L $M +accept 3 "" -stab-overlap-c4=off -card-mto $L $M +accept 3 "" -stab-overlap-pilot=0 -stab-overlap-pilot-cap=1 $L $M +accept 8 "" -stab-overlap-c4=0 $L TN_72_8_8 +accept 8 "" -stab-overlap=on -stab-overlap-c4=1000 -card-mto $L TN_72_8_8 +accept 8 "" -stab-overlap=on -stab-overlap-pilot=1 -stab-overlap-pilot-cap=1 $L TN_72_8_8 +accept 10 "" -stab-overlap=on -stab-overlap-c4=off -stab-overlap-enc=seq $L BB_90_8_10 +vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates); |g| -> rows: 6:45 (<= 3); native propagator rows 45 (no clauses)$" -v -stab-overlap-c4=off $L BB_90_8_10 +vgrep 10 "^c stab-overlap X: 45 of 45 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates; 0 dense (more than 0 Tanner 4-cycles)); |g|" -v -stab-overlap-c4=0 $L BB_90_8_10 +vgrep 8 "^c stab-overlap X: 36 of 36 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates; 36 dense (more than 11 Tanner 4-cycles): dropped from the first probe with cap >= P' + 4, P' = max(12, lb, activation)); |g| -> rows: 9:36 (<= 4)" -v $L TN_72_8_8 +vgrep 8 "^c stab-overlap X: 36 of 36 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates; 36 dense (more than 11 Tanner 4-cycles): pilot (3 seeds) at cap P' = max(12, lb, activation) before the first probe with cap >= P' + 4); |g|" -v -stab-overlap-pilot=3 $L TN_72_8_8 +vgrep 8 "^c stab-overlap X: 36 of 36 rows used (0 rejected: H g != 0 or G g != 0; 0 duplicates); |g| -> rows: 9:36 (<= 4)" -v -stab-overlap-c4=off $L TN_72_8_8 +# TN_72_8_8 (d = 8, ub-pre off: caps 1, 2, 4, 8): P >= 10 (weight-9 rows active from cap 10): no pilot, dense rows used +runs=$((runs + 1)); run -frontier-stats -stab-overlap=on -ub-pre=off $L TN_72_8_8 +if [[ $rc -ne 0 ]] || ! grep -q "^c OVERLAP" <<<"$err" || grep -q "OVERLAP-PILOT" <<<"$err"; then echo "FAIL (TN_72_8_8 -stab-overlap=on: dense rows used, no pilot expected)" >&2; fails=$((fails + 1)); fi +# TN_108_2_12 with -ub-pre=off: caps 1, 2, 4, 8, 16; at cap 16 lb = 9, pilot cap 1 -> P = max(1, 9, 10) = 10, 16 >= 14: +# one pilot per half (3 seeds) +runs=$((runs + 1)); run -frontier-stats -ub-pre=off -stab-overlap-pilot=3 -stab-overlap-pilot-cap=1 -cpu-lim=60 TN_108_2_12 +if ! grep -Eq "^c OVERLAP-PILOT X cap 10: dense_rows 54 seed 0 [0-9]+/[0-9]+, seed 1 [0-9]+/[0-9]+, seed 2 [0-9]+/[0-9]+ median [0-9.]+ -> (kept|dropped)$" <<<"$err"; then + echo "FAIL (TN_108_2_12 -ub-pre=off: c OVERLAP-PILOT X line expected): $(grep PILOT <<<"$err")" >&2; fails=$((fails + 1)); fi +runs=$((runs + 1)); run -frontier-stats -ub-pre=off -cpu-lim=20 TN_108_2_12 # default: no pilot, dense rows dropped at cap 16 +if grep -q "OVERLAP-PILOT" <<<"$err" || ! grep -q "^c OVERLAP-DROP X cap 16: dense_rows 54$" <<<"$err"; then echo "FAIL (default -stab-overlap-pilot=0: c OVERLAP-DROP X cap 16 expected, no pilot)" >&2; fails=$((fails + 1)); fi +runs=$((runs + 1)); run -frontier-stats -cpu-lim=20 TN_108_2_12 # with -ub-pre (U0 = 12): caps <= 11, dense rows never dropped +if grep -q "OVERLAP-DROP\|OVERLAP-PILOT" <<<"$err"; then echo "FAIL (TN_108_2_12 default: caps stay below 16, no drop/pilot line expected)" >&2; fails=$((fails + 1)); fi + # 8. a CC trap withdraws the bounds already sent (test mutant 2 with the GH-124 rule set traps on LP_136_32_4 after # emitting d_lb lines; with the GH-133 rules the same mutant answers wrongly instead, which this check does not need) runs=$((runs + 1))