diff --git a/MODIFICATIONS.md b/MODIFICATIONS.md index 92cff272..574f4ea8 100644 --- a/MODIFICATIONS.md +++ b/MODIFICATIONS.md @@ -18,7 +18,7 @@ New code, not derived from MaxCDCL. | Area | Description | |------|-------------| | QLDPC encoding | MaxSAT formulation for stabilizer distance (Hx/Hz/Gx/Gz matrices) | -| Fork + pipe | Child runs solver; parent enforces wall-clock timeout (`-cpu-lim`) via `SIGKILL` | +| Fork + pipe | Child runs solver; parent enforces wall-clock timeout (`-cpu-lim`) via `SIGKILL`; the parent waits in `poll()` on the pipe and a SIGCHLD self-pipe, so it sees the child's exit at once (GH-224; was 10 ms `usleep` polling) | | Bounds sync | Parent reads `TRY` / `LB` / `UB` / `RESULT` lines from pipe | | Progress output | Default mode prints `c trying d:`, `c d_lb:`, `c d_ub:`, `c d:`, `o` | | Quiet / debug | Default `verb=0`; child stdout to `/dev/null`; `-v` / `-debug` for solver log | diff --git a/optimization/experiments/GH-224/analysis.md b/optimization/experiments/GH-224/analysis.md new file mode 100644 index 00000000..0b2d665d --- /dev/null +++ b/optimization/experiments/GH-224/analysis.md @@ -0,0 +1,66 @@ +# GH-224: parent wait loop without the 10 ms polling floor + +Change: `solve_in_child_fork` (`src/core/distqldpc.cc`) used to wait for the solver child with `usleep(10000)` between checks. It now waits in `poll()` on the bounds pipe and on a SIGCHLD self-pipe. The timeout is the remaining `-cpu-lim` time, capped at 100 ms. The solver child is unchanged. + +Binaries (yfclab2, frozen): old = main fecee8c9 (`frozen/server-gh224-main-fecee8c`), new = 2587b9de (`frozen/server-gh224-2587b9d`). + +## Tier 0 +- `make test-cc`: PASS on yfclab2 (`raw/t0tests/test_cc_new.txt`) and on the Mac (`raw/t0tests/mac_test_cc.txt`). The output equals main's except one timing-dependent counter: partE "levels abandoned" is 37 on main and 38 on new. This test never calls the changed function. +- `make test-cc-flags`: 566 checks, 0 failed (server and Mac). +- `scripts/smoke_test.sh` and `scripts/test_partition_soft_literals.py`: pass. +- Behaviour (`raw/behaviour/behaviour.txt`), old vs new, with identical output lines: + - `-cpu-lim=3` timeout, MaxSAT and CC: TIMEOUT at 3.03 s with the same bounds. + - Tighter `prlimit --as` (200 MB MaxSAT, 60 MB CC): the same UNKNOWN. + - Child killed from outside with SIGKILL: UNKNOWN within 6-8 ms. + - Child SIGSTOP/SIGCONT: finishes normally. +- Answers: 9450 + 216 panel runs, all rc 0 and all equal to the stem distance. + +## Tier 0 + Tier 1 panel (`raw/t01/`) +Setup: +- Layout of main fecee8c9: 26 tier0 and 9 tier1 codes. +- Modes: MaxSAT default (mto), MaxSAT `-no-card`, CC default. +- Seeds 0-4, 9 repetitions. +- old and new run interleaved on one pinned core per (code, mode, seed), with rotating order; cores 72-101 only, each with an idle SMT sibling. +- Cell = median over repetitions, then median over seeds. Ratio = new / old. + +| Tier | Mode | cells | geomean | worst cell | cells > 1.25 | +|---|---|---:|---:|---|---:| +| 0 | cc | 26 | 0.666 | 0.964 | 0 | +| 0 | mto | 26 | 0.849 | 1.032 | 0 | +| 0 | nocard | 26 | 0.853 | 1.086 | 0 | +| 1 | cc | 9 | 0.879 | 0.995 | 0 | +| 1 | mto | 9 | 0.978 | 0.987 | 0 | +| 1 | nocard | 9 | 0.981 | 0.993 | 0 | + +**Logs.** stdout is byte-identical in every run of both arms for 522 of 525 units. The other 3 (all GB_144_12_12 CC) differ only in the order of a `c d_ub` line relative to the level lines. That order is timing-dependent: main's own runs vary the same way. + +**Floor.** Wait slack = wall - user - sys, over runs shorter than 0.2 s (about 3300 per arm): + +| Arm | median | p90 | +|---|---:|---:| +| old | 11.9 ms | 16.2 ms | +| new | 4.8 ms | 7.8 ms | + +Wall times of the CC cells, in 1 ms bins: +- old LP_442 splits into two groups, 27-31 ms and 34-44 ms; +- new LP_442 is one contiguous group, 25-33 ms; +- old BB_186 is spread over 28-60 ms; +- new BB_186 is 21-30 ms. + +The MaxSAT cells of 1-10 s also run about 2 % faster in CPU time: the parent no longer wakes up 100 times a second on the solver's core. + +## Tier 2/3 spot check (`raw/spot_analysis.md`) +Tiers 2-5 are unaffected by construction: the solver child and the deadline path are unchanged, and the parent wakes up less often. This was spot-checked, not run in full; there was no Tier 5 run. + +Setup: 3 seeds x 3 repetitions, interleaved. +- Tier 2: LP_544, TN_108 and BB_144_14_14, in all three modes. +- Tier 3: TN_250, LP_1020 and HGP_481, CC only. + +| Tier | geomean | worst cell | +|---|---:|---| +| 2 | 0.952 | 1.001 (TN_108 CC) | +| 3 | 0.959 | 1.002 (TN_250 CC, 50.6 s) | + +Every answer is correct. The log differences are the same timing-dependent line-order cases. + +Runners: `runner/interleave.py`, `runner/analyze.py` and `runner/behaviour.sh`. diff --git a/optimization/experiments/GH-224/raw/behaviour/behaviour.txt b/optimization/experiments/GH-224/raw/behaviour/behaviour.txt new file mode 100644 index 00000000..6780e575 --- /dev/null +++ b/optimization/experiments/GH-224/raw/behaviour/behaviour.txt @@ -0,0 +1,12 @@ +timeout-maxsat old rc=1 wall=3.031 c d_ub: 15|c d_lb: 2|c d_lb: 3|c d_lb: 5|c d_lb: 5|c d_ub: 15|c status: TIMEOUT (child killed after -cpu-lim)|c d : UNKNOWN|s UNKNOWN| +timeout-maxsat new rc=1 wall=3.025 c d_ub: 15|c d_lb: 2|c d_lb: 3|c d_lb: 5|c d_lb: 5|c d_ub: 15|c status: TIMEOUT (child killed after -cpu-lim)|c d : UNKNOWN|s UNKNOWN| +timeout-cc old rc=1 wall=3.031 c d_ub: 52|c d_lb: 2|c d_ub: 40|c d_lb: 4|c d_lb: 6|c d_lb: 8|c d_lb: 10|c d_lb: 12|c d_lb: 14|c d_lb: 16|c d_lb: 18|c d_lb: 20|c d_lb: 20|c d_ub: 40|c status: TIMEOUT (child killed after -cpu-lim)|c d : UNKNOWN|s UNKNOWN| +timeout-cc new rc=1 wall=3.031 c d_ub: 52|c d_lb: 2|c d_ub: 40|c d_lb: 4|c d_lb: 6|c d_lb: 8|c d_lb: 10|c d_lb: 12|c d_lb: 14|c d_lb: 16|c d_lb: 18|c d_lb: 20|c d_lb: 20|c d_ub: 40|c status: TIMEOUT (child killed after -cpu-lim)|c d : UNKNOWN|s UNKNOWN| +memcap-200M old rc=1 wall=2.913 c d_lb: -|c d_ub: -|c status: UNKNOWN|c d : UNKNOWN|s UNKNOWN| +memcap-200M new rc=1 wall=3.060 c d_lb: -|c d_ub: -|c status: UNKNOWN|c d : UNKNOWN|s UNKNOWN| +memcap-60M-cc old rc=1 wall=1.383 c d_ub: 50|c d_lb: 2|c d_lb: 2|c d_ub: 50|c status: UNKNOWN|c d : UNKNOWN|s UNKNOWN| +memcap-60M-cc new rc=1 wall=1.281 c d_ub: 50|c d_lb: 2|c d_lb: 2|c d_ub: 50|c status: UNKNOWN|c d : UNKNOWN|s UNKNOWN| +child-sigkill old rc=1 after-kill=0.008 c status: UNKNOWN|s UNKNOWN| +child-sigkill new rc=1 after-kill=0.006 c status: UNKNOWN|s UNKNOWN| +child-stop-cont old rc=0 wall=7.373 o 10| +child-stop-cont new rc=0 wall=7.220 o 10| diff --git a/optimization/experiments/GH-224/raw/spot_analysis.md b/optimization/experiments/GH-224/raw/spot_analysis.md new file mode 100644 index 00000000..7437c112 --- /dev/null +++ b/optimization/experiments/GH-224/raw/spot_analysis.md @@ -0,0 +1,44 @@ +## Cells (new vs old; median over reps, then over seeds; wall in s) + +| Tier | Mode | Code | seeds | old wall | new wall | wall ratio | cpu ratio | +|---|---|---|---:|---:|---:|---:|---:| +| tier2 | cc | BB_144_14_14 | 3 | 0.6231 | 0.6204 | 0.996 | 1.006 | +| tier2 | cc | LP_544_80_12 | 3 | 0.0438 | 0.0333 | 0.759 | 0.934 | +| tier2 | cc | TN_108_2_12 | 3 | 1.8107 | 1.8118 | 1.001 | 1.001 | +| tier2 | mto | BB_144_14_14 | 3 | 13.3797 | 13.1300 | 0.981 | 0.977 | +| tier2 | mto | LP_544_80_12 | 3 | 14.5664 | 14.1177 | 0.969 | 0.968 | +| tier2 | mto | TN_108_2_12 | 3 | 19.8998 | 19.4537 | 0.978 | 0.979 | +| tier2 | nocard | BB_144_14_14 | 3 | 13.1625 | 12.6378 | 0.960 | 0.961 | +| tier2 | nocard | LP_544_80_12 | 3 | 13.9501 | 13.4979 | 0.968 | 0.968 | +| tier2 | nocard | TN_108_2_12 | 3 | 19.9104 | 19.4988 | 0.979 | 0.979 | +| tier3 | cc | HGP_481_1_16 | 3 | 0.1725 | 0.1561 | 0.905 | 0.946 | +| tier3 | cc | LP_1020_136_16 | 3 | 0.2804 | 0.2725 | 0.972 | 0.975 | +| tier3 | cc | TN_250_10_15 | 3 | 50.5596 | 50.6515 | 1.002 | 1.002 | + +## Verdict per tier and mode + +| Tier | Mode | cells | geomean | worst cell | cells > 1.25 | verdict | +|---|---|---:|---:|---|---:|---| +| tier2 | cc | 3 | 0.911 | 1.001 (TN_108_2_12) | 0 | PASS | +| tier2 | mto | 3 | 0.976 | 0.981 (BB_144_14_14) | 0 | PASS | +| tier2 | nocard | 3 | 0.969 | 0.979 (TN_108_2_12) | 0 | PASS | +| tier3 | cc | 3 | 0.959 | 1.002 (TN_250_10_15) | 0 | PASS | +| tier2 | all | 9 | 0.952 | 1.001 | 0 | PASS | +| tier3 | all | 3 | 0.959 | 1.002 | 0 | PASS | + +## Logs + +units with byte-identical stdout in every run of both arms: 34; other units: 2 (of which old itself varies across reps: 1; identical up to line order in every run: 1) +- ('tier3', 'cc', 'LP_1020_136_16', 2): distinct stdouts old 2, new 2, same set: False +- ('tier3', 'cc', 'TN_250_10_15', 0): distinct stdouts old 1, new 2, same set: False + +## Answers + +runs: 216; rc != 0 or answer != stem: 0 [] + +## Wait slack (wall - user - sys) of runs with wall < 0.2 s, in ms + +| Arm | runs | median | p90 | max | +|---|---:|---:|---:|---:| +| old | 20 | 12.27 | 14.79 | 15.59 | +| new | 21 | 3.37 | 4.25 | 4.99 | diff --git a/optimization/experiments/GH-224/raw/t01/analysis.md b/optimization/experiments/GH-224/raw/t01/analysis.md new file mode 100644 index 00000000..8c7a4a0b --- /dev/null +++ b/optimization/experiments/GH-224/raw/t01/analysis.md @@ -0,0 +1,140 @@ +## Cells (new vs old; median over reps, then over seeds; wall in s) + +| Tier | Mode | Code | seeds | old wall | new wall | wall ratio | cpu ratio | +|---|---|---|---:|---:|---:|---:|---:| +| tier0 | cc | AMC_108_6_9 | 5 | 0.0253 | 0.0209 | 0.825 | 1.174 | +| tier0 | cc | AMC_216_6_12 | 5 | 0.0293 | 0.0242 | 0.827 | 0.905 | +| tier0 | cc | AMC_330_6_14 | 5 | 0.0333 | 0.0321 | 0.964 | 0.993 | +| tier0 | cc | BB_108_8_10 | 5 | 0.0274 | 0.0167 | 0.611 | 0.840 | +| tier0 | cc | BB_120_8_12 | 5 | 0.0253 | 0.0205 | 0.809 | 1.076 | +| tier0 | cc | BB_144_12_12 | 5 | 0.0248 | 0.0210 | 0.848 | 1.141 | +| tier0 | cc | BB_30_4_6 | 5 | 0.0223 | 0.0157 | 0.706 | 1.196 | +| tier0 | cc | BB_72_12_6 | 5 | 0.0231 | 0.0155 | 0.674 | 1.091 | +| tier0 | cc | BB_90_8_10 | 5 | 0.0250 | 0.0163 | 0.651 | 0.992 | +| tier0 | cc | COLOR_19_1_5 | 5 | 0.0230 | 0.0133 | 0.578 | 0.929 | +| tier0 | cc | COLOR_7_1_3 | 5 | 0.0231 | 0.0129 | 0.561 | 0.939 | +| tier0 | cc | GB_144_12_8 | 5 | 0.0267 | 0.0182 | 0.682 | 0.957 | +| tier0 | cc | HGP_106_16_4 | 5 | 0.0268 | 0.0156 | 0.582 | 0.906 | +| tier0 | cc | HGP_113_1_8 | 5 | 0.0279 | 0.0161 | 0.577 | 0.846 | +| tier0 | cc | HGP_13_1_3 | 5 | 0.0231 | 0.0121 | 0.525 | 0.900 | +| tier0 | cc | HGP_306_36_5 | 5 | 0.0352 | 0.0299 | 0.848 | 1.128 | +| tier0 | cc | HGP_41_1_5 | 5 | 0.0256 | 0.0160 | 0.625 | 0.939 | +| tier0 | cc | HGP_45_9_3 | 5 | 0.0222 | 0.0152 | 0.682 | 1.160 | +| tier0 | cc | LP_136_32_4 | 5 | 0.0260 | 0.0181 | 0.697 | 1.039 | +| tier0 | cc | LP_238_44_6 | 5 | 0.0250 | 0.0229 | 0.915 | 1.095 | +| tier0 | cc | LP_34_20_2 | 5 | 0.0242 | 0.0137 | 0.567 | 0.880 | +| tier0 | cc | TN_36_8_3 | 5 | 0.0268 | 0.0136 | 0.507 | 0.840 | +| tier0 | cc | TN_36_8_4 | 5 | 0.0239 | 0.0123 | 0.512 | 0.836 | +| tier0 | cc | TN_54_11_4 | 5 | 0.0288 | 0.0143 | 0.495 | 0.860 | +| tier0 | cc | TN_72_14_4 | 5 | 0.0284 | 0.0144 | 0.508 | 0.814 | +| tier0 | cc | TN_72_8_8 | 5 | 0.0236 | 0.0211 | 0.894 | 0.977 | +| tier0 | mto | AMC_108_6_9 | 5 | 0.1000 | 0.0968 | 0.968 | 1.011 | +| tier0 | mto | AMC_216_6_12 | 5 | 0.2981 | 0.2937 | 0.985 | 0.999 | +| tier0 | mto | AMC_330_6_14 | 5 | 0.6915 | 0.6771 | 0.979 | 0.987 | +| tier0 | mto | BB_108_8_10 | 5 | 0.0492 | 0.0464 | 0.942 | 0.995 | +| tier0 | mto | BB_120_8_12 | 5 | 0.5875 | 0.5649 | 0.961 | 0.971 | +| tier0 | mto | BB_144_12_12 | 5 | 0.1203 | 0.1235 | 1.027 | 1.018 | +| tier0 | mto | BB_30_4_6 | 5 | 0.0340 | 0.0280 | 0.823 | 1.087 | +| tier0 | mto | BB_72_12_6 | 5 | 0.0323 | 0.0276 | 0.855 | 1.039 | +| tier0 | mto | BB_90_8_10 | 5 | 0.0549 | 0.0487 | 0.887 | 1.014 | +| tier0 | mto | COLOR_19_1_5 | 5 | 0.0244 | 0.0180 | 0.738 | 1.000 | +| tier0 | mto | COLOR_7_1_3 | 5 | 0.0229 | 0.0138 | 0.603 | 0.990 | +| tier0 | mto | GB_144_12_8 | 5 | 0.0682 | 0.0620 | 0.909 | 0.996 | +| tier0 | mto | HGP_106_16_4 | 5 | 0.0590 | 0.0513 | 0.869 | 0.980 | +| tier0 | mto | HGP_113_1_8 | 5 | 0.0700 | 0.0598 | 0.855 | 0.944 | +| tier0 | mto | HGP_13_1_3 | 5 | 0.0251 | 0.0135 | 0.537 | 0.903 | +| tier0 | mto | HGP_306_36_5 | 5 | 0.3514 | 0.3452 | 0.983 | 1.000 | +| tier0 | mto | HGP_41_1_5 | 5 | 0.0261 | 0.0215 | 0.823 | 1.000 | +| tier0 | mto | HGP_45_9_3 | 5 | 0.0242 | 0.0231 | 0.957 | 1.036 | +| tier0 | mto | LP_136_32_4 | 5 | 0.0550 | 0.0471 | 0.857 | 1.012 | +| tier0 | mto | LP_238_44_6 | 5 | 0.2506 | 0.2585 | 1.032 | 1.028 | +| tier0 | mto | LP_34_20_2 | 5 | 0.0247 | 0.0147 | 0.593 | 0.845 | +| tier0 | mto | TN_36_8_3 | 5 | 0.0273 | 0.0213 | 0.779 | 0.946 | +| tier0 | mto | TN_36_8_4 | 5 | 0.0269 | 0.0219 | 0.815 | 0.893 | +| tier0 | mto | TN_54_11_4 | 5 | 0.0478 | 0.0387 | 0.810 | 0.927 | +| tier0 | mto | TN_72_14_4 | 5 | 0.0597 | 0.0484 | 0.810 | 0.911 | +| tier0 | mto | TN_72_8_8 | 5 | 0.6436 | 0.6200 | 0.963 | 0.974 | +| tier0 | nocard | AMC_108_6_9 | 5 | 0.0897 | 0.0910 | 1.014 | 1.024 | +| tier0 | nocard | AMC_216_6_12 | 5 | 0.2769 | 0.2720 | 0.982 | 0.985 | +| tier0 | nocard | AMC_330_6_14 | 5 | 0.6725 | 0.6664 | 0.991 | 0.990 | +| tier0 | nocard | BB_108_8_10 | 5 | 0.0477 | 0.0439 | 0.919 | 1.064 | +| tier0 | nocard | BB_120_8_12 | 5 | 0.5319 | 0.5160 | 0.970 | 0.986 | +| tier0 | nocard | BB_144_12_12 | 5 | 0.1193 | 0.1179 | 0.989 | 1.005 | +| tier0 | nocard | BB_30_4_6 | 5 | 0.0225 | 0.0244 | 1.086 | 1.112 | +| tier0 | nocard | BB_72_12_6 | 5 | 0.0326 | 0.0258 | 0.793 | 1.025 | +| tier0 | nocard | BB_90_8_10 | 5 | 0.0483 | 0.0415 | 0.860 | 1.028 | +| tier0 | nocard | COLOR_19_1_5 | 5 | 0.0242 | 0.0178 | 0.739 | 1.008 | +| tier0 | nocard | COLOR_7_1_3 | 5 | 0.0234 | 0.0161 | 0.688 | 1.049 | +| tier0 | nocard | GB_144_12_8 | 5 | 0.0668 | 0.0612 | 0.917 | 0.978 | +| tier0 | nocard | HGP_106_16_4 | 5 | 0.0578 | 0.0464 | 0.803 | 0.952 | +| tier0 | nocard | HGP_113_1_8 | 5 | 0.0621 | 0.0510 | 0.822 | 0.959 | +| tier0 | nocard | HGP_13_1_3 | 5 | 0.0240 | 0.0135 | 0.561 | 0.904 | +| tier0 | nocard | HGP_306_36_5 | 5 | 0.3096 | 0.3028 | 0.978 | 0.998 | +| tier0 | nocard | HGP_41_1_5 | 5 | 0.0259 | 0.0198 | 0.761 | 1.020 | +| tier0 | nocard | HGP_45_9_3 | 5 | 0.0238 | 0.0203 | 0.854 | 1.039 | +| tier0 | nocard | LP_136_32_4 | 5 | 0.0548 | 0.0493 | 0.901 | 1.019 | +| tier0 | nocard | LP_238_44_6 | 5 | 0.2436 | 0.2490 | 1.022 | 1.014 | +| tier0 | nocard | LP_34_20_2 | 5 | 0.0254 | 0.0190 | 0.749 | 0.945 | +| tier0 | nocard | TN_36_8_3 | 5 | 0.0269 | 0.0200 | 0.744 | 0.892 | +| tier0 | nocard | TN_36_8_4 | 5 | 0.0354 | 0.0258 | 0.728 | 0.955 | +| tier0 | nocard | TN_54_11_4 | 5 | 0.0485 | 0.0374 | 0.770 | 0.979 | +| tier0 | nocard | TN_72_14_4 | 5 | 0.0553 | 0.0447 | 0.809 | 0.945 | +| tier0 | nocard | TN_72_8_8 | 5 | 0.5531 | 0.5362 | 0.969 | 0.976 | +| tier1 | cc | AMC_438_6_17 | 5 | 0.0778 | 0.0699 | 0.898 | 0.965 | +| tier1 | cc | BB_186_10_14 | 5 | 0.0414 | 0.0234 | 0.564 | 0.829 | +| tier1 | cc | BB_288_12_18 | 5 | 0.3146 | 0.3130 | 0.995 | 1.007 | +| tier1 | cc | COLOR_127_1_13 | 5 | 0.0627 | 0.0587 | 0.936 | 1.008 | +| tier1 | cc | GB_144_12_12 | 5 | 0.0709 | 0.0654 | 0.923 | 1.007 | +| tier1 | cc | HGP_265_1_12 | 5 | 0.0308 | 0.0255 | 0.828 | 0.921 | +| tier1 | cc | HGP_610_64_6 | 5 | 0.1471 | 0.1357 | 0.922 | 0.969 | +| tier1 | cc | LP_340_56_8 | 5 | 0.0272 | 0.0268 | 0.985 | 1.114 | +| tier1 | cc | LP_442_68_10 | 5 | 0.0298 | 0.0285 | 0.957 | 0.972 | +| tier1 | mto | AMC_438_6_17 | 5 | 7.9938 | 7.8562 | 0.983 | 0.977 | +| tier1 | mto | BB_186_10_14 | 5 | 1.1637 | 1.1350 | 0.975 | 0.978 | +| tier1 | mto | BB_288_12_18 | 5 | 9.9731 | 9.7827 | 0.981 | 0.980 | +| tier1 | mto | COLOR_127_1_13 | 5 | 1.3208 | 1.2798 | 0.969 | 0.975 | +| tier1 | mto | GB_144_12_12 | 5 | 1.0759 | 1.0499 | 0.976 | 0.978 | +| tier1 | mto | HGP_265_1_12 | 5 | 1.7066 | 1.6676 | 0.977 | 0.980 | +| tier1 | mto | HGP_610_64_6 | 5 | 8.1101 | 8.0034 | 0.987 | 0.999 | +| tier1 | mto | LP_340_56_8 | 5 | 1.8571 | 1.8146 | 0.977 | 0.981 | +| tier1 | mto | LP_442_68_10 | 5 | 4.9794 | 4.8794 | 0.980 | 0.976 | +| tier1 | nocard | AMC_438_6_17 | 5 | 7.7806 | 7.5688 | 0.973 | 0.966 | +| tier1 | nocard | BB_186_10_14 | 5 | 1.0473 | 1.0235 | 0.977 | 0.981 | +| tier1 | nocard | BB_288_12_18 | 5 | 10.0105 | 9.8113 | 0.980 | 0.980 | +| tier1 | nocard | COLOR_127_1_13 | 5 | 1.4968 | 1.4582 | 0.974 | 0.977 | +| tier1 | nocard | GB_144_12_12 | 5 | 1.0738 | 1.0582 | 0.985 | 0.984 | +| tier1 | nocard | HGP_265_1_12 | 5 | 1.7180 | 1.6769 | 0.976 | 0.983 | +| tier1 | nocard | HGP_610_64_6 | 5 | 8.6281 | 8.5126 | 0.987 | 0.988 | +| tier1 | nocard | LP_340_56_8 | 5 | 2.1456 | 2.1094 | 0.983 | 0.983 | +| tier1 | nocard | LP_442_68_10 | 5 | 4.0491 | 4.0201 | 0.993 | 0.976 | + +## Verdict per tier and mode + +| Tier | Mode | cells | geomean | worst cell | cells > 1.25 | verdict | +|---|---|---:|---:|---|---:|---| +| tier0 | cc | 26 | 0.666 | 0.964 (AMC_330_6_14) | 0 | PASS | +| tier0 | mto | 26 | 0.849 | 1.032 (LP_238_44_6) | 0 | PASS | +| tier0 | nocard | 26 | 0.853 | 1.086 (BB_30_4_6) | 0 | PASS | +| tier1 | cc | 9 | 0.879 | 0.995 (BB_288_12_18) | 0 | PASS | +| tier1 | mto | 9 | 0.978 | 0.987 (HGP_610_64_6) | 0 | PASS | +| tier1 | nocard | 9 | 0.981 | 0.993 (LP_442_68_10) | 0 | PASS | +| tier0 | all | 78 | 0.784 | 1.086 | 0 | PASS | +| tier1 | all | 27 | 0.945 | 0.995 | 0 | PASS | + +## Logs + +units with byte-identical stdout in every run of both arms: 522; other units: 3 (of which old itself varies across reps: 2; identical up to line order in every run: 3) +- ('tier1', 'cc', 'GB_144_12_12', 0): distinct stdouts old 2, new 2, same set: False +- ('tier1', 'cc', 'GB_144_12_12', 2): distinct stdouts old 2, new 2, same set: True +- ('tier1', 'cc', 'GB_144_12_12', 3): distinct stdouts old 1, new 2, same set: False + +## Answers + +runs: 9450; rc != 0 or answer != stem: 0 [] + +## Wait slack (wall - user - sys) of runs with wall < 0.2 s, in ms + +| Arm | runs | median | p90 | max | +|---|---:|---:|---:|---:| +| old | 3331 | 11.88 | 16.15 | 49.91 | +| new | 3337 | 4.77 | 7.82 | 19.38 | diff --git a/optimization/experiments/GH-224/raw/t01/config.json b/optimization/experiments/GH-224/raw/t01/config.json new file mode 100644 index 00000000..e28e96a0 --- /dev/null +++ b/optimization/experiments/GH-224/raw/t01/config.json @@ -0,0 +1,50 @@ +{ + "arms": { + "old": [ + "/home/yfc/mac-agent-20261009/frozen/server-gh224-main-fecee8c/distqldpc", + [] + ], + "new": [ + "/home/yfc/mac-agent-20261009/frozen/server-gh224-2587b9d/distqldpc", + [] + ] + }, + "cpus": [ + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101 + ], + "reps": 9, + "seeds": 5, + "modes": "mto,nocard,cc", + "limit": 600, + "units": 525, + "started": 1793815873.1662354 +} \ No newline at end of file diff --git a/optimization/experiments/GH-224/raw/t01/results.jsonl.gz b/optimization/experiments/GH-224/raw/t01/results.jsonl.gz new file mode 100644 index 00000000..b8c1f335 Binary files /dev/null and b/optimization/experiments/GH-224/raw/t01/results.jsonl.gz differ diff --git a/optimization/experiments/GH-224/raw/t01/skips.log b/optimization/experiments/GH-224/raw/t01/skips.log new file mode 100644 index 00000000..63cf72ab --- /dev/null +++ b/optimization/experiments/GH-224/raw/t01/skips.log @@ -0,0 +1,4 @@ +1793815874 cpu 84 busy, unit ('AMC_438_6_17', 'cc', 2) +1793816085 cpu 101 busy, unit ('BB_108_8_10', 'nocard', 0) +1793816086 cpu 97 busy, unit ('BB_108_8_10', 'cc', 2) +1793816109 cpu 85 busy, unit ('COLOR_19_1_5', 'cc', 0) diff --git a/optimization/experiments/GH-224/raw/t0tests/mac_test_cc.txt b/optimization/experiments/GH-224/raw/t0tests/mac_test_cc.txt new file mode 100644 index 00000000..5cde5cf9 --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/mac_test_cc.txt @@ -0,0 +1,62 @@ +c++ -Wno-reserved-user-defined-literal -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 +./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: 3600 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) +partB: 200 CSS codes (52 with a verified dual map, 51 with X-half orbits, 76 with dX != dZ, 54 with all-odd Hz), 9200 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, 37 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; 3300 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-195 partU: 300 half instances (200 with orbits), 259200 ladder runs (128 rule subsets with pack,erasure x 3 seeds x 2 gates, charge and bfs mixed in; 28800 with GH-181 tokens, 6278 of them pruned by erasure with redundant rows packed), 0 bad; erasure tests 122540960, prunes 121941834, give-ups 14376 with the production gate (240 instances pruned); tests 1586324, prunes 1534092 with the size gate (209 instances) +mutant 25 (erasure bound weakened by one: extra - 1 outside qubits): 1370/9600 half ladders wrong +mutant 26 (erasure with the fixed support S ignored): 2204/9600 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 +make test-cc CXX="c++ -Wno-reserved-user-defined-literal" 1579.37s user 9.16s system 99% cpu 26:35.32 total +rc=0 diff --git a/optimization/experiments/GH-224/raw/t0tests/mac_test_flags.txt b/optimization/experiments/GH-224/raw/t0tests/mac_test_flags.txt new file mode 100644 index 00000000..398fd0ad --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/mac_test_flags.txt @@ -0,0 +1,5 @@ +bash tests/test_cc_flags.sh ./bin/distqldpc +test_cc_flags: 566 checks, 0 failed +CC_FLAG_TESTS PASS +make test-cc-flags CXX="c++ -Wno-reserved-user-defined-literal" 5.28s user 1.91s system 85% cpu 8.385 total +rc=0 diff --git a/optimization/experiments/GH-224/raw/t0tests/partition_new.txt b/optimization/experiments/GH-224/raw/t0tests/partition_new.txt new file mode 100644 index 00000000..c0dc325c --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/partition_new.txt @@ -0,0 +1,672 @@ +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 3 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 96 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=12, hconfls=12, core 7, tier2 0, local 0, 2 soft cls unsat (1 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 9, nbFixedLH 0 +c nbHardens 5 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 9, phase 20000000, starts 1, UP 245 +c UB=2 fails, cnfls=12, hcnfls=12, core 7, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 5 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 9, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 12 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 49(14.08%), hardens 5 (fixed 10), dynVars 95, shorten: 0 +c restarts : 4 +c conflicts : 12 (inf /sec) +c decisions : 82 (0.00 % random) (inf /sec) +c propagations : 348 (inf /sec) +c conflict literals : 19 (5.00 % deleted) +c Memory used : 13.00 MB +c CPU time : 0 s +c nbSimplifyAll : 0 +c s_propagations : 98 +c s_cost_ratio : 28.16% + +s UNSATISFIABLE +Partition regression passed: all 1024 assignments checked; optimum 5. +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 3 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 96 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=12, hconfls=12, core 6, tier2 0, local 0, 2 soft cls unsat (1 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 9, nbFixedLH 0 +c nbHardens 5 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 9, phase 20000000, starts 1, UP 222 +c UB=2 fails, cnfls=12, hcnfls=12, core 6, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 5 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 9, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 12 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 49(15.22%), hardens 5 (fixed 10), dynVars 95, shorten: 0 +c restarts : 4 +c conflicts : 12 (9615 /sec) +c decisions : 81 (0.00 % random) (64904 /sec) +c propagations : 322 (258013 /sec) +c conflict literals : 18 (5.26 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.001248 s +c nbSimplifyAll : 0 +c s_propagations : 98 +c s_cost_ratio : 30.43% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=2, hconfls=2, core 1, tier2 0, local 0, 2 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 1, nbFixedLH 0 +c nbHardens 1 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 2 conflicts with init 9999 + +c UB=2 fails, cnfls=2, hcnfls=2, core 1, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 1, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 2 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 47(64.38%), hardens 1 (fixed 10), dynVars 51, shorten: 0 +c restarts : 3 +c conflicts : 2 (2051 /sec) +c decisions : 18 (0.00 % random) (18462 /sec) +c propagations : 73 (74872 /sec) +c conflict literals : 2 (0.00 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.000975 s +c nbSimplifyAll : 0 +c s_propagations : 90 +c s_cost_ratio : 123.29% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 3 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 96 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=12, hconfls=12, core 6, tier2 0, local 0, 2 soft cls unsat (1 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 9, nbFixedLH 0 +c nbHardens 5 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 9, phase 20000000, starts 1, UP 222 +c UB=2 fails, cnfls=12, hcnfls=12, core 6, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 5 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 9, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 12 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 49(15.22%), hardens 5 (fixed 10), dynVars 95, shorten: 0 +c restarts : 4 +c conflicts : 12 (inf /sec) +c decisions : 81 (0.00 % random) (inf /sec) +c propagations : 322 (inf /sec) +c conflict literals : 18 (5.26 % deleted) +c Memory used : 13.00 MB +c CPU time : 0 s +c nbSimplifyAll : 0 +c s_propagations : 98 +c s_cost_ratio : 30.43% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=2, hconfls=2, core 1, tier2 0, local 0, 2 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 1, nbFixedLH 0 +c nbHardens 1 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 2 conflicts with init 9999 + +c UB=2 fails, cnfls=2, hcnfls=2, core 1, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 1, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 2 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 47(64.38%), hardens 1 (fixed 10), dynVars 51, shorten: 0 +c restarts : 3 +c conflicts : 2 (2058 /sec) +c decisions : 18 (0.00 % random) (18519 /sec) +c propagations : 73 (75103 /sec) +c conflict literals : 2 (0.00 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.000972 s +c nbSimplifyAll : 0 +c s_propagations : 90 +c s_cost_ratio : 123.29% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 3 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 96 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=12, hconfls=12, core 6, tier2 0, local 0, 2 soft cls unsat (1 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 9, nbFixedLH 0 +c nbHardens 5 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 9, phase 20000000, starts 1, UP 222 +c UB=2 fails, cnfls=12, hcnfls=12, core 6, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 5 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 9, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 12 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 49(15.22%), hardens 5 (fixed 10), dynVars 95, shorten: 0 +c restarts : 4 +c conflicts : 12 (32000 /sec) +c decisions : 81 (0.00 % random) (216000 /sec) +c propagations : 322 (858667 /sec) +c conflict literals : 18 (5.26 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.000375 s +c nbSimplifyAll : 0 +c s_propagations : 98 +c s_cost_ratio : 30.43% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=2, hconfls=2, core 1, tier2 0, local 0, 2 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 1, nbFixedLH 0 +c nbHardens 1 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 2 conflicts with init 9999 + +c UB=2 fails, cnfls=2, hcnfls=2, core 1, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 1, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 2 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 47(64.38%), hardens 1 (fixed 10), dynVars 51, shorten: 0 +c restarts : 3 +c conflicts : 2 (2068 /sec) +c decisions : 18 (0.00 % random) (18614 /sec) +c propagations : 73 (75491 /sec) +c conflict literals : 2 (0.00 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.000967 s +c nbSimplifyAll : 0 +c s_propagations : 90 +c s_cost_ratio : 123.29% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 2, nbFixedLH 0 +c nbHardens 3 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 96 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=12, hconfls=12, core 6, tier2 0, local 0, 2 soft cls unsat (1 at L0), 26 fixed vars at L0, softCnfl 0, nbFlyRd 9, nbFixedLH 0 +c nbHardens 5 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 9, phase 20000000, starts 1, UP 222 +c UB=2 fails, cnfls=12, hcnfls=12, core 6, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 5 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 9, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 12 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 49(15.22%), hardens 5 (fixed 10), dynVars 95, shorten: 0 +c restarts : 4 +c conflicts : 12 (12474 /sec) +c decisions : 81 (0.00 % random) (84200 /sec) +c propagations : 322 (334719 /sec) +c conflict literals : 18 (5.26 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.000962 s +c nbSimplifyAll : 0 +c s_propagations : 98 +c s_cost_ratio : 30.43% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 13, of which 10 unit, 3 nonUnit and 0 empty +c total nb of literals: 57 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 1 conflict sets found with length 3 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 10 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 53 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 10), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 107 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=2, hconfls=2, core 1, tier2 0, local 0, 2 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 1, nbFixedLH 0 +c nbHardens 1 (fixed 10), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 2 conflicts with init 9999 + +c UB=2 fails, cnfls=2, hcnfls=2, core 1, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 10), lk: 0, shorten: 0, pureSo 0, nbFlyRd 1, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 8, hardConflicts: 2 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 47(64.38%), hardens 1 (fixed 10), dynVars 51, shorten: 0 +c restarts : 3 +c conflicts : 2 (inf /sec) +c decisions : 18 (0.00 % random) (inf /sec) +c propagations : 73 (inf /sec) +c conflict literals : 2 (0.00 % deleted) +c Memory used : 13.00 MB +c CPU time : 0 s +c nbSimplifyAll : 0 +c s_propagations : 90 +c s_cost_ratio : 123.29% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 14, of which 10 unit, 4 nonUnit and 0 empty +c total nb of literals: 61 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 3 conflict sets found with length 10 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 11 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 11), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 59 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 11), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 120 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 0, nbFixedLH 0 +c nbHardens 3 (fixed 11), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 107 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=8, hconfls=8, core 7, tier2 0, local 0, 2 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 0, nbFixedLH 0 +c nbHardens 7 (fixed 11), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 5, phase 20000000, starts 1, UP 230 +c UB=2 fails, cnfls=8, hcnfls=8, core 7, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 7 (fixed 11), lk: 0, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 9, hardConflicts: 8 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 52(14.77%), hardens 7 (fixed 11), dynVars 106, shorten: 0 +c restarts : 4 +c conflicts : 8 (4825 /sec) +c decisions : 87 (0.00 % random) (52473 /sec) +c propagations : 352 (212304 /sec) +c conflict literals : 21 (25.00 % deleted) +c Memory used : 13.00 MB +c CPU time : 0.001658 s +c nbSimplifyAll : 0 +c s_propagations : 114 +c s_cost_ratio : 32.39% + +s UNSATISFIABLE +c This is COMiniSatPS. +c WARNING: for repeatability, setting FPU to use double precision +c ============================[ Problem Statistics ]============================= +c | | +c initial UB: 2147483647 +c | Number of variables: 10 | +c | Number of clauses: 15 | +c | Parse time: 0.00 s | +c | | +c ============================[ Search Statistics ]============================== +c | Conflicts | ORIGINAL | LEARNT | Progress | +c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | +c =============================================================================== +c nb soft clauses: 14, of which 10 unit, 4 nonUnit and 0 empty +c total nb of literals: 61 +c conflLits 3, conflLits2 0, nbFailedLits 0, fixedVarsBypreproc 0, totalFixedVars 0 +c init nbIsets: 4 +c nbIsets after pass 1: 3 +c isets 3, derivedCost 3 +c 2 conflict sets found with length 7 +c fixedCost 0, nbSatLits 0, totalFixedVars 0, objForSearch: 11 + +c no UB provided, search from scratch... +c ends of initiationization by VSIDS at 0 conflicts with init 10000 + +c UB=1 fails, cnfls=0, hcnfls=0, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 1 (fixed 11), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 59 (Sinz+MTO) for UB 2 +c ends of initiationization by VSIDS at 1 conflicts with init 9999 + +c UB=2 fails, cnfls=1, hcnfls=1, core 0, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 2.00, dev 0.00, succRate 1.00, nbSucc 1, nbHardens 1 (fixed 11), lk: 1, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 + +c Cardinality: 120 (Sinz+MTO) for UB 4 +c UB=4 succs, confls=3, hconfls=3, core 2, tier2 0, local 0, 3 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 0, nbFixedLH 0 +c nbHardens 3 (fixed 11), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c ends of initiationization by VSIDS at 3 conflicts with init 9998 + + +c Cardinality: 107 (Sinz+MTO) for UB 3 +c UB=3 succs, confls=7, hconfls=7, core 6, tier2 0, local 0, 2 soft cls unsat (0 at L0), 0 fixed vars at L0, softCnfl 0, nbFlyRd 0, nbFixedLH 0 +c nbHardens 5 (fixed 11), shorten: 0, prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, lk: 0, shorten: 0, quasiC: 0 (fixed: 0) + +c LRB phase 1: conflicts 4, phase 20000000, starts 1, UP 185 +c UB=2 fails, cnfls=7, hcnfls=7, core 6, tier2 0, local 0, quasiC: 0 (fixed: 0) +c prunedLB 0.00, dev 0.00, succRate 0.00, nbSucc 0, nbHardens 5 (fixed 11), lk: 0, shorten: 0, pureSo 0, nbFlyRd 0, nbFixedLH 0 +c =============================================================================== +c initCost: 0, fixedBySearch: 0, optimal: 5, maxsat: 9, hardConflicts: 7 +c nbLK: 2, nbSuccLK: 1(50.00%), nbLKup: 40(13.29%), hardens 5 (fixed 11), dynVars 106, shorten: 0 +c restarts : 4 +c conflicts : 7 (inf /sec) +c decisions : 77 (0.00 % random) (inf /sec) +c propagations : 301 (inf /sec) +c conflict literals : 17 (5.56 % deleted) +c Memory used : 13.00 MB +c CPU time : 0 s +c nbSimplifyAll : 0 +c s_propagations : 110 +c s_cost_ratio : 36.54% + +s UNSATISFIABLE +Partition adjacent oracles passed: 11 total inputs, 1024 assignments each. +rc=0 diff --git a/optimization/experiments/GH-224/raw/t0tests/smoke_new.txt b/optimization/experiments/GH-224/raw/t0tests/smoke_new.txt new file mode 100644 index 00000000..45c32d6f --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/smoke_new.txt @@ -0,0 +1,2 @@ +DistQLDPC smoke validation passed +rc=0 diff --git a/optimization/experiments/GH-224/raw/t0tests/test_cc_new.txt b/optimization/experiments/GH-224/raw/t0tests/test_cc_new.txt new file mode 100644 index 00000000..5579b0ba --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/test_cc_new.txt @@ -0,0 +1,86 @@ +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:48, + from tests/test_cc_engine.cc:102: +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:1865:29: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 1865 | 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:1310:29: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 1310 | 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:172:20: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 172 | (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: 3600 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) +partB: 200 CSS codes (52 with a verified dual map, 51 with X-half orbits, 76 with dX != dZ, 54 with all-odd Hz), 9200 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, 38 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; 3300 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-195 partU: 300 half instances (200 with orbits), 259200 ladder runs (128 rule subsets with pack,erasure x 3 seeds x 2 gates, charge and bfs mixed in; 28800 with GH-181 tokens, 6278 of them pruned by erasure with redundant rows packed), 0 bad; erasure tests 122540960, prunes 121941834, give-ups 14376 with the production gate (240 instances pruned); tests 1586324, prunes 1534092 with the size gate (209 instances) +mutant 25 (erasure bound weakened by one: extra - 1 outside qubits): 1370/9600 half ladders wrong +mutant 26 (erasure with the fixed support S ignored): 2204/9600 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-224/raw/t0tests/test_cc_old.txt b/optimization/experiments/GH-224/raw/t0tests/test_cc_old.txt new file mode 100644 index 00000000..fb3ef240 --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/test_cc_old.txt @@ -0,0 +1,86 @@ +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:102: +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:1864:29: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 1864 | 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:1309:29: warning: ignoring return value of ‘ssize_t write(int, const void*, size_t)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] + 1309 | 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: 3600 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) +partB: 200 CSS codes (52 with a verified dual map, 51 with X-half orbits, 76 with dX != dZ, 54 with all-odd Hz), 9200 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, 37 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; 3300 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-195 partU: 300 half instances (200 with orbits), 259200 ladder runs (128 rule subsets with pack,erasure x 3 seeds x 2 gates, charge and bfs mixed in; 28800 with GH-181 tokens, 6278 of them pruned by erasure with redundant rows packed), 0 bad; erasure tests 122540960, prunes 121941834, give-ups 14376 with the production gate (240 instances pruned); tests 1586324, prunes 1534092 with the size gate (209 instances) +mutant 25 (erasure bound weakened by one: extra - 1 outside qubits): 1370/9600 half ladders wrong +mutant 26 (erasure with the fixed support S ignored): 2204/9600 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-224/raw/t0tests/test_flags_new.txt b/optimization/experiments/GH-224/raw/t0tests/test_flags_new.txt new file mode 100644 index 00000000..72b5e4cd --- /dev/null +++ b/optimization/experiments/GH-224/raw/t0tests/test_flags_new.txt @@ -0,0 +1,4 @@ +bash tests/test_cc_flags.sh ./bin/distqldpc +test_cc_flags: 566 checks, 0 failed +CC_FLAG_TESTS PASS +rc=0 diff --git a/optimization/experiments/GH-224/raw/t2spot/config.json b/optimization/experiments/GH-224/raw/t2spot/config.json new file mode 100644 index 00000000..4c75b5de --- /dev/null +++ b/optimization/experiments/GH-224/raw/t2spot/config.json @@ -0,0 +1,38 @@ +{ + "arms": { + "old": [ + "/home/yfc/mac-agent-20261009/frozen/server-gh224-main-fecee8c/distqldpc", + [] + ], + "new": [ + "/home/yfc/mac-agent-20261009/frozen/server-gh224-2587b9d/distqldpc", + [] + ] + }, + "cpus": [ + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89 + ], + "reps": 3, + "seeds": 3, + "modes": "mto,nocard,cc", + "limit": 1800, + "units": 27, + "started": 1793816191.7475114 +} \ No newline at end of file diff --git a/optimization/experiments/GH-224/raw/t2spot/results.jsonl.gz b/optimization/experiments/GH-224/raw/t2spot/results.jsonl.gz new file mode 100644 index 00000000..dbfb898a Binary files /dev/null and b/optimization/experiments/GH-224/raw/t2spot/results.jsonl.gz differ diff --git a/optimization/experiments/GH-224/raw/t2spot/skips.log b/optimization/experiments/GH-224/raw/t2spot/skips.log new file mode 100644 index 00000000..b06b2c20 --- /dev/null +++ b/optimization/experiments/GH-224/raw/t2spot/skips.log @@ -0,0 +1 @@ +1793816192 cpu 84 busy, unit ('TN_108_2_12', 'nocard', 0) diff --git a/optimization/experiments/GH-224/raw/t3spot/config.json b/optimization/experiments/GH-224/raw/t3spot/config.json new file mode 100644 index 00000000..7d7b0af4 --- /dev/null +++ b/optimization/experiments/GH-224/raw/t3spot/config.json @@ -0,0 +1,32 @@ +{ + "arms": { + "old": [ + "/home/yfc/mac-agent-20261009/frozen/server-gh224-main-fecee8c/distqldpc", + [] + ], + "new": [ + "/home/yfc/mac-agent-20261009/frozen/server-gh224-2587b9d/distqldpc", + [] + ] + }, + "cpus": [ + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101 + ], + "reps": 3, + "seeds": 3, + "modes": "cc", + "limit": 1800, + "units": 9, + "started": 1793816191.745035 +} \ No newline at end of file diff --git a/optimization/experiments/GH-224/raw/t3spot/results.jsonl.gz b/optimization/experiments/GH-224/raw/t3spot/results.jsonl.gz new file mode 100644 index 00000000..ed3a85d8 Binary files /dev/null and b/optimization/experiments/GH-224/raw/t3spot/results.jsonl.gz differ diff --git a/optimization/experiments/GH-224/runner/analyze.py b/optimization/experiments/GH-224/runner/analyze.py new file mode 100644 index 00000000..885d5669 --- /dev/null +++ b/optimization/experiments/GH-224/runner/analyze.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""GH-224 judgement of an interleave.py panel. Cell = (tier, mode, stem); per seed the median over the repetitions, then +the median over the seeds; ratio = cell(arm) / cell(ref). Per tier x mode: geomean, worst cell, cells > 1.25 +(pass = geomean < 1 and no cell > 1.25). Also: answers vs the stem, stdout identity (ref vs arm, per unit), and the +wait slack (wall - user - sys of the process tree) of fast runs, which shows the 10 ms polling floor. +usage: analyze.py REF ARM results.jsonl [--slack-max 0.2]""" +import collections, json, math, statistics as st, sys +REF, ARM, path = sys.argv[1], sys.argv[2], sys.argv[3] +SLACK_MAX = float(sys.argv[5]) if len(sys.argv) > 5 else 0.2 +R = [json.loads(l) for l in open(path)] +g = lambda v: math.exp(sum(map(math.log, v)) / len(v)) +U = collections.defaultdict(lambda: collections.defaultdict(list)) # (tier, mode, stem, seed) -> arm -> runs +for r in R: U[(r['tier'], r['mode'], r['stem'], r['seed'])][r['arm']].append(r) + + +def stem_d(stem): + f = stem.split('_')[3] + return int(f) if f.isdigit() else None + + +bad_ans = [(r['stem'], r['mode'], r['seed'], r['arm'], r['o'], r['rc']) for r in R + if r['rc'] != 0 or r['o'] is None or (stem_d(r['stem']) is not None and int(r['o'].split()[1]) != stem_d(r['stem']))] +C = collections.defaultdict(dict) +for (tier, mode, stem, seed), d in U.items(): + if REF in d and ARM in d: + C[(tier, mode, stem)][seed] = {a: (st.median(x['wall'] for x in d[a]), st.median(x['utime'] + x['stime'] for x in d[a])) + for a in (REF, ARM)} +print(f'## Cells ({ARM} vs {REF}; median over reps, then over seeds; wall in s)\n') +print(f'| Tier | Mode | Code | seeds | {REF} wall | {ARM} wall | wall ratio | cpu ratio |') +print('|---|---|---|---:|---:|---:|---:|---:|') +per = collections.defaultdict(list) +for (tier, mode, stem), d in sorted(C.items()): + w0 = st.median(v[REF][0] for v in d.values()); w1 = st.median(v[ARM][0] for v in d.values()) + c0 = st.median(v[REF][1] for v in d.values()); c1 = st.median(v[ARM][1] for v in d.values()) + per[(tier, mode)].append((w1 / w0, stem)) + print(f'| {tier} | {mode} | {stem} | {len(d)} | {w0:.4f} | {w1:.4f} | {w1 / w0:.3f} | {c1 / max(c0, 1e-9):.3f} |') +print(f'\n## Verdict per tier and mode\n') +print('| Tier | Mode | cells | geomean | worst cell | cells > 1.25 | verdict |') +print('|---|---|---:|---:|---|---:|---|') +for (tier, mode), v in sorted(per.items()): + rs = [x for x, _ in v]; mx = max(v) + print(f'| {tier} | {mode} | {len(v)} | {g(rs):.3f} | {mx[0]:.3f} ({mx[1]}) | {sum(x > 1.25 for x in rs)} | ' + f'{"PASS" if g(rs) < 1 and mx[0] <= 1.25 else "FAIL"} |') +for tier in sorted({t for t, _ in per}): + rs = [x for (t, _), v in per.items() if t == tier for x, _ in v] + print(f'| {tier} | all | {len(rs)} | {g(rs):.3f} | {max(rs):.3f} | {sum(x > 1.25 for x in rs)} | ' + f'{"PASS" if g(rs) < 1 and max(rs) <= 1.25 else "FAIL"} |') +# stdout identity per unit +same = differ = 0; nondet_ref = 0; diff_units = [] +for k, d in U.items(): + if REF not in d or ARM not in d: continue + s0 = {x['stdout'] for x in d[REF]}; s1 = {x['stdout'] for x in d[ARM]} + if len(s0) > 1: nondet_ref += 1 + if s0 == s1 and len(s0) == 1: same += 1 + else: differ += 1; diff_units.append((k, len(s0), len(s1), s0 == s1)) +ms_same = sum(1 for k, n0, n1, eq in diff_units + if len({tuple(sorted(x['stdout'].splitlines())) for a in (REF, ARM) for x in U[k][a]}) == 1) +print(f'\n## Logs\n\nunits with byte-identical stdout in every run of both arms: {same}; other units: {differ} ' + f'(of which {REF} itself varies across reps: {nondet_ref}; identical up to line order in every run: {ms_same})') +for k, n0, n1, eq in sorted(diff_units)[:40]: + print(f'- {k}: distinct stdouts {REF} {n0}, {ARM} {n1}, same set: {eq}') +print(f'\n## Answers\n\nruns: {len(R)}; rc != 0 or answer != stem: {len(bad_ans)} {bad_ans[:10]}') +# slack of fast runs +print(f'\n## Wait slack (wall - user - sys) of runs with wall < {SLACK_MAX} s, in ms\n') +print('| Arm | runs | median | p90 | max |') +print('|---|---:|---:|---:|---:|') +for a in (REF, ARM): + s = sorted(1000 * (r['wall'] - r['utime'] - r['stime']) for r in R if r['arm'] == a and r['wall'] < SLACK_MAX) + if s: print(f'| {a} | {len(s)} | {st.median(s):.2f} | {s[int(0.9 * (len(s) - 1))]:.2f} | {s[-1]:.2f} |') diff --git a/optimization/experiments/GH-224/runner/arms_gh224.json b/optimization/experiments/GH-224/runner/arms_gh224.json new file mode 100644 index 00000000..2fc482ef --- /dev/null +++ b/optimization/experiments/GH-224/runner/arms_gh224.json @@ -0,0 +1,2 @@ +{"old": ["/home/yfc/mac-agent-20261009/frozen/server-gh224-main-fecee8c/distqldpc", []], + "new": ["/home/yfc/mac-agent-20261009/frozen/server-gh224-2587b9d/distqldpc", []]} diff --git a/optimization/experiments/GH-224/runner/behaviour.sh b/optimization/experiments/GH-224/runner/behaviour.sh new file mode 100644 index 00000000..2bf849c7 --- /dev/null +++ b/optimization/experiments/GH-224/runner/behaviour.sh @@ -0,0 +1,36 @@ +#!/bin/bash +# GH-224 behaviour checks, old vs new binary, one pinned core (arg 1), 4 GB cap unless stated: +# (1) -cpu-lim wall deadline -> SIGKILL -> TIMEOUT with bounds (MaxSAT and CC); +# (2) a tighter memory cap (prlimit --as) that the child exceeds; +# (3) the child killed from outside (SIGKILL) -> UNKNOWN at once; (4) the child stopped and continued (SIGSTOP/SIGCONT). +# usage (from a worktree root): behaviour.sh CORE OLD NEW [WORKDIR] +C=$1; OLD=$2; NEW=$3; W=${4:-.} +run() { # run LABEL AS_BYTES ARGS... + local lab=$1 as=$2; shift 2 + for arm in old new; do + b=$OLD; [[ $arm == new ]] && b=$NEW + t0=$(date +%s.%N) + out=$(taskset -c $C prlimit --as=$as -- $b "$@" 2>&1 < /dev/null); rc=$? + t1=$(date +%s.%N) + printf '%-28s %-4s rc=%d wall=%.3f %s\n' "$lab" $arm $rc $(echo "$t1 - $t0" | bc) "$(echo "$out" | grep -E '^(c d_lb|c d_ub|c status|o |s |c d )' | tr '\n' '|' )" + done +} +run timeout-maxsat 4294967296 -cpu-lim=3 TN_250_10_15 +run timeout-cc 4294967296 -engine=cc -cpu-lim=3 $(ls data/matrices/tier5 | grep _Hx | grep BB_756 | sed s/_Hx.txt//) +run memcap-200M 209715200 -cpu-lim=60 $(ls data/matrices/tier5 | grep _Hx | grep LP_2610 | sed s/_Hx.txt//) +run memcap-60M-cc 62914560 -engine=cc -cpu-lim=60 $(ls data/matrices/tier5 | grep _Hx | grep LP_2610 | sed s/_Hx.txt//) +for arm in old new; do # (3) external SIGKILL of the child after 1 s + b=$OLD; [[ $arm == new ]] && b=$NEW + t0=$(date +%s.%N) + taskset -c $C prlimit --as=4294967296 -- $b -cpu-lim=60 TN_250_10_15 > $W/gh224_kill_$arm.txt 2>&1 < /dev/null & + p=$!; sleep 1; ch=$(pgrep -P $p -n) + tk=$(date +%s.%N); kill -9 $ch; wait $p; rc=$?; t1=$(date +%s.%N) + printf '%-28s %-4s rc=%d after-kill=%.3f %s\n' child-sigkill $arm $rc $(echo "$t1 - $tk" | bc) "$(grep -E '^(c status|s |o )' $W/gh224_kill_$arm.txt | tr '\n' '|')" +done +for arm in old new; do # (4) SIGSTOP the child for 2 s, then SIGCONT; the run must finish normally + b=$OLD; [[ $arm == new ]] && b=$NEW + t0=$(date +%s.%N) + taskset -c $C prlimit --as=4294967296 -- $b -cpu-lim=60 LP_442_68_10 > $W/gh224_stop_$arm.txt 2>&1 < /dev/null & + p=$!; sleep 0.5; ch=$(pgrep -P $p -n); kill -STOP $ch; sleep 2; kill -CONT $ch; wait $p; rc=$?; t1=$(date +%s.%N) + printf '%-28s %-4s rc=%d wall=%.3f %s\n' child-stop-cont $arm $rc $(echo "$t1 - $t0" | bc) "$(grep -E '^(c status|s |o )' $W/gh224_stop_$arm.txt | tr '\n' '|')" +done diff --git a/optimization/experiments/GH-224/runner/interleave.py b/optimization/experiments/GH-224/runner/interleave.py new file mode 100644 index 00000000..9bd15218 --- /dev/null +++ b/optimization/experiments/GH-224/runner/interleave.py @@ -0,0 +1,108 @@ +#!/usr/bin/env python3 +"""GH-224 interleaved A/B panel for yfclab2 (after GH-217 rep.py and gh217_queue.py). + +A unit is (stem, mode, seed). One unit runs REPS rounds on one pinned core; each round runs every arm once, and the arm +order rotates from round to round (old,new / new,old / ...), so slow phases of the machine hit every arm. Units are +spread over the given cores (72-103 only). Before each unit, the worker samples its core c and the SMT sibling c+128 for +0.5 s (/proc/stat) and skips the core for 20 s if either is busier than 15 %. Every process: + taskset -c C prlimit --as=4294967296 -- BIN ARM_ARGS MODE_ARGS -seed=S -cpu-lim=LIMIT CODE (stdin /dev/null) +Wall time = time.monotonic() around the process; user/sys time from wait4. stdout is stored per run. + +usage: interleave.py --arms ARMS.json --cpus 72-103 --reps 9 --seeds 5 --modes mto,nocard,cc --limit 600 --out DIR STEM... + ARMS.json: {"old": ["/path/bin", [extra args]], "new": [...]} (first arm = reference) + modes: mto = default MaxSAT (both cardinality encodings), nocard = MaxSAT -no-card, cc = -engine=cc (CC defaults) +""" +import argparse, glob, json, os, queue, subprocess, threading, time + +MODES = {'mto': [], 'nocard': ['-no-card'], 'cc': ['-engine=cc']} +ap = argparse.ArgumentParser() +ap.add_argument('--arms', required=True); ap.add_argument('--cpus', required=True) +ap.add_argument('--reps', type=int, default=9); ap.add_argument('--seeds', type=int, default=5) +ap.add_argument('--modes', default='mto,nocard,cc'); ap.add_argument('--limit', type=int, default=600) +ap.add_argument('--out', required=True); ap.add_argument('stems', nargs='+') +a = ap.parse_args() +arms = json.load(open(a.arms)) +cpus = [] +for part in a.cpus.split(','): + lo, _, hi = part.partition('-'); cpus += list(range(int(lo), int(hi or lo) + 1)) +assert cpus and all(72 <= c <= 103 for c in cpus), 'GH-224: yfclab2 logical CPUs 72-103 only' +os.makedirs(a.out + '/tmp', exist_ok=True) +done = set() +if os.path.exists(f'{a.out}/results.jsonl'): + for l in open(f'{a.out}/results.jsonl'): + r = json.loads(l); done.add((r['stem'], r['mode'], r['seed'])) + + +def code_of(stem): + f = glob.glob(f'data/matrices/*/{stem}_Hx.txt') + assert len(f) == 1, (stem, f) + return f[0][:-7], os.path.basename(os.path.dirname(f[0])) + + +units = [(s, m, seed) for s in a.stems for m in a.modes.split(',') for seed in range(a.seeds) if (s, m, seed) not in done] +q = queue.Queue(); [q.put(u) for u in units] +lock = threading.Lock() + + +def stat(): + d = {} + for l in open('/proc/stat'): + if l.startswith('cpu') and l[3].isdigit(): + f = l.split(); v = list(map(int, f[1:])); d[int(f[0][3:])] = (sum(v), v[3] + v[4]) + return d + + +def busy(c): + x = stat(); time.sleep(0.5); y = stat(); out = [] + for k in (c, c + 128): + t = y[k][0] - x[k][0]; out.append(1 - (y[k][1] - x[k][1]) / t if t else 0.0) + return max(out) + + +def run_one(cpu, b, args, code): + cmd = ['taskset', '-c', str(cpu), 'prlimit', '--as=4294967296', '--', b] + args + [f'-cpu-lim={a.limit}', code] + fo, fe = f'{a.out}/tmp/{cpu}.out', f'{a.out}/tmp/{cpu}.err' + with open(fo, 'w') as so, open(fe, 'w') as se: + t0 = time.monotonic() + p = subprocess.Popen(cmd, stdout=so, stderr=se, stdin=subprocess.DEVNULL) + _, st, ru = os.wait4(p.pid, 0) + wall = time.monotonic() - t0 + p.returncode = os.waitstatus_to_exitcode(st) + return wall, p.returncode, ru, open(fo).read(), open(fe).read() + + +def worker(cpu): + while True: + try: u = q.get_nowait() + except queue.Empty: return + tries = 0 + while busy(cpu) > 0.15: + tries += 1 + with lock: + with open(f'{a.out}/skips.log', 'a') as f: f.write(f'{time.time():.0f} cpu {cpu} busy, unit {u}\n') + time.sleep(20) + stem, mode, seed = u + code, tier = code_of(stem) + names = list(arms) + for rep in range(a.reps): + order = names[rep % len(names):] + names[:rep % len(names)] + for arm in order: + b, extra = arms[arm] + args = extra + MODES[mode] + [f'-seed={seed}'] + wall, rc, ru, out, err = run_one(cpu, b, args, code) + o = [l for l in out.splitlines() if l.startswith('o ')] + rec = dict(stem=stem, tier=tier, mode=mode, seed=seed, rep=rep, arm=arm, cpu=cpu, wall=round(wall, 6), + utime=round(ru.ru_utime, 4), stime=round(ru.ru_stime, 4), maxrss_kb=ru.ru_maxrss, + rc=rc, o=o[-1] if o else None, stdout=out, stderr=err[-2000:], start=time.time()) + with lock: + with open(f'{a.out}/results.jsonl', 'a') as f: f.write(json.dumps(rec) + '\n') + with lock: + print(f'{stem} {mode} s{seed} cpu{cpu} done', flush=True) + + +json.dump(dict(arms=arms, cpus=cpus, reps=a.reps, seeds=a.seeds, modes=a.modes, limit=a.limit, units=len(units), + started=time.time()), open(f'{a.out}/config.json', 'w'), indent=1) +ts = [threading.Thread(target=worker, args=(c,)) for c in cpus] +[t.start() for t in ts]; [t.join() for t in ts] +open(f'{a.out}/RUNNER_DONE', 'w').write(f'{time.time():.0f} {len(units)} units\n') +print('done', len(units), 'units') diff --git a/src/core/distqldpc.cc b/src/core/distqldpc.cc index 3282db79..10167e13 100644 --- a/src/core/distqldpc.cc +++ b/src/core/distqldpc.cc @@ -42,6 +42,7 @@ #include #include #include +#include /* GH-224 */ #include "utils/System.h" #include "SimpSolver.h" @@ -2200,17 +2201,18 @@ static void apply_pipe_line(BoundsBook& b, const char* line, ProgressState* prog } } -static void drain_bounds_pipe(int pipe_r, BoundsBook& b, std::string& carry, ProgressState* prog) { +/* Returns true once the pipe has reached end of file (every write end closed). */ +static bool drain_bounds_pipe(int pipe_r, BoundsBook& b, std::string& carry, ProgressState* prog) { char chunk[512]; for (;;) { ssize_t n = read(pipe_r, chunk, sizeof(chunk)); if (n < 0) { if (errno == EINTR) continue; - break; + return false; } if (n == 0) - break; + return true; carry.append(chunk, chunk + n); size_t pos; while ((pos = carry.find('\n')) != std::string::npos) { @@ -2221,6 +2223,31 @@ static void drain_bounds_pipe(int pipe_r, BoundsBook& b, std::string& carry, Pro } } +/* GH-224: SIGCHLD self-pipe. While the parent waits for the solver child, SIGCHLD writes one byte here so that + * the parent's poll() returns as soon as the child exits (the old loop slept 10 ms per check, which quantized the + * wall time of fast runs into 10 ms buckets). */ +static volatile int g_sigchld_wake_w = -1; + +static void sigchld_wake(int) { + int saved = errno; + int fd = g_sigchld_wake_w; + if (fd >= 0) { + char c = 0; + ssize_t r = write(fd, &c, 1); /* non-blocking; a full pipe already guarantees a wake-up */ + (void)r; + } + errno = saved; +} + +static void set_nonblock_cloexec(int fd) { + int fl = fcntl(fd, F_GETFL, 0); + if (fl >= 0) + fcntl(fd, F_SETFL, fl | O_NONBLOCK); + int fdfl = fcntl(fd, F_GETFD, 0); + if (fdfl >= 0) + fcntl(fd, F_SETFD, fdfl | FD_CLOEXEC); +} + static double wall_seconds() { struct timeval tv; gettimeofday(&tv, NULL); @@ -2293,8 +2320,34 @@ static int solve_in_child_fork( timed_out = false; double deadline = (cpu_lim != INT32_MAX) ? wall_seconds() + (double)cpu_lim : -1.0; + /* GH-224: wait in poll() on the bounds pipe and on a SIGCHLD self-pipe instead of usleep(10000). The handler is + * installed only in the parent and after fork(), so the solver child is unaffected; a child that exits before + * the handler is in place is caught by the waitpid(WNOHANG) that precedes every poll(). The poll timeout is the + * remaining -cpu-lim time, capped at 100 ms as a safety net (1 ms if the self-pipe cannot be created). */ + int wake[2] = {-1, -1}; + struct sigaction sa_old; + bool have_wake = (pipe(wake) == 0); + if (have_wake) { + set_nonblock_cloexec(wake[0]); + set_nonblock_cloexec(wake[1]); + g_sigchld_wake_w = wake[1]; + struct sigaction sa; + memset(&sa, 0, sizeof(sa)); + sa.sa_handler = sigchld_wake; + sigemptyset(&sa.sa_mask); + sa.sa_flags = SA_RESTART | SA_NOCLDSTOP; + if (sigaction(SIGCHLD, &sa, &sa_old) != 0) { + g_sigchld_wake_w = -1; + close(wake[0]); + close(wake[1]); + have_wake = false; + } + } + bool pipe_eof = false; + for (;;) { - drain_bounds_pipe(pipefd[0], book, carry, &prog); + if (!pipe_eof) + pipe_eof = drain_bounds_pipe(pipefd[0], book, carry, &prog); int status = 0; pid_t w = waitpid(pid, &status, WNOHANG); @@ -2316,9 +2369,41 @@ static int solve_in_child_fork( apply_pipe_line(book, carry.c_str(), &prog); break; } - usleep(10000); + + int timeout_ms = have_wake ? 100 : 1; + if (deadline >= 0.0) { + double left_ms = (deadline - wall_seconds()) * 1000.0; + if (left_ms + 1.0 < (double)timeout_ms) + timeout_ms = left_ms > 0.0 ? (int)left_ms + 1 : 0; + } + struct pollfd pfd[2]; + int nfd = 0; + if (!pipe_eof) { + pfd[nfd].fd = pipefd[0]; + pfd[nfd].events = POLLIN; + pfd[nfd].revents = 0; + nfd++; + } + if (have_wake) { + pfd[nfd].fd = wake[0]; + pfd[nfd].events = POLLIN; + pfd[nfd].revents = 0; + nfd++; + } + (void)poll(pfd, (nfds_t)nfd, timeout_ms); /* EINTR (SIGCHLD) is fine: the loop re-checks everything */ + if (have_wake) { + char sink[64]; + while (read(wake[0], sink, sizeof(sink)) > 0) { + } + } } + if (have_wake) { + sigaction(SIGCHLD, &sa_old, NULL); + g_sigchld_wake_w = -1; + close(wake[0]); + close(wake[1]); + } close(pipefd[0]); out = book; return out.distance;