Skip to content

Commit 19fefcd

Browse files
committed
🦓
1 parent fde3988 commit 19fefcd

1 file changed

Lines changed: 15 additions & 17 deletions

File tree

‎docs/sat-ideas.md‎

Lines changed: 15 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -571,29 +571,27 @@ condition, and result.
571571

572572
This is the latest recorded snapshot, measured on 2026-09-15 with a release
573573
build, single runs, and a 60-second per-cell timeout (120 seconds for the
574-
listed combinations). The `--nogood` column uses the current `1 << 11`-entry
575-
database with the 96-literal bound; for enumeration, the value is the time to
576-
the 10th solution with `--no-stop`. Replace this table on a future rerun
577-
instead of appending another historical table.
574+
listed combinations). The `--activity` column was measured on 2026-09-16 on
575+
the same machine and with the same protocol. The `--nogood` column uses the
576+
current `1 << 11`-entry database with the 96-literal bound; for enumeration,
577+
the value is the time to the 10th solution with `--no-stop`. Replace this
578+
table on a future rerun instead of appending another historical table.
578579

579580
| Case | Plain | `--phase-saving` | `--lookahead` | `--backjump` | `--nogood` | `--activity` |
580581
| --- | ---: | ---: | ---: | ---: | ---: | ---: |
581-
| `B3/S23 26 8 4 -y 1 -n a` | 1.227 s | 3.752 s | 5.665 s | 36.538 s | 2.690 s | TBD |
582-
| `B3/S23 64 64 1 -n a` | >60 s | 1.854 s | 0.049 s | 0.026 s | 0.014 s | TBD |
583-
| `3457/357/5 20 16 7 -x 3 -s D2- -n a` | 2.269 s | 3.208 s | N/A | N/A | N/A | TBD |
584-
| `R3,C2,S2,B3,N+ 50 10 4 -x 2 -s D2- -n a` | >60 s | 13.622 s | 30.922 s | >60 s | >60 s | TBD |
585-
| `B2n3/S23-q 30 9 4 -x 1 -n a` | 4.154 s | 3.498 s | N/A | >60 s | 14.728 s | TBD |
586-
| `B3/S23 20 20 2 -n r --seed 1 --no-stop` to 10th solution | 5.716 s | N/A | N/A | N/A | 0.114 s | TBD |
587-
588-
The `--activity` column is pending measurement; the current runs were made on a
589-
different machine than the one used for the other columns, so they are not
590-
comparable and are not recorded here.
582+
| `B3/S23 26 8 4 -y 1 -n a` | 1.227 s | 3.752 s | 5.665 s | 36.538 s | 2.690 s | 1.520 s |
583+
| `B3/S23 64 64 1 -n a` | >60 s | 1.854 s | 0.049 s | 0.026 s | 0.014 s | 0.026 s |
584+
| `3457/357/5 20 16 7 -x 3 -s D2- -n a` | 2.269 s | 3.208 s | N/A | N/A | N/A | 2.523 s |
585+
| `R3,C2,S2,B3,N+ 50 10 4 -x 2 -s D2- -n a` | >60 s | 13.622 s | 30.922 s | >60 s | >60 s | ~60 s |
586+
| `B2n3/S23-q 30 9 4 -x 1 -n a` | 4.154 s | 3.498 s | N/A | >60 s | 14.728 s | 2.685 s |
587+
| `B3/S23 20 20 2 -n r --seed 1 --no-stop` to 10th solution | 5.716 s | N/A | N/A | N/A | 0.114 s | 2.114 s |
591588

592589
On the deep `26 8 4` case the combined options `--nogood --phase-saving` and
593590
`--nogood --lookahead` take 9.189 s and 8.180 s, while `--backjump
594-
--phase-saving` still exceeds 120 seconds. The enumeration guard makes
595-
solution counts match the plain search; `B3/S23 5 5 2` reports 26 solutions
596-
with backjumping and nogood.
591+
--phase-saving` still exceeds 120 seconds. The factorio `--activity` run
592+
finishes just under the timeout (about 59.7 s) and is recorded as `~60 s`. The
593+
enumeration guard makes solution counts match the plain search; `B3/S23 5 5 2`
594+
reports 26 solutions with backjumping and nogood.
597595

598596
## Comparison with Logic Life Search (LLS)
599597

0 commit comments

Comments
 (0)