From 00619283cc20502def048f68a8ed7c0fa96b9841 Mon Sep 17 00:00:00 2001 From: Matarener Date: Fri, 23 Oct 2026 21:14:04 +0300 Subject: [PATCH 1/2] line-system-510-signing-nonexistence: the 510-vertex signing of line-system-saturation 11.1 does not exist Hand proof (descent to 120 lines in R^24, frame form, two classes sharing one block are incompatible) with exhaustive finite checks in verify.py, a positive k'=1 control, Delsarte inequalities, and CP-SAT provenance (two-class sub-test INFEASIBLE). Also rules out the 1023-line cos 1/4 candidate in R^31. Negative result, no kappa claim. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../README.md | 99 ++++ .../SOURCES.json | 24 + .../TASK.json | 72 +++ .../VERIFY.json | 20 + .../logs/progress.txt | 184 +++++++ .../logs/sat_k2_c2_cpsat.txt | 260 ++++++++++ .../logs/sat_k2_cpsat.txt | 263 ++++++++++ .../logs/sat_sb_k1_cpsat.txt | 327 +++++++++++++ .../logs/sat_sb_k2_c1_cpsat.txt | 291 ++++++++++++ .../logs/sat_sb_k2_c2_cpsat.txt | 448 ++++++++++++++++++ .../logs/sat_sb_k2_c2_nocol_cpsat.txt | 297 ++++++++++++ .../logs/sat_sb_k2_c2_nosb_cpsat.txt | 150 ++++++ .../tools/delsarte_lp.py | 149 ++++++ .../tools/frame_reduction.py | 188 ++++++++ .../tools/sat_k2.py | 143 ++++++ .../tools/sat_sb.py | 198 ++++++++ .../verify.py | 180 +++++++ 17 files changed, 3293 insertions(+) create mode 100644 research/line-system-510-signing-nonexistence/README.md create mode 100644 research/line-system-510-signing-nonexistence/SOURCES.json create mode 100644 research/line-system-510-signing-nonexistence/TASK.json create mode 100644 research/line-system-510-signing-nonexistence/VERIFY.json create mode 100644 research/line-system-510-signing-nonexistence/logs/progress.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_k2_c2_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_k2_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_sb_k1_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c1_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nocol_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nosb_cpsat.txt create mode 100644 research/line-system-510-signing-nonexistence/tools/delsarte_lp.py create mode 100644 research/line-system-510-signing-nonexistence/tools/frame_reduction.py create mode 100644 research/line-system-510-signing-nonexistence/tools/sat_k2.py create mode 100644 research/line-system-510-signing-nonexistence/tools/sat_sb.py create mode 100644 research/line-system-510-signing-nonexistence/verify.py diff --git a/research/line-system-510-signing-nonexistence/README.md b/research/line-system-510-signing-nonexistence/README.md new file mode 100644 index 0000000000..d2bf443ba4 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/README.md @@ -0,0 +1,99 @@ +# The 510-vertex signing of `line-system-saturation` §11.1 does not exist (negative result, no κ claim) + +**Answer to an open question.** `research/line-system-saturation` (#2244) §11.1 asks whether the doubled +non-collinearity graph of W(7,2) has a ±1 signing S with S² = 60S + 256I, equivalently 510 unit vectors in ℝ³⁰ +with |cos| ∈ {0, 1/4} realising the saturated uniform-angle pattern (k′ = 4, m = 2, λ = 4 of its Theorem G). +**It does not.** The proof is short and by hand. Its finite steps are checked exhaustively by `verify.py` +(standard library only), and an independent CP-SAT run agrees. + +Consequences, all paper-side and scoped exactly as in #2244: +- no saturated uniform-angle (cos 1/4) system on the descent ladder 120 lines in ℝ²⁴ (k′ = 2, m = 8), + 252 in ℝ²⁸ (k′ = 3, m = 4), 510 in ℝ³⁰ (k′ = 4, m = 2); +- the 1023-line candidate in ℝ³¹ (k′ = 5, m = 1, cos 1/4), which #2244 §11.1 notes descends to exactly this + object, does not exist either; so uniform-angle saturation with m = 1 at k′ = 5 is ruled out. + +Not touched: saturated W(7,2) systems with several angles (§11.3), level-2 bounds (§11.2), non-dense pairings +(§11.4). This changes no κ, supplier or selected record. + +## Proof + +Statuses follow #2244. **PROVEN** below, with finite steps **CHECKED** by `verify.py`. + +**Step 1 (descent).** Proposition D1 of #2244 §5.2 at a label p with m_p = 2 keeps the lines with labels in +p^⊥ ∖ {p} and merges q, q + p. The lines are unchanged, so angles stay in {0, 1/4}, and non-collinear quotient +labels have all four representatives pairwise non-collinear (b(q, r + p) = b(q, r)). The result is a saturated +uniform W(5,2) system with m = 4 in ℝ²⁸; once more gives O₂: W(3,2), m = 8, 120 lines in ℝ²⁴. It suffices to +rule out O₂. + +**Step 2 (frame form).** Coordinates (x₁, y₁, x₂, y₂) on F₂⁴, b = x₁y₁′ + y₁x₁′ + x₂y₂′ + y₂x₂′. Take the +generator L = ⟨a, b⟩, a = x₁, b = x₂, c = a + b. Its 24 lines are pairwise orthogonal, so they form an orthonormal +frame. Let blocks A, B, C be the 8 frame lines of a, b, c. Any other unit line u has u·e ∈ {0, ±1/4} on frame +lines, and norm 1 forces exactly 16 non-zero entries ±1/4. The support is fixed by the labels: b(a, p) = y₁, +b(b, p) = y₂. The class K₁ = {y = (1,1)} lives on A ∪ B and K₂ = {y = (1,0)} on A ∪ C, so the two classes meet +only on block A. For p ∈ K₁, q ∈ K₂: b(p, q) = x₁(p) + x₁(q) + x₂(q). Put P_i = {p ∈ K₁ : x₁ = i} and +Q_i = {q ∈ K₂ : x₁ + x₂ = i}. On the A-parts (vectors in {±1}⁸, scaled by 4), P₀ ⟂ Q₀ and P₁ ⟂ Q₁, while +P₀–Q₁ and P₁–Q₀ products are ±4. Each collinearity group of K₁ is a Hadamard matrix of order 16 containing +one point of P₀ and one of P₁. The two points of P₀ are non-collinear. + +**Step 3 (A-parts).** Let U_i, V_i be the A-parts of P_i, Q_i, with N_i = Σ_{U_i} uuᵀ. Hadamard columns are +orthogonal, so N₀ + N₁ = 32I = M₀ + M₁. From U₀ ⟂ V₀, U₁ ⟂ V₁ and the full rank of the sums, all four +dimensions are 4, S₀ := span U₀ = (span U₁)^⊥ and V₁ ⊆ S₀. +(a) A 4-space holds at most 16 vectors of {±1}⁸. U₀ and V₁ both span S₀ and share no line (products ±4, not +±8). So S₀ holds exactly 8 lines and is the graph of a signed permutation, with (s, Ms)·(t, Mt) = 2 s·t. +(b) Cross products ±4 force odd Hamming distance, so U₀ is one parity class: 4 pairwise orthogonal directions. +(c) A point's group partner has A-parts in S₀^⊥, so each point of P₀ uses each direction exactly twice. + +**Step 4 (contradiction).** The two lines of p ∈ P₀ on a direction e are twins, so they are (e, w) and (e, −w) +up to sign. Take a line (±e, w′) of the other point p′ ∈ P₀; it exists by (c). Non-collinearity needs +|±8 + w·w′| = |±8 − w·w′| = 4, so w·w′ = 0 and both values equal 8. Contradiction. ∎ + +The proof uses only two classes sharing one block. This is why the two-class CP-SAT sub-test below is already +infeasible. + +## Evidence + +`verify.py` (registered, about 1 s, standard library only) checks: +- that #2244 states the question as open; +- the Step 2 combinatorics exhaustively on W(3,2); +- lemmas (a) and (b) by enumeration, and the Step 4 arithmetic; +- a positive control: the k′ = 1 rung exists, 48 lines in ℝ¹⁶ (frame + Sylvester H₁₆ + bent-shifted H₁₆) built + and checked exactly, plus two failure controls; +- the Delsarte inequalities. For each rung the forced distance distribution passes every Gegenbauer + inequality up to degree 40 (degree 2 is 0, a tight frame), so two-point LP bounds cannot decide this question, + in line with #2244 §6. The plain LP bound for ℝ³⁰ with angles {90°, arccos 1/4} is 900 (floating-point LP, not + certified here; `tools/delsarte_lp.py`). + +`tools/` and `logs/` (renamed `.txt`, since `*.log` is ignored) are provenance, not registered replay. They need `ortools==9.15.6755` and write a +`progress.log` beside themselves, so run them from a copy: + +| run | instance | result | +|---|---|---| +| `sat_k2.py 1800 6` | full O₂, plain encoding | UNKNOWN after 30 min | +| `sat_k2.py 1800 6 2` | two classes, plain | UNKNOWN after 30 min | +| `sat_sb.py 1 300 6` | k′ = 1 control | FEASIBLE in 4 s, checked exactly | +| `sat_sb.py 2 600 2 1` | one class of O₂ | FEASIBLE in 51 s, checked exactly | +| `sat_sb.py 2 1800 6 2` | two classes, lex-leader symmetry breaking + Hadamard column constraints | **INFEASIBLE in 559 s** | +| `sat_sb.py 2 1800 3 2 nocol` | same without column constraints | **INFEASIBLE in 1319 s** | +| `sat_sb.py 2 1800 3 2 nosb` | same without symmetry breaking | UNKNOWN after 30 min | + +The solver results carry no proof certificate. They corroborate the hand proof but do not replace it. + +## Reproduce + +```sh +python3 -B research/line-system-510-signing-nonexistence/verify.py +``` + +## Open next questions + +Structured versions are in `TASK.json`. +- **Saturated W(7,2) systems with several angles.** These would still reopen k′ = 5 (#2244 §11.3). First step: + apply the frame lemma (a generator class is a frame) with the angle set left free, and check whether the + two-class block argument extends. +- **Non-dense pairings** (#2244 §11.4) are untouched and remain the larger lever. + +## Credit + +The question, the descent proposition, Theorem G and the counts used here are from `line-system-saturation` +(#2244). This package adds the frame reduction, the hand proof and the checks. Prepared for Mark (Matarener) +with substantial Claude (Anthropic) assistance. Apache-2.0. diff --git a/research/line-system-510-signing-nonexistence/SOURCES.json b/research/line-system-510-signing-nonexistence/SOURCES.json new file mode 100644 index 0000000000..17dbb2ec65 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/line-system-saturation/README.md", + "usage": "input", + "git_blob": "8e998ee15db765ce90d52d53d4a61f3fd75e5dae", + "sha256": "a99a58bc58e42348596534ce8f73809255ac89b330589b0f4d9cf2199d669e87" + } + ] +} diff --git a/research/line-system-510-signing-nonexistence/TASK.json b/research/line-system-510-signing-nonexistence/TASK.json new file mode 100644 index 0000000000..b50512ec8f --- /dev/null +++ b/research/line-system-510-signing-nonexistence/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Decide the OPEN 510-vertex signing of line-system-saturation section 11.1 (saturated uniform-angle W(7,2) line system, m=2, cos 1/4), a candidate new local unit at windows h=10..11.", + "scope_change_reason": "The card asks for a new local cost interface; this package settles whether one specific candidate unit (the saturated W4/W5 line systems of #2244) can exist at all. Negative result, no interface or kappa claim.", + "bottleneck_link": "Side result: #2244 shows a saturated W4 line system would reopen k'=5 local units (h=10..11) below the break-even fit; this removes the uniform-angle candidates (510 in R^30, 1023 in R^31).", + "budget_minutes": 240, + "stop_rule": "Stop at a decision for the 120-line descendant (proof or exact witness); no search beyond 30-minute CP-SAT runs.", + "outcome": "negative-result", + "evidence": "Hand proof in README.md; finite steps checked exhaustively by verify.py; CP-SAT two-class sub-test INFEASIBLE (559 s, and 1319 s without column constraints), logs in logs/.", + "author": "Mark (Matarener)", + "ai_assistance": "Substantial Claude (Anthropic) assistance: proof drafting, encodings, scripts and README.", + "open_questions": [ + { + "question": "Do saturated W(7,2) systems with several non-orthogonal angles exist?", + "why_it_matters": "#2244 section 11.3: any saturated W4 system reopens k'=5 local units at h=10..11.", + "first_step": "Apply the frame lemma (a generator class is an orthonormal frame) with free angles and test whether the two-class block argument of this package extends.", + "blocked_by": "Non-uniform angles break the {+-1} entry structure used in Step 3." + }, + { + "question": "Can non-dense pairings (rank below the dense window) beat the break-even fit at h <= 13?", + "why_it_matters": "#2244 section 11.4: the remaining paper-side lever after uniform saturation is closed.", + "first_step": "Bound the clique number of the non-orthogonality graph against the needed rank for E8-type units.", + "blocked_by": "No cost model for non-dense pairings in the current packages." + } + ] +} diff --git a/research/line-system-510-signing-nonexistence/VERIFY.json b/research/line-system-510-signing-nonexistence/VERIFY.json new file mode 100644 index 0000000000..05fc5b5103 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/line-system-saturation/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Section 11.1 input binding; exhaustive W(3,2) frame-form combinatorics; lemmas (a),(b) by enumeration; Step 4 arithmetic; positive control (48 lines in R^16 built exactly) with two failure controls; Delsarte inequalities for all rungs." + } + ] +} diff --git a/research/line-system-510-signing-nonexistence/logs/progress.txt b/research/line-system-510-signing-nonexistence/logs/progress.txt new file mode 100644 index 0000000000..680d26f7ce --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/progress.txt @@ -0,0 +1,184 @@ +[2026-10-23 19:10:15] === delsarte_lp.py start: n=30, |cos| in {0, 1/4}, even degrees 2..60 === +[2026-10-23 19:10:15] Part A (fixed distribution 1 + 253 + 256 = 510): +[2026-10-23 19:10:15] k= 2 1+253Q_k(0)+256Q_k(1/4) = 0 (~0) +[2026-10-23 19:10:15] k= 4 1+253Q_k(0)+256Q_k(1/4) = 442/899 (~0.491657) +[2026-10-23 19:10:15] k= 6 1+253Q_k(0)+256Q_k(1/4) = 357/341 (~1.04692) +[2026-10-23 19:10:15] k= 8 1+253Q_k(0)+256Q_k(1/4) = 20007/19778 (~1.01158) +[2026-10-23 19:10:15] k=10 1+253Q_k(0)+256Q_k(1/4) = 5801759/5854288 (~0.991027) +[2026-10-23 19:10:15] k=12 1+253Q_k(0)+256Q_k(1/4) = 6945847/6918704 (~1.00392) +[2026-10-23 19:10:15] k=14 1+253Q_k(0)+256Q_k(1/4) = 8503057/8515328 (~0.998559) +[2026-10-23 19:10:15] k=16 1+253Q_k(0)+256Q_k(1/4) = 30039175231/30025046528 (~1.00047) +[2026-10-23 19:10:15] worst over k<= 60: k=2 value 0 -> ALL >= 0: LP does not kill the object +[2026-10-23 19:10:15] Part B (plain LP): N <= 900 = 900.0000 (float LP 900.0000); vertex A0=435, A1/4=464 +[2026-10-23 19:10:15] Part C (with tight-frame equality): N <= 900 = 900.0000 (float LP 900.0000); vertex A0=435, A1/4=464 +[2026-10-23 19:10:15] absolute bound (3 inner products 0, +-a on lines): C(n+2,3)=4960 +[2026-10-23 19:10:15] === delsarte_lp.py done; results in delsarte_lp_result.json === +[2026-10-23 19:13:50] === frame_reduction.py start (exact combinatorics, no solver) === +[2026-10-23 19:13:50] k'=1: m=16, N=48 lines in R^16; non-frame lines 32; support sizes [16]; classes 1 x 2 points (ok=True, same support inside class=True, Hadamard-16 groups=True); cross-class support intersections []; per line: 15 orthogonal + 32 at 1/4 +[2026-10-23 19:13:50] E1 (direct signing): 768 edge-sign bits, 1128 pair constraints, ~2.38e+04 product terms +[2026-10-23 19:13:50] E2 (frame-reduced): 512 sign bits, 496 in-class + 0 cross-class pair constraints, 7936 XOR auxiliaries +[2026-10-23 19:13:50] k'=2: m=8, N=120 lines in R^24; non-frame lines 96; support sizes [16]; classes 3 x 4 points (ok=True, same support inside class=True, Hadamard-16 groups=True); cross-class support intersections [8]; per line: 55 orthogonal + 64 at 1/4 +[2026-10-23 19:13:50] E1 (direct signing): 3840 edge-sign bits, 7140 pair constraints, ~3.34e+05 product terms +[2026-10-23 19:13:50] E2 (frame-reduced): 1536 sign bits, 1488 in-class + 3072 cross-class pair constraints, 48384 XOR auxiliaries +[2026-10-23 19:13:50] k'=3: m=4, N=252 lines in R^28; non-frame lines 224; support sizes [16]; classes 7 x 8 points (ok=True, same support inside class=True, Hadamard-16 groups=True); cross-class support intersections [8]; per line: 123 orthogonal + 128 at 1/4 +[2026-10-23 19:13:50] E1 (direct signing): 16128 edge-sign bits, 31626 pair constraints, ~3.02e+06 product terms +[2026-10-23 19:13:50] E2 (frame-reduced): 3584 sign bits, 3472 in-class + 21504 cross-class pair constraints, 227584 XOR auxiliaries +[2026-10-23 19:13:50] k'=4: m=2, N=510 lines in R^30; non-frame lines 480; support sizes [16]; classes 15 x 16 points (ok=True, same support inside class=True, Hadamard-16 groups=True); cross-class support intersections [8]; per line: 253 orthogonal + 256 at 1/4 +[2026-10-23 19:13:50] E1 (direct signing): 65280 edge-sign bits, 129795 pair constraints, ~2.49e+07 product terms +[2026-10-23 19:13:50] E2 (frame-reduced): 7680 sign bits, 7440 in-class + 107520 cross-class pair constraints, 979200 XOR auxiliaries +[2026-10-23 19:13:50] wrote e2_k2.opb: 52224 variables, 198215 constraints, 119 gauge-fixed (NOT solved) +[2026-10-23 19:13:50] === frame_reduction.py done === +[2026-10-23 19:13:58] descendant n=16: fixed distribution 1+15+32=48: worst k=2 value 0; k=4 value 15/17; plain LP (tight frame) N<=144 +[2026-10-23 19:13:58] descendant n=24: fixed distribution 1+55+64=120: worst k=2 value 0; k=4 value 98/115; plain LP (tight frame) N<=4680/11 +[2026-10-23 19:13:58] descendant n=28: fixed distribution 1+123+128=252: worst k=2 value 0; k=4 value 64/87; plain LP (tight frame) N<=700 +[2026-10-23 19:14:57] REPORT.md written (first report). Waiting for Mark's command; no solver launched. +[2026-10-23 19:17:11] === sat_k2.py start: k'=2, 96 non-frame lines in R^24, 1536 sign bits, 4560 pair constraints, 119 gauge-fixed; CP-SAT 6 workers, limit 1800 s === +[2026-10-23 19:18:11] sat_k2 running, 60 s elapsed (limit 1800 s) +[2026-10-23 19:19:11] sat_k2 running, 120 s elapsed (limit 1800 s) +[2026-10-23 19:20:11] sat_k2 running, 180 s elapsed (limit 1800 s) +[2026-10-23 19:21:11] sat_k2 running, 240 s elapsed (limit 1800 s) +[2026-10-23 19:22:11] sat_k2 running, 300 s elapsed (limit 1800 s) +[2026-10-23 19:23:11] sat_k2 running, 360 s elapsed (limit 1800 s) +[2026-10-23 19:24:11] sat_k2 running, 420 s elapsed (limit 1800 s) +[2026-10-23 19:25:11] sat_k2 running, 480 s elapsed (limit 1800 s) +[2026-10-23 19:26:11] sat_k2 running, 540 s elapsed (limit 1800 s) +[2026-10-23 19:27:11] sat_k2 running, 600 s elapsed (limit 1800 s) +[2026-10-23 19:28:11] sat_k2 running, 660 s elapsed (limit 1800 s) +[2026-10-23 19:29:11] sat_k2 running, 720 s elapsed (limit 1800 s) +[2026-10-23 19:30:11] sat_k2 running, 780 s elapsed (limit 1800 s) +[2026-10-23 19:31:11] sat_k2 running, 840 s elapsed (limit 1800 s) +[2026-10-23 19:32:11] sat_k2 running, 900 s elapsed (limit 1800 s) +[2026-10-23 19:33:11] sat_k2 running, 960 s elapsed (limit 1800 s) +[2026-10-23 19:34:11] sat_k2 running, 1020 s elapsed (limit 1800 s) +[2026-10-23 19:35:11] sat_k2 running, 1080 s elapsed (limit 1800 s) +[2026-10-23 19:36:11] sat_k2 running, 1140 s elapsed (limit 1800 s) +[2026-10-23 19:37:11] sat_k2 running, 1201 s elapsed (limit 1800 s) +[2026-10-23 19:38:11] sat_k2 running, 1261 s elapsed (limit 1800 s) +[2026-10-23 19:39:11] sat_k2 running, 1321 s elapsed (limit 1800 s) +[2026-10-23 19:40:11] sat_k2 running, 1381 s elapsed (limit 1800 s) +[2026-10-23 19:41:11] sat_k2 running, 1441 s elapsed (limit 1800 s) +[2026-10-23 19:42:11] sat_k2 running, 1501 s elapsed (limit 1800 s) +[2026-10-23 19:43:11] sat_k2 running, 1561 s elapsed (limit 1800 s) +[2026-10-23 19:44:11] sat_k2 running, 1621 s elapsed (limit 1800 s) +[2026-10-23 19:45:11] sat_k2 running, 1681 s elapsed (limit 1800 s) +[2026-10-23 19:46:11] sat_k2 running, 1741 s elapsed (limit 1800 s) +[2026-10-23 19:47:11] sat_k2 running, 1801 s elapsed (limit 1800 s) +[2026-10-23 19:47:13] CP-SAT status UNKNOWN after 1801.9 s +[2026-10-23 19:47:13] RESULT: UNKNOWN (time limit reached, no decision) +[2026-10-23 19:47:13] === sat_k2.py done === +[2026-10-23 19:48:15] sub-test: only 2 of 3 classes, 8 points kept +[2026-10-23 19:48:16] === sat_k2.py start: k'=2, 64 non-frame lines in R^24, 1024 sign bits, 2016 pair constraints, 87 gauge-fixed; CP-SAT 6 workers, limit 1800 s === +[2026-10-23 19:49:16] sat_k2 running, 60 s elapsed (limit 1800 s) +[2026-10-23 19:50:16] sat_k2 running, 120 s elapsed (limit 1800 s) +[2026-10-23 19:51:16] sat_k2 running, 180 s elapsed (limit 1800 s) +[2026-10-23 19:52:16] sat_k2 running, 240 s elapsed (limit 1800 s) +[2026-10-23 19:53:16] sat_k2 running, 300 s elapsed (limit 1800 s) +[2026-10-23 19:54:16] sat_k2 running, 360 s elapsed (limit 1800 s) +[2026-10-23 19:55:16] sat_k2 running, 420 s elapsed (limit 1800 s) +[2026-10-23 19:56:16] sat_k2 running, 480 s elapsed (limit 1800 s) +[2026-10-23 19:57:16] sat_k2 running, 540 s elapsed (limit 1800 s) +[2026-10-23 19:58:16] sat_k2 running, 600 s elapsed (limit 1800 s) +[2026-10-23 19:59:16] sat_k2 running, 660 s elapsed (limit 1800 s) +[2026-10-23 20:00:16] sat_k2 running, 720 s elapsed (limit 1800 s) +[2026-10-23 20:01:16] sat_k2 running, 780 s elapsed (limit 1800 s) +[2026-10-23 20:02:16] sat_k2 running, 840 s elapsed (limit 1800 s) +[2026-10-23 20:03:16] sat_k2 running, 900 s elapsed (limit 1800 s) +[2026-10-23 20:04:16] sat_k2 running, 960 s elapsed (limit 1800 s) +[2026-10-23 20:05:16] sat_k2 running, 1020 s elapsed (limit 1800 s) +[2026-10-23 20:06:16] sat_k2 running, 1080 s elapsed (limit 1800 s) +[2026-10-23 20:07:16] sat_k2 running, 1141 s elapsed (limit 1800 s) +[2026-10-23 20:08:16] sat_k2 running, 1201 s elapsed (limit 1800 s) +[2026-10-23 20:09:16] sat_k2 running, 1261 s elapsed (limit 1800 s) +[2026-10-23 20:10:16] sat_k2 running, 1321 s elapsed (limit 1800 s) +[2026-10-23 20:11:16] sat_k2 running, 1381 s elapsed (limit 1800 s) +[2026-10-23 20:12:16] sat_k2 running, 1441 s elapsed (limit 1800 s) +[2026-10-23 20:13:16] sat_k2 running, 1501 s elapsed (limit 1800 s) +[2026-10-23 20:14:16] sat_k2 running, 1561 s elapsed (limit 1800 s) +[2026-10-23 20:15:16] sat_k2 running, 1621 s elapsed (limit 1800 s) +[2026-10-23 20:16:16] sat_k2 running, 1681 s elapsed (limit 1800 s) +[2026-10-23 20:17:16] sat_k2 running, 1741 s elapsed (limit 1800 s) +[2026-10-23 20:18:16] sat_k2 running, 1801 s elapsed (limit 1800 s) +[2026-10-23 20:18:17] CP-SAT status UNKNOWN after 1801.0 s +[2026-10-23 20:18:17] RESULT: UNKNOWN (time limit reached, no decision) +[2026-10-23 20:18:17] === sat_k2.py done === +[2026-10-23 20:22:43] === sat_sb.py start: k'=1, 32 non-frame lines in R^16, 512 sign bits, 496 pair + 240 column constraints, 93 symmetry-breaking constraints; CP-SAT 6 workers, limit 300 s === +[2026-10-23 20:22:47] CP-SAT status OPTIMAL after 3.8 s +[2026-10-23 20:22:47] exact check of 48 lines (4u, integer): norms ok=True, bad pairs=0 +[2026-10-23 20:22:47] RESULT: FEASIBLE (full object exists) +[2026-10-23 20:22:47] === sat_sb.py done === +[2026-10-23 20:22:58] === sat_sb.py start: k'=2 sub-test 2 classes, 64 non-frame lines in R^24, 1024 sign bits, 2016 pair + 480 column constraints, 165 symmetry-breaking constraints; CP-SAT 6 workers, limit 1800 s === +[2026-10-23 20:23:59] sat_sb_k2_c2 running, 60 s elapsed (limit 1800 s) +[2026-10-23 20:24:59] sat_sb_k2_c2 running, 120 s elapsed (limit 1800 s) +[2026-10-23 20:25:59] sat_sb_k2_c2 running, 180 s elapsed (limit 1800 s) +[2026-10-23 20:26:59] sat_sb_k2_c2 running, 240 s elapsed (limit 1800 s) +[2026-10-23 20:27:59] sat_sb_k2_c2 running, 300 s elapsed (limit 1800 s) +[2026-10-23 20:28:59] sat_sb_k2_c2 running, 360 s elapsed (limit 1800 s) +[2026-10-23 20:29:59] sat_sb_k2_c2 running, 420 s elapsed (limit 1800 s) +[2026-10-23 20:30:59] sat_sb_k2_c2 running, 480 s elapsed (limit 1800 s) +[2026-10-23 20:31:59] sat_sb_k2_c2 running, 540 s elapsed (limit 1800 s) +[2026-10-23 20:32:17] CP-SAT status INFEASIBLE after 559.1 s +[2026-10-23 20:32:17] RESULT: INFEASIBLE -> 510-line object does not exist +[2026-10-23 20:32:17] === sat_sb.py done === +[2026-10-23 20:32:54] === sat_sb.py start: k'=2 sub-test 1 classes, 32 non-frame lines in R^24, 512 sign bits, 496 pair + 240 column constraints, 90 symmetry-breaking constraints, flags []; CP-SAT 2 workers, limit 600 s === +[2026-10-23 20:33:45] CP-SAT status OPTIMAL after 50.9 s +[2026-10-23 20:33:45] exact check of 56 lines (4u, integer): norms ok=True, bad pairs=0 +[2026-10-23 20:33:45] RESULT: FEASIBLE (sub-test only) +[2026-10-23 20:33:45] === sat_sb.py done === +[2026-10-23 20:33:55] === sat_sb.py start: k'=2 sub-test 2 classes, 64 non-frame lines in R^24, 1024 sign bits, 2016 pair + 480 column constraints, 0 symmetry-breaking constraints, flags ['nosb']; CP-SAT 3 workers, limit 1800 s === +[2026-10-23 20:33:55] === sat_sb.py start: k'=2 sub-test 2 classes, 64 non-frame lines in R^24, 1024 sign bits, 2016 pair + 0 column constraints, 165 symmetry-breaking constraints, flags ['nocol']; CP-SAT 3 workers, limit 1800 s === +[2026-10-23 20:34:55] sat_sb_k2_c2_nosb running, 60 s elapsed (limit 1800 s) +[2026-10-23 20:34:55] sat_sb_k2_c2_nocol running, 60 s elapsed (limit 1800 s) +[2026-10-23 20:35:55] sat_sb_k2_c2_nosb running, 120 s elapsed (limit 1800 s) +[2026-10-23 20:35:55] sat_sb_k2_c2_nocol running, 120 s elapsed (limit 1800 s) +[2026-10-23 20:36:55] sat_sb_k2_c2_nosb running, 180 s elapsed (limit 1800 s) +[2026-10-23 20:36:55] sat_sb_k2_c2_nocol running, 180 s elapsed (limit 1800 s) +[2026-10-23 20:37:55] sat_sb_k2_c2_nosb running, 240 s elapsed (limit 1800 s) +[2026-10-23 20:37:55] sat_sb_k2_c2_nocol running, 240 s elapsed (limit 1800 s) +[2026-10-23 20:38:55] sat_sb_k2_c2_nosb running, 300 s elapsed (limit 1800 s) +[2026-10-23 20:38:55] sat_sb_k2_c2_nocol running, 300 s elapsed (limit 1800 s) +[2026-10-23 20:39:55] sat_sb_k2_c2_nosb running, 360 s elapsed (limit 1800 s) +[2026-10-23 20:39:55] sat_sb_k2_c2_nocol running, 360 s elapsed (limit 1800 s) +[2026-10-23 20:40:55] sat_sb_k2_c2_nosb running, 420 s elapsed (limit 1800 s) +[2026-10-23 20:40:55] sat_sb_k2_c2_nocol running, 420 s elapsed (limit 1800 s) +[2026-10-23 20:41:55] sat_sb_k2_c2_nosb running, 480 s elapsed (limit 1800 s) +[2026-10-23 20:41:55] sat_sb_k2_c2_nocol running, 480 s elapsed (limit 1800 s) +[2026-10-23 20:42:55] sat_sb_k2_c2_nosb running, 540 s elapsed (limit 1800 s) +[2026-10-23 20:42:55] sat_sb_k2_c2_nocol running, 540 s elapsed (limit 1800 s) +[2026-10-23 20:43:55] sat_sb_k2_c2_nosb running, 600 s elapsed (limit 1800 s) +[2026-10-23 20:43:55] sat_sb_k2_c2_nocol running, 600 s elapsed (limit 1800 s) +[2026-10-23 20:44:55] sat_sb_k2_c2_nosb running, 660 s elapsed (limit 1800 s) +[2026-10-23 20:44:55] sat_sb_k2_c2_nocol running, 660 s elapsed (limit 1800 s) +[2026-10-23 20:45:55] sat_sb_k2_c2_nosb running, 720 s elapsed (limit 1800 s) +[2026-10-23 20:45:55] sat_sb_k2_c2_nocol running, 720 s elapsed (limit 1800 s) +[2026-10-23 20:46:55] sat_sb_k2_c2_nosb running, 780 s elapsed (limit 1800 s) +[2026-10-23 20:46:55] sat_sb_k2_c2_nocol running, 780 s elapsed (limit 1800 s) +[2026-10-23 20:47:55] sat_sb_k2_c2_nosb running, 840 s elapsed (limit 1800 s) +[2026-10-23 20:47:55] sat_sb_k2_c2_nocol running, 840 s elapsed (limit 1800 s) +[2026-10-23 20:48:55] sat_sb_k2_c2_nosb running, 900 s elapsed (limit 1800 s) +[2026-10-23 20:48:55] sat_sb_k2_c2_nocol running, 900 s elapsed (limit 1800 s) +[2026-10-23 20:49:55] sat_sb_k2_c2_nosb running, 960 s elapsed (limit 1800 s) +[2026-10-23 20:49:55] sat_sb_k2_c2_nocol running, 960 s elapsed (limit 1800 s) +[2026-10-23 20:50:55] sat_sb_k2_c2_nosb running, 1020 s elapsed (limit 1800 s) +[2026-10-23 20:50:55] sat_sb_k2_c2_nocol running, 1020 s elapsed (limit 1800 s) +[2026-10-23 20:51:55] sat_sb_k2_c2_nosb running, 1080 s elapsed (limit 1800 s) +[2026-10-23 20:51:55] sat_sb_k2_c2_nocol running, 1080 s elapsed (limit 1800 s) +[2026-10-23 20:52:55] sat_sb_k2_c2_nosb running, 1140 s elapsed (limit 1800 s) +[2026-10-23 20:52:55] sat_sb_k2_c2_nocol running, 1140 s elapsed (limit 1800 s) +[2026-10-23 20:53:55] sat_sb_k2_c2_nosb running, 1200 s elapsed (limit 1800 s) +[2026-10-23 20:53:55] sat_sb_k2_c2_nocol running, 1200 s elapsed (limit 1800 s) +[2026-10-23 20:54:55] sat_sb_k2_c2_nosb running, 1260 s elapsed (limit 1800 s) +[2026-10-23 20:54:55] sat_sb_k2_c2_nocol running, 1260 s elapsed (limit 1800 s) +[2026-10-23 20:55:54] CP-SAT status INFEASIBLE after 1319.2 s +[2026-10-23 20:55:54] RESULT: INFEASIBLE -> 510-line object does not exist +[2026-10-23 20:55:54] === sat_sb.py done === +[2026-10-23 20:55:55] sat_sb_k2_c2_nosb running, 1320 s elapsed (limit 1800 s) +[2026-10-23 20:56:55] sat_sb_k2_c2_nosb running, 1380 s elapsed (limit 1800 s) +[2026-10-23 20:57:55] sat_sb_k2_c2_nosb running, 1440 s elapsed (limit 1800 s) +[2026-10-23 20:58:55] sat_sb_k2_c2_nosb running, 1500 s elapsed (limit 1800 s) +[2026-10-23 20:59:55] sat_sb_k2_c2_nosb running, 1560 s elapsed (limit 1800 s) +[2026-10-23 21:00:55] sat_sb_k2_c2_nosb running, 1620 s elapsed (limit 1800 s) +[2026-10-23 21:01:55] sat_sb_k2_c2_nosb running, 1680 s elapsed (limit 1800 s) +[2026-10-23 21:02:55] sat_sb_k2_c2_nosb running, 1740 s elapsed (limit 1800 s) +[2026-10-23 21:03:55] CP-SAT status UNKNOWN after 1800.3 s +[2026-10-23 21:03:55] RESULT: UNKNOWN (time limit reached, no decision) +[2026-10-23 21:03:55] === sat_sb.py done === diff --git a/research/line-system-510-signing-nonexistence/logs/sat_k2_c2_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_k2_c2_cpsat.txt new file mode 100644 index 0000000000..4504125e32 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_k2_c2_cpsat.txt @@ -0,0 +1,260 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 1800 log_search_progress: true num_search_workers: 6 + +Initial satisfaction model '': (model_fingerprint: 0xe6887ec827148743) +#Variables: 26'112 (24'009 primary variables) + - 26'112 Booleans in [0,1] +#kBoolXor: 24'064 +#kLinear1: 87 +#kLinearN: 2'016 (#terms: 25'088) + +Starting presolve at 0.10s + 1.64e-02s 0.00e+00d [DetectDominanceRelations] + 1.65e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 1.62e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 2.52e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 3.34e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 73'296 nodes and 113'407 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 2.43226 dtime: 1.00015 +[Symmetry] #generators: 57, average support size: 2282.18 +[Symmetry] 736 orbits on 23967 variables with sizes: 448,448,448,392,392,392,196,196,196,147,... +[Symmetry] Found orbitope of size 737 x 2 + 4.30e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 7.44e-01s 7.72e-03d [operations_research::sat::CpModelPresolver::Probe] #probed=50'064 + 2.04e-03s 0.00e+00d [MaxClique] + 2.25e-02s 0.00e+00d [DetectDominanceRelations] + 1.82e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 1.35e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.89e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 2.57e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.36e-03s 7.24e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'016 + 1.22e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 1.93e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=2'016 + 9.01e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] + 1.37e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 2.71e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] + 2.19e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 1.40e-02s 2.02e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 2.56e-03s 1.20e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'016 + 8.27e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::MergeClauses] + 1.97e-02s 0.00e+00d [DetectDominanceRelations] + 8.37e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.05e-02s 0.00e+00d [DetectDominanceRelations] + 8.77e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 3.79e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 2.80e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 73'296 nodes and 113'407 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 2.46799 dtime: 1.00015 +[Symmetry] #generators: 57, average support size: 2282.18 +[Symmetry] 736 orbits on 23967 variables with sizes: 448,448,448,392,392,392,196,196,196,147,... +[Symmetry] Found orbitope of size 737 x 2 + 2.18e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 3.41e-01s 7.72e-03d [operations_research::sat::CpModelPresolver::Probe] #probed=50'064 + 4.74e-04s 0.00e+00d [MaxClique] + 1.34e-02s 0.00e+00d [DetectDominanceRelations] + 7.77e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.11e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.17e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 2.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 4.90e-03s 7.24e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'016 + 9.17e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 1.45e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=2'016 + 9.08e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] + 8.11e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 3.12e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] + 2.86e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 1.49e-02s 2.02e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 2.56e-03s 1.20e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'016 + 1.05e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::MergeClauses] + 1.40e-02s 0.00e+00d [DetectDominanceRelations] + 7.32e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 4.01e-04s 0.00e+00d [MergeNoOverlap] + 5.44e-04s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 999 affine relations were detected. + - rule 'TODO bool_xor: remove constraint' was applied 87 times. + - rule 'TODO dual: only one blocking constraint?' was applied 12'288 times. + - rule 'affine: new relation' was applied 999 times. + - rule 'bool_xor: one active literal' was applied 993 times. + - rule 'bool_xor: remove false literal' was applied 2'985 times. + - rule 'bool_xor: two active literals' was applied 999 times. + - rule 'linear1: x in domain' was applied 87 times. + - rule 'linear: fixed or dup variables' was applied 993 times. + - rule 'linear: remapped using affine relations' was applied 125 times. + - rule 'presolve: 1080 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 2 times. + +Presolved satisfaction model '': (model_fingerprint: 0x941d6b80ad661dc9) +#Variables: 24'033 (22'017 primary variables) + - 24'033 Booleans in [0,1] +#kBoolXor: 22'072 +#kLinearN: 2'016 (#terms: 24'095) +[Symmetry] Graph for symmetry has 71'217 nodes and 113'407 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 2.79074 dtime: 1.00002 +[Symmetry] #generators: 57, average support size: 2282.18 +[Symmetry] 736 orbits on 23967 variables with sizes: 448,448,448,392,392,392,196,196,196,147,... +[Symmetry] Found orbitope of size 737 x 2 + +Preloading model. +#Model 10.58s var:24033/24033 constraints:24088/24088 + +Starting search at 10.58s with 6 workers. +4 full problem subsolvers: [default_lp, max_lp_sym, no_lp, quick_restart] +2 first solution subsolvers: [fj, fs_random_no_lp] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 29.84m, 29.84m] 29.84m 0.00ns 29.84m 2 [ 6.77ms, 3.47m] 1.73m 1.73m 3.47m + 'feasibility_pump': 8434 [ 1.53ms, 223.29ms] 11.37ms 5.64ms 1.60m 8420 [156.67us, 156.67us] 156.67us 0.00ns 1.32s + 'fj': 1121 [363.03ms, 1.84s] 752.69ms 222.54ms 14.06m 1121 [ 46.42ms, 108.86ms] 101.99ms 3.25ms 1.91m + 'fs_random_no_lp': 1 [ 29.82m, 29.82m] 29.82m 0.00ns 29.82m 2 [ 6.57ms, 6.89m] 3.44m 3.44m 6.89m + 'max_lp_sym': 1 [ 29.83m, 29.83m] 29.83m 0.00ns 29.83m 2 [ 6.70ms, 2.68m] 1.34m 1.34m 2.68m + 'no_lp': 1 [ 29.83m, 29.83m] 29.83m 0.00ns 29.83m 2 [ 6.57ms, 4.45m] 2.23m 2.23m 4.45m + 'quick_restart': 1 [ 29.83m, 29.83m] 29.83m 0.00ns 29.83m 2 [ 6.77ms, 50.75s] 25.38s 25.37s 50.76s + 'rins/rens': 347 [ 94.11ms, 10.40s] 2.43s 2.29s 14.06m 184 [ 10.63ms, 100.21ms] 94.21ms 20.17ms 17.33s + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 24'033 3'056'694 9'521'953 6'700 1'583'311 4'686'722 121'687'827 96'072'522 + 'fs_random_no_lp': 24'033 3'453'038 8'272'748 350 864'852 4'321'771 154'791'563 112'017'790 + 'max_lp_sym': 24'033 2'209'643 9'375'882 913 2'096'214 4'359'954 99'056'608 149'560'508 + 'no_lp': 24'033 3'774'580 13'961'738 11'370 2'355'392 6'181'068 188'525'306 133'612'869 + 'quick_restart': 24'033 226'410 19'721'404 20'623 4'148'034 4'475'447 69'330'832 87'236'463 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 0 0 24'033 24'033 0 220'747 11'633 + 'fs_random_no_lp': 0 0 24'033 24'033 0 161'416 16'147 + 'max_lp_sym': 0 0 24'033 24'033 0 97'955 11'409 + 'no_lp': 0 0 24'033 24'033 0 198'602 17'501 + 'quick_restart': 0 0 24'033 24'033 0 50'173 11'006 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 1'697'018 16'143'894 0 94'150'508 81'954'463 325'518 + 'fs_random_no_lp': 2'380'557 23'257'390 0 110'308'579 96'604'763 347'499 + 'max_lp_sym': 1'466'118 18'010'662 0 81'450'713 71'094'344 256'570 + 'no_lp': 2'018'373 22'639'120 0 122'717'993 109'227'702 336'754 + 'quick_restart': 35'460 146'247 0 4'681'735 4'037'114 25'623 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 376'717 3'863'301 0 12'654 216'200 407'745 2'094 + 'fs_random_no_lp': 331'021 3'063'301 0 2'270 26'660 168'821 256 + 'max_lp_sym': 736'118 5'222'042 0 8'870 84'653 329'625 421 + 'no_lp': 673'494 6'247'582 0 16'820 208'085 451'071 1'687 + 'quick_restart': 1'888'762 6'135'127 0 13'070 63'963 214'729 151 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 0 0 0 316'735 37'583 3'920 8'783 12'654 0 8'913 0 0 2'469'620 7'207'785 3'056'694 + 'fs_random_no_lp': 0 0 0 332'850 34'005 24 14'649 2'270 0 175 0 0 2'899'498 8'996'723 3'453'038 + 'max_lp_sym': 0 0 0 249'961 15'810 2'758 6'609 8'870 0 3'187 0 0 1'853'755 5'899'897 2'209'643 + 'no_lp': 0 0 0 323'761 34'612 7'007 12'993 16'820 0 4'785 0 0 3'185'105 8'879'106 3'774'580 + 'quick_restart': 0 0 0 25'025 3'636 14 598 13'070 0 879 0 0 158'840 327'707 226'410 + +Lp stats Component Iterations AddedCuts OPTIMAL DUAL_F. DUAL_U. + 'default_lp': 62 2'027'944 3'947 2'949'877 0 0 + 'max_lp_sym': 62 402'495 0 3'929'371 1 0 + 'quick_restart': 62 1'923'329 31'619 3'204'385 0 0 + +Lp dimension Final dimension of first component + 'default_lp': 2 rows, 22 columns, 23 entries + 'max_lp_sym': 2 rows, 22 columns, 23 entries + 'quick_restart': 2 rows, 22 columns, 23 entries + +Lp debug CutPropag CutEqPropag Adjust Overflow Bad BadScaling + 'default_lp': 0 205 0 0 6'321 0 + 'max_lp_sym': 0 0 0 0 0 0 + 'quick_restart': 0 1'310 0 0 56'627 0 + +Lp pool Constraints Updates Simplif Merged Shortened Split Strengthened Cuts/Call + 'default_lp': 4'071 671 0 0 0 0 322 3'947/20'790 + 'max_lp_sym': 72 0 0 0 0 0 0 0/0 + 'quick_restart': 31'743 4'756 0 0 0 0 2'678 31'619/144'104 + +Lp Cut quick_restart default_lp + CG_FF: 4'701 484 + CG_K: 661 73 + CG_KL: 370 19 + CG_R: 8'187 820 + MIR_1_FF: 6'672 1'072 + MIR_1_K: 788 98 + MIR_1_KL: 20 - + MIR_1_R: 4'362 666 + MIR_2_FF: 1'444 184 + MIR_2_K: 21 2 + MIR_2_KL: 21 2 + MIR_2_R: 893 100 + MIR_3_FF: 429 46 + MIR_3_K: 9 - + MIR_3_KL: 6 1 + MIR_3_R: 340 29 + MIR_4_FF: 52 4 + MIR_4_K: 1 1 + MIR_4_KL: 1 1 + MIR_4_R: 80 5 + MIR_5_FF: 4 - + MIR_5_R: 3 - + MIR_6_FF: 1 - + MIR_6_R: 4 - + ZERO_HALF_FF: 643 103 + ZERO_HALF_K: 25 1 + ZERO_HALF_KL: 9 - + ZERO_HALF_R: 1'872 236 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 347/347 52% 9.89e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 49 23 241'259 1'395'808 0 0 659 5'697'218 + 'fj_restart_compound': 89 23 0 506'169 221'460 141'998 0 13'027'833 + 'fj_restart_compound_obj': 97 23 0 558'899 223'625 167'406 0 14'195'937 + 'fj_restart_compound_perturb': 35 14 0 232'768 133'215 49'686 0 5'473'317 + 'fj_restart_compound_perturb_obj': 103 23 0 680'641 226'331 227'006 1 14'961'965 + 'fj_restart_decay': 68 26 287'651 2'564'796 0 0 662 6'930'733 + 'fj_restart_decay_compound': 64 24 0 423'771 225'978 98'712 0 10'055'373 + 'fj_restart_decay_compound_obj': 56 23 0 380'586 220'186 80'082 0 8'943'929 + 'fj_restart_decay_compound_perturb': 80 18 0 464'582 176'086 143'943 0 11'568'459 + 'fj_restart_decay_compound_perturb_obj': 82 27 0 513'865 256'993 128'153 0 12'505'744 + 'fj_restart_decay_obj': 121 20 261'471 4'582'624 0 0 1'217 11'285'331 + 'fj_restart_decay_perturb': 62 23 251'689 2'336'489 0 0 605 6'293'812 + 'fj_restart_decay_perturb_obj': 38 17 180'655 1'419'559 0 0 371 3'965'097 + 'fj_restart_obj': 69 23 250'065 1'984'672 0 0 981 7'755'435 + 'fj_restart_perturb': 73 14 163'355 2'071'937 0 0 1'100 7'845'895 + 'fj_restart_perturb_obj': 35 16 164'601 1'008'638 0 0 480 4'077'284 + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 0 0 0 + 'fj solution hints': 329 0 329 + 'lp solutions': 27'118 151 10'344 + 'pump': 8'433 196 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 16'905 35'351 0 0 + 'fs_random_no_lp': 19'799 8'025 0 0 + 'max_lp_sym': 8'010 41'018 0 0 + 'no_lp': 25'402 26'817 0 0 + 'quick_restart': 9'554 36'844 0 0 + +LRAT_status: NA +CpSolverResponse summary: +status: UNKNOWN +objective: NA +best_bound: NA +integers: 24033 +booleans: 24033 +conflicts: 3453038 +branches: 8272748 +propagations: 154791563 +integer_propagations: 112017790 +restarts: 350 +lp_iterations: 0 +walltime: 1800.94 +usertime: 1800.94 +deterministic_time: 1232.97 +gap_integral: 0 + diff --git a/research/line-system-510-signing-nonexistence/logs/sat_k2_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_k2_cpsat.txt new file mode 100644 index 0000000000..7497b486eb --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_k2_cpsat.txt @@ -0,0 +1,263 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 1800 log_search_progress: true num_search_workers: 6 + +Initial satisfaction model '': (model_fingerprint: 0x5c0dd9276c74e82a) +#Variables: 52'224 (47'545 primary variables) + - 52'224 Booleans in [0,1] +#kBoolXor: 48'384 +#kLinear1: 119 +#kLinearN: 4'560 (#terms: 50'688) + +Starting presolve at 0.27s + 2.65e-02s 0.00e+00d [DetectDominanceRelations] + 2.87e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 3.50e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 6.50e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 4.28e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 145'888 nodes and 224'079 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 3.22688 dtime: 1.00057 +[Symmetry] #generators: 46, average support size: 3159.96 +[Symmetry] 2960 orbits on 35650 variables with sizes: 64,64,64,64,64,64,64,64,64,64,... +[Symmetry] Found orbitope of size 947 x 2 + 4.22e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 7.23e-01s 1.55e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=99'184 + 9.73e-04s 0.00e+00d [MaxClique] + 2.87e-02s 0.00e+00d [DetectDominanceRelations] + 1.99e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 2.04e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 4.11e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 4.14e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.00e-02s 1.46e-04d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=4'560 + 1.73e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 4.01e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=4'560 + 2.00e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] + 1.65e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 6.62e-03s 7.87e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=1'860 + 3.71e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 2.38e-02s 3.76e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 5.26e-03s 2.41e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=4'560 + 1.61e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.63e-02s 0.00e+00d [DetectDominanceRelations] + 1.49e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.66e-02s 0.00e+00d [DetectDominanceRelations] + 1.43e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 6.83e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 4.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 145'888 nodes and 224'079 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 2.47356 dtime: 1.00057 +[Symmetry] #generators: 46, average support size: 3159.96 +[Symmetry] 2960 orbits on 35650 variables with sizes: 64,64,64,64,64,64,64,64,64,64,... +[Symmetry] Found orbitope of size 947 x 2 + 4.44e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 6.89e-01s 1.55e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=99'184 + 2.06e-03s 0.00e+00d [MaxClique] + 2.58e-02s 0.00e+00d [DetectDominanceRelations] + 1.87e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.01e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 4.58e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 4.48e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 8.07e-03s 1.46e-04d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=4'560 + 1.70e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 2.39e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=4'560 + 1.49e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] + 1.49e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 5.64e-03s 7.12e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=1'680 + 3.55e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 2.37e-02s 3.76e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 4.72e-03s 2.41e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=4'560 + 1.83e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.94e-02s 0.00e+00d [DetectDominanceRelations] + 1.49e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.44e-03s 0.00e+00d [MergeNoOverlap] + 3.04e-03s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 2471 affine relations were detected. + - rule 'TODO bool_xor: remove constraint' was applied 119 times. + - rule 'TODO dual: only one blocking constraint?' was applied 27'648 times. + - rule 'affine: new relation' was applied 2'471 times. + - rule 'bool_xor: one active literal' was applied 2'513 times. + - rule 'bool_xor: remove false literal' was applied 7'497 times. + - rule 'bool_xor: two active literals' was applied 2'471 times. + - rule 'linear1: x in domain' was applied 119 times. + - rule 'linear: fixed or dup variables' was applied 2'513 times. + - rule 'linear: remapped using affine relations' was applied 1'181 times. + - rule 'presolve: 2632 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 2 times. + +Presolved satisfaction model '': (model_fingerprint: 0x7d9f052d83449aec) +#Variables: 47'121 (42'561 primary variables) + - 47'121 Booleans in [0,1] +#kBoolXor: 43'400 +#kLinearN: 4'560 (#terms: 48'175) +[Symmetry] Graph for symmetry has 140'785 nodes and 224'079 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 3.27558 dtime: 1.00026 +[Symmetry] #generators: 46, average support size: 3159.96 +[Symmetry] 2960 orbits on 35650 variables with sizes: 64,64,64,64,64,64,64,64,64,64,... +[Symmetry] Found orbitope of size 947 x 2 + +Preloading model. +#Model 13.61s var:47121/47121 constraints:47960/47960 + +Starting search at 13.62s with 6 workers. +4 full problem subsolvers: [default_lp, max_lp_sym, no_lp, quick_restart] +2 first solution subsolvers: [fj, fs_random_no_lp] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 29.79m, 29.79m] 29.79m 0.00ns 29.79m 2 [ 14.93ms, 3.83m] 1.91m 1.91m 3.83m + 'feasibility_pump': 7980 [ 9.68ms, 600.18ms] 22.76ms 11.11ms 3.03m 7979 [316.41us, 316.41us] 316.41us 0.00ns 2.52s + 'fj': 819 [498.46ms, 3.43s] 975.72ms 305.37ms 13.32m 819 [101.06ms, 117.19ms] 104.33ms 5.54ms 1.42m + 'fs_random_no_lp': 1 [ 29.77m, 29.77m] 29.77m 0.00ns 29.77m 2 [ 13.15ms, 4.27m] 2.14m 2.14m 4.27m + 'max_lp_sym': 1 [ 29.77m, 29.77m] 29.77m 0.00ns 29.77m 2 [ 13.69ms, 37.76s] 18.89s 18.87s 37.78s + 'no_lp': 1 [ 29.77m, 29.77m] 29.77m 0.00ns 29.77m 2 [ 13.15ms, 6.66m] 3.33m 3.33m 6.66m + 'quick_restart': 1 [ 29.79m, 29.79m] 29.79m 0.00ns 29.79m 2 [ 14.93ms, 59.78s] 29.90s 29.88s 59.80s + 'rins/rens': 243 [154.87ms, 11.11s] 3.30s 3.12s 13.36m 121 [ 11.98ms, 100.16ms] 97.12ms 13.27ms 11.75s + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 47'121 2'745'448 8'904'588 1'291 2'702'654 5'477'864 105'734'527 63'516'916 + 'fs_random_no_lp': 47'121 3'223'895 12'812'688 1'898 3'605'044 6'873'577 187'386'920 166'441'285 + 'max_lp_sym': 47'121 275'493 651'999 2 188'486 462'117 50'969'491 102'069'427 + 'no_lp': 47'121 4'318'858 12'384'747 12'279 3'173'770 7'512'682 172'416'183 96'838'747 + 'quick_restart': 47'121 57'811 12'510'820 5'117 5'292'745 5'419'573 21'112'098 33'181'473 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 0 0 47'121 47'121 0 136'943 8'731 + 'fs_random_no_lp': 0 0 47'121 47'121 0 128'302 11'764 + 'max_lp_sym': 0 0 47'121 47'121 0 12'871 15'966 + 'no_lp': 0 0 47'121 47'121 0 270'201 13'994 + 'quick_restart': 0 0 47'121 47'121 0 29'039 11'662 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 1'779'644 18'187'690 0 84'910'185 73'351'502 320'762 + 'fs_random_no_lp': 2'042'392 17'429'039 0 113'492'708 97'827'992 369'160 + 'max_lp_sym': 210'076 2'574'638 0 11'909'967 10'543'227 9'599 + 'no_lp': 2'398'433 22'051'874 0 125'265'491 108'418'971 468'434 + 'quick_restart': 7'901 20'374 0 1'028'162 646'155 7'788 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 322'099 3'027'833 0 13'084 208'572 297'072 1'959 + 'fs_random_no_lp': 481'316 4'033'597 0 10'439 154'458 315'223 1'084 + 'max_lp_sym': 0 0 0 0 0 0 0 + 'no_lp': 316'937 3'246'808 0 11'179 210'970 286'327 2'509 + 'quick_restart': 1'121'804 3'952'459 0 8'375 39'582 134'858 57 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 0 0 0 313'131 26'330 5'321 7'631 13'084 0 5'071 0 0 2'258'756 7'252'819 2'745'448 + 'fs_random_no_lp': 0 0 0 357'457 27'351 103 11'703 10'439 0 9'583 0 0 2'695'560 9'327'741 3'223'895 + 'max_lp_sym': 0 0 0 9'188 1'878 0 411 0 0 0 0 0 235'179 981'976 275'493 + 'no_lp': 0 0 0 451'725 46'356 5'804 16'709 11'179 0 11'729 0 0 3'511'889 9'800'638 4'318'858 + 'quick_restart': 0 0 0 7'676 1'016 8 112 8'375 0 560 0 0 28'473 75'011 57'811 + +Lp stats Component Iterations AddedCuts OPTIMAL DUAL_F. DUAL_U. + 'default_lp': 94 1'735'931 5'655 1'783'043 0 0 + 'max_lp_sym': 315 209'065 0 1'457'828 8 0 + 'quick_restart': 94 1'832'099 181'661 1'578'507 0 0 + +Lp dimension Final dimension of first component + 'default_lp': 2 rows, 22 columns, 23 entries + 'max_lp_sym': 2 rows, 22 columns, 23 entries + 'quick_restart': 2 rows, 22 columns, 23 entries + +Lp debug CutPropag CutEqPropag Adjust Overflow Bad BadScaling + 'default_lp': 0 74 0 0 6'277 0 + 'max_lp_sym': 0 0 0 0 0 0 + 'quick_restart': 0 3'925 0 0 465'153 0 + +Lp pool Constraints Updates Simplif Merged Shortened Split Strengthened Cuts/Call + 'default_lp': 6'803 406 0 0 0 0 212 5'655/18'536 + 'max_lp_sym': 411 0 0 0 0 0 0 0/0 + 'quick_restart': 182'809 20'397 0 0 0 0 12'007 181'661/606'809 + +Lp Cut default_lp quick_restart + CG_FF: 807 27'796 + CG_K: 166 4'311 + CG_KL: 123 2'599 + CG_R: 981 45'985 + MIR_1_FF: 1'351 31'403 + MIR_1_K: 262 2'951 + MIR_1_KL: 9 160 + MIR_1_R: 785 15'507 + MIR_2_FF: 251 12'715 + MIR_2_K: 1 155 + MIR_2_KL: - 328 + MIR_2_R: 83 5'409 + MIR_3_FF: 32 2'365 + MIR_3_K: - 68 + MIR_3_KL: - 86 + MIR_3_R: 16 1'373 + MIR_4_FF: 5 352 + MIR_4_K: - 9 + MIR_4_KL: - 12 + MIR_4_R: 5 291 + MIR_5_FF: - 28 + MIR_5_K: - 1 + MIR_5_KL: - 1 + MIR_5_R: - 45 + MIR_6_FF: - 7 + MIR_6_K: - 1 + MIR_6_R: - 12 + ZERO_HALF_FF: 305 9'950 + ZERO_HALF_K: 15 576 + ZERO_HALF_KL: 16 197 + ZERO_HALF_R: 442 16'968 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 242/242 53% 9.92e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 22 12 237'845 583'756 0 0 106 3'255'767 + 'fj_restart_compound': 42 12 0 284'025 186'378 48'611 0 7'387'067 + 'fj_restart_compound_obj': 52 20 0 390'879 299'468 45'486 0 9'540'988 + 'fj_restart_compound_perturb': 32 11 0 226'540 168'050 28'926 0 5'804'602 + 'fj_restart_compound_perturb_obj': 39 18 0 312'198 260'481 25'421 0 7'597'062 + 'fj_restart_decay': 23 13 256'508 773'150 0 0 86 3'272'289 + 'fj_restart_decay_compound': 70 23 0 478'306 340'643 68'536 0 12'341'617 + 'fj_restart_decay_compound_obj': 39 20 0 349'718 287'939 30'417 0 7'898'201 + 'fj_restart_decay_compound_perturb': 75 17 0 429'774 247'810 90'366 0 12'143'415 + 'fj_restart_decay_compound_perturb_obj': 57 12 0 312'007 176'865 66'925 0 9'086'628 + 'fj_restart_decay_obj': 58 20 427'078 2'001'929 0 0 233 7'312'809 + 'fj_restart_decay_perturb': 55 20 412'856 1'903'207 0 0 221 6'975'584 + 'fj_restart_decay_perturb_obj': 59 18 386'495 2'059'381 0 0 240 7'226'092 + 'fj_restart_obj': 113 20 481'943 3'002'375 0 0 714 13'877'412 + 'fj_restart_perturb': 28 10 205'620 753'530 0 0 157 3'788'939 + 'fj_restart_perturb_obj': 55 17 358'448 1'473'567 0 0 312 7'270'406 + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 0 0 0 + 'fj solution hints': 255 0 255 + 'lp solutions': 4'635 111 3'712 + 'pump': 7'979 132 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 11'976 29'770 0 0 + 'fs_random_no_lp': 16'226 28'475 0 0 + 'max_lp_sym': 2'512 0 0 0 + 'no_lp': 25'740 21'860 0 0 + 'quick_restart': 7'372 29'119 0 0 + +LRAT_status: NA +CpSolverResponse summary: +status: UNKNOWN +objective: NA +best_bound: NA +integers: 47121 +booleans: 47121 +conflicts: 4318858 +branches: 12384747 +propagations: 172416183 +integer_propagations: 96838747 +restarts: 12279 +lp_iterations: 0 +walltime: 1801.85 +usertime: 1801.85 +deterministic_time: 1082.91 +gap_integral: 0 + diff --git a/research/line-system-510-signing-nonexistence/logs/sat_sb_k1_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_sb_k1_cpsat.txt new file mode 100644 index 0000000000..4c1ade5c0c --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_sb_k1_cpsat.txt @@ -0,0 +1,327 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 300 log_search_progress: true num_search_workers: 6 + +Initial satisfaction model '': (model_fingerprint: 0xf147780b7ad01259) +#Variables: 14'374 (13'546 primary variables) + - 14'374 Booleans in [0,1] +#kBoolAnd: 45 (#enforced: 45) (#literals: 90) +#kBoolXor: 12'691 +#kLinear1: 48 +#kLinear2: 2'700 (#enforced: 915) +#kLinear3: 870 +#kLinearN: 736 (#terms: 12'032) + +Starting presolve at 0.05s + 8.25e-03s 0.00e+00d [DetectDominanceRelations] + 9.89e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 9.87e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 1.38e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 1.02e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 42'203 nodes and 67'489 arcs. +[Symmetry] Symmetry computation done. time: 0.0317963 dtime: 0.0241713 +[SAT presolve] num removable Booleans: 870 / 12'737 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:3'434 literals:8'519 vars:2'161 one_side_vars:2 simple_definition:941 singleton_clauses:0 +[SAT presolve] [0.0018015s] clauses:3'434 literals:8'519 vars:2'161 one_side_vars:2 simple_definition:941 singleton_clauses:0 +[SAT presolve] [0.0137967s] clauses:1'063 literals:7'163 vars:1'347 one_side_vars:830 simple_definition:166 singleton_clauses:0 + 1.20e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=59 + 2.29e-01s 1.10e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=24'562 #fixed_bools=1'397 #equiv=1'580 #new_binary_clauses=5'318 + 2.08e-03s 1.25e-06d [MaxClique] + 9.30e-03s 0.00e+00d [DetectDominanceRelations] + 5.93e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=6 #num_dual_strengthening=3 + 5.57e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 1.25e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=36 + 8.63e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.02e-03s 3.47e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=727 #num_inclusions=104 #num_redundant=26 + 5.61e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 2.58e-03s 3.43e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=1'333 #num_inclusions=28 + 1.20e-02s 3.32e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=45 #num_clauses=581 #num_checked=581 + 4.83e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 3.89e-03s 1.48e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=228 + 1.18e-03s 1.01e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 6.59e-03s 8.68e-04d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 8.86e-04s 4.93e-05d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=727 + 1.83e-03s 2.05e-05d [operations_research::sat::CpModelPresolver::MergeClauses] #num_collisions=14 #num_merges=14 #num_saved_literals=28 + 7.07e-03s 0.00e+00d [DetectDominanceRelations] + 3.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 7.03e-03s 0.00e+00d [DetectDominanceRelations] + 3.01e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.32e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 1.24e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 32'716 nodes and 47'395 arcs. +[Symmetry] Symmetry computation done. time: 0.0153109 dtime: 0.0100029 +[SAT presolve] num removable Booleans: 38 / 8'929 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:622 literals:4'189 vars:919 one_side_vars:564 simple_definition:257 singleton_clauses:0 +[SAT presolve] [0.0002755s] clauses:622 literals:4'189 vars:919 one_side_vars:564 simple_definition:257 singleton_clauses:0 +[SAT presolve] [0.0011318s] clauses:622 literals:4'189 vars:919 one_side_vars:564 simple_definition:257 singleton_clauses:0 + 7.46e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.68e-01s 5.96e-03d [operations_research::sat::CpModelPresolver::Probe] #probed=24'400 #fixed_bools=13 #equiv=70 #new_binary_clauses=1'796 + 7.24e-04s 9.01e-05d [MaxClique] + 9.08e-03s 0.00e+00d [DetectDominanceRelations] + 3.18e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 4.60e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 7.78e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=40 + 7.42e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.85e-03s 3.39e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=725 #num_inclusions=90 #num_redundant=12 + 5.27e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 2.46e-03s 3.36e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=1'340 + 4.44e-03s 3.29e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=36 #num_clauses=580 #num_checked=580 + 8.39e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 1.08e-03s 2.10e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=325 + 2.18e-03s 4.73e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 5.66e-03s 8.55e-04d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 9.06e-04s 4.86e-05d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=725 + 1.66e-03s 2.05e-05d [operations_research::sat::CpModelPresolver::MergeClauses] #num_collisions=14 #num_merges=14 #num_saved_literals=28 + 7.03e-03s 0.00e+00d [DetectDominanceRelations] + 3.02e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 6.94e-03s 0.00e+00d [DetectDominanceRelations] + 2.89e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.32e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 7.84e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 32'571 nodes and 47'014 arcs. +[Symmetry] Symmetry computation done. time: 0.0151143 dtime: 0.00983884 +[SAT presolve] num removable Booleans: 38 / 8'842 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:616 literals:4'176 vars:905 one_side_vars:555 simple_definition:252 singleton_clauses:0 +[SAT presolve] [0.0002952s] clauses:616 literals:4'176 vars:905 one_side_vars:555 simple_definition:252 singleton_clauses:0 +[SAT presolve] [0.0012017s] clauses:616 literals:4'176 vars:905 one_side_vars:555 simple_definition:252 singleton_clauses:0 + 7.50e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.52e-01s 5.01e-03d [operations_research::sat::CpModelPresolver::Probe] #probed=24'384 #fixed_bools=8 #equiv=32 #new_binary_clauses=807 + 6.63e-04s 7.58e-05d [MaxClique] + 7.71e-03s 0.00e+00d [DetectDominanceRelations] + 3.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 4.17e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 7.45e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=21 + 7.39e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.85e-03s 3.32e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=724 #num_inclusions=78 + 7.09e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 2.68e-03s 3.36e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=1'337 + 3.79e-03s 3.29e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=33 #num_clauses=580 #num_checked=580 + 7.01e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 1.87e-03s 2.20e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=343 + 3.61e-04s 4.57e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 4.54e-03s 8.59e-04d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 1.01e-03s 4.85e-05d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=724 + 2.50e-03s 2.05e-05d [operations_research::sat::CpModelPresolver::MergeClauses] #num_collisions=14 #num_merges=14 #num_saved_literals=28 + 7.35e-03s 0.00e+00d [DetectDominanceRelations] + 2.88e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.90e-04s 0.00e+00d [MergeNoOverlap] + 3.28e-04s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 2708 affine relations were detected. + - rule 'TODO bool_xor: remove constraint' was applied 1'367 times. + - rule 'TODO dual: only one blocking constraint?' was applied 13'699 times. + - rule 'affine: new relation' was applied 2'708 times. + - rule 'at_most_one: empty or all false' was applied 3 times. + - rule 'at_most_one: removed literals' was applied 3 times. + - rule 'at_most_one: satisfied' was applied 40 times. + - rule 'bool_and: x => x' was applied 1 time. + - rule 'bool_or: always true' was applied 344 times. + - rule 'bool_or: implications' was applied 1'838 times. + - rule 'bool_or: removed enforcement literal' was applied 826 times. + - rule 'bool_or: singleton' was applied 2 times. + - rule 'bool_xor: always true' was applied 2'873 times. + - rule 'bool_xor: one active literal' was applied 661 times. + - rule 'bool_xor: remove false literal' was applied 4'859 times. + - rule 'bool_xor: two active literals' was applied 980 times. + - rule 'dual: enforced equivalence' was applied 1 time. + - rule 'dual: fix variable' was applied 14 times. + - rule 'duplicate: removed constraint' was applied 97 times. + - rule 'duplicate: removed enforced constraint' was applied 59 times. + - rule 'enforcement: always false' was applied 45 times. + - rule 'enforcement: false literal' was applied 4 times. + - rule 'enforcement: true literal' was applied 43 times. + - rule 'linear inclusion: sparsify superset' was applied 38 times. + - rule 'linear1: x in domain' was applied 47 times. + - rule 'linear2: convert ax + by != cte to clauses' was applied 2'654 times. + - rule 'linear: always true' was applied 47 times. + - rule 'linear: divide by GCD' was applied 26 times. + - rule 'linear: empty' was applied 12 times. + - rule 'linear: fixed or dup variables' was applied 1'308 times. + - rule 'linear: negative clause' was applied 783 times. + - rule 'linear: positive clause' was applied 42 times. + - rule 'linear: remapped using affine relations' was applied 521 times. + - rule 'presolve: 2187 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 3 times. + - rule 'probing: bool_or reduced to implication' was applied 203 times. + - rule 'probing: simplified clauses' was applied 283 times. + - rule 'setppc: removed dominated constraints' was applied 25 times. + +Presolved satisfaction model '': (model_fingerprint: 0x7b09508a70e5b630) +#Variables: 8'710 (8'085 primary variables) + - 8'710 Booleans in [0,1] +#kBoolAnd: 23 (#enforced: 23) (#literals: 56) +#kBoolAndClauses: 14 (#enforced: 14 #multi: 14) (#literals: 56) +#kBoolOr: 552 (#literals: 4'020) +#kBoolXor: 8'093 +#kLinearN: 724 (#terms: 9'698) +[Symmetry] Graph for symmetry has 26'832 nodes and 46'858 arcs. +[Symmetry] Symmetry computation done. time: 0.0135246 dtime: 0.00948721 + +Preloading model. +#Model 1.46s var:8710/8710 constraints:9406/9406 + +Starting search at 1.46s with 6 workers. +4 full problem subsolvers: [default_lp, max_lp, no_lp, quick_restart] +2 first solution subsolvers: [fj, fs_random_no_lp] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + +#Model 1.87s var:8622/8710 constraints:9389/9406 +#Model 1.99s var:8589/8710 constraints:9384/9406 +#Model 2.10s var:8577/8710 constraints:9381/9406 +#Model 2.18s var:8484/8710 constraints:9342/9406 +#Model 2.20s var:8447/8710 constraints:9337/9406 +#Model 2.33s var:8399/8710 constraints:9324/9406 +#Model 2.45s var:8391/8710 constraints:9323/9406 +#Model 2.58s var:8384/8710 constraints:9318/9406 +#Model 2.74s var:8382/8710 constraints:9318/9406 +#Model 3.16s var:8368/8710 constraints:9307/9406 +#1 3.74s fs_random_no_lp + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 2.30s, 2.30s] 2.30s 0.00ns 2.30s 2 [ 7.45ms, 143.12ms] 75.28ms 67.83ms 150.57ms + 'feasibility_pump': 15 [ 4.37ms, 86.12ms] 13.86ms 21.66ms 207.97ms 14 [ 89.17us, 5.28ms] 475.80us 1.33ms 6.66ms + 'fj': 4 [266.69ms, 532.20ms] 460.14ms 111.91ms 1.84s 4 [100.33ms, 125.41ms] 115.97ms 9.43ms 463.88ms + 'fs_random_no_lp': 1 [ 2.28s, 2.28s] 2.28s 0.00ns 2.28s 2 [ 3.14ms, 182.03ms] 92.59ms 89.45ms 185.18ms + 'max_lp': 1 [ 2.30s, 2.30s] 2.30s 0.00ns 2.30s 2 [ 25.60ms, 200.20ms] 112.90ms 87.30ms 225.79ms + 'no_lp': 1 [ 2.30s, 2.30s] 2.30s 0.00ns 2.30s 2 [ 3.14ms, 176.87ms] 90.00ms 86.86ms 180.01ms + 'quick_restart': 1 [ 2.29s, 2.29s] 2.29s 0.00ns 2.29s 2 [ 6.21ms, 176.98ms] 91.60ms 85.39ms 183.19ms + 'rins/rens': 15 [ 8.22ms, 16.83ms] 9.64ms 1.99ms 144.56ms 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 8'710 1'827 43'934 2 35'340 37'771 165'547 179'876 + 'fs_random_no_lp': 8'710 6'244 79'561 42 52'173 59'562 867'667 758'932 + 'max_lp': 8'710 212 76'410 3 63'207 65'191 153'175 222'501 + 'no_lp': 8'710 5'543 75'841 42 50'958 57'591 794'186 738'746 + 'quick_restart': 8'710 258 81'907 18 64'313 66'390 182'288 223'628 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 133 0 8'710 8'577 4'136 805 1'322 + 'fs_random_no_lp': 342 1'262 8'710 7'106 8'130 1'980 3'331 + 'max_lp': 342 1'479 8'710 6'889 6'652 493 96 + 'no_lp': 342 1'353 8'710 7'015 7'868 963 3'726 + 'quick_restart': 342 1'472 8'710 6'896 7'650 540 24 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 1'132 5'615 1'062 29'257 0 236 + 'fs_random_no_lp': 3'580 13'123 2'221 82'727 0 813 + 'max_lp': 109 383 48 1'995 0 47 + 'no_lp': 2'761 11'252 1'254 87'265 0 753 + 'quick_restart': 101 233 55 1'625 0 60 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 1'161 6'089 0 0 0 961 0 + 'fs_random_no_lp': 2'921 13'953 0 69 521 2'884 9 + 'max_lp': 2'463 12'852 0 3 31 2'219 0 + 'no_lp': 3'231 17'350 0 73 811 3'236 12 + 'quick_restart': 3'350 16'604 2 32 263 3'126 2 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 0 0 0 232 40 0 4 0 0 0 0 0 0 3'827 1'827 + 'fs_random_no_lp': 77 78 26 793 174 7 20 69 166 24 0 0 0 8'069 6'244 + 'max_lp': 39 32 10 44 0 3 3 3 29 18 0 0 0 202 212 + 'no_lp': 98 55 9 738 259 5 15 73 3 77 0 0 0 9'550 5'543 + 'quick_restart': 67 48 10 55 0 3 5 32 11 10 0 0 0 86 258 + +Lp stats Component Iterations AddedCuts OPTIMAL DUAL_F. DUAL_U. + 'default_lp': 8 13'689 188 5'204 0 102 + 'max_lp': 4 4'162 559 261 174 7 + 'quick_restart': 8 4'161 1'045 928 0 51 + +Lp dimension Final dimension of first component + 'default_lp': 74 rows, 169 columns, 962 entries + 'max_lp': 535 rows, 1790 columns, 5160 entries + 'quick_restart': 69 rows, 169 columns, 897 entries + +Lp debug CutPropag CutEqPropag Adjust Overflow Bad BadScaling + 'default_lp': 0 0 48 0 528 0 + 'max_lp': 4 0 5 0 6'586 0 + 'quick_restart': 0 21 2 0 4'111 0 + +Lp pool Constraints Updates Simplif Merged Shortened Split Strengthened Cuts/Call + 'default_lp': 446 0 0 0 0 0 0 188/339 + 'max_lp': 1'452 57 0 0 19 0 11 559/1'138 + 'quick_restart': 1'303 50 0 0 0 0 11 1'045/1'940 + +Lp Cut default_lp max_lp quick_restart + CG_FF: 20 36 107 + CG_K: 1 6 29 + CG_KL: - 4 3 + CG_R: 20 32 126 + Clique: - 33 - + MIR_1_FF: 55 91 351 + MIR_1_K: - 2 26 + MIR_1_KL: - - 1 + MIR_1_R: 25 26 183 + MIR_1_RLT: - 71 - + MIR_2_FF: 29 83 90 + MIR_2_K: - - 4 + MIR_2_R: 5 17 20 + MIR_3_FF: 10 20 15 + MIR_3_R: 4 9 6 + MIR_4_FF: 9 9 12 + MIR_4_K: - - 1 + MIR_4_R: 1 3 4 + MIR_5_FF: 4 5 5 + MIR_5_K: - - 1 + MIR_5_R: 2 1 6 + MIR_6_FF: 3 - - + MIR_6_R: - - 5 + ZERO_HALF_FF: - 80 16 + ZERO_HALF_KL: - - 2 + ZERO_HALF_R: - 31 32 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 0/0 0% 5.00e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 1 1 6'695 32'262 0 0 6'974 152'373 + 'fj_restart_decay_perturb': 1 1 6'070 40'013 0 0 473 131'700 + 'fj_restart_perturb_obj': 2 2 20'726 32'320 0 0 41'530 337'409 + +Solutions (1) Num Rank + 'fs_random_no_lp': 1 [0,0] + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 1 0 1 + 'fj solution hints': 0 0 0 + 'lp solutions': 9 15 6 + 'pump': 0 0 + +Improving bounds shared Num Sym + 'fs_random_no_lp': 160 0 + 'max_lp': 90 0 + 'no_lp': 37 0 + 'quick_restart': 55 0 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 1 0 2'041 5'227 + 'fs_random_no_lp': 1'781 0 5'226 5'227 + 'max_lp': 2'702 0 4'985 5'227 + 'no_lp': 295 0 5'227 5'227 + 'quick_restart': 448 0 5'227 5'227 + +LRAT_status: NA +CpSolverResponse summary: +status: OPTIMAL +objective: NA +best_bound: NA +integers: 8047 +booleans: 8710 +conflicts: 6244 +branches: 79561 +propagations: 867667 +integer_propagations: 758932 +restarts: 42 +lp_iterations: 0 +walltime: 3.83335 +usertime: 3.83335 +deterministic_time: 1.42066 +gap_integral: 0 +solution_fingerprint: 0x690e1c9dc98c0244 + diff --git a/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c1_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c1_cpsat.txt new file mode 100644 index 0000000000..1ede08960c --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c1_cpsat.txt @@ -0,0 +1,291 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 600 log_search_progress: true num_search_workers: 2 + +Initial satisfaction model '': (model_fingerprint: 0xb63411cd49266ac7) +#Variables: 14'252 (13'427 primary variables) + - 14'252 Booleans in [0,1] +#kBoolAnd: 42 (#enforced: 42) (#literals: 84) +#kBoolXor: 12'630 +#kLinear1: 48 +#kLinear2: 2'520 (#enforced: 854) +#kLinear3: 812 +#kLinearN: 736 (#terms: 12'032) + +Starting presolve at 0.07s + 1.29e-02s 0.00e+00d [DetectDominanceRelations] + 9.53e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 7.83e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 1.44e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 1.02e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 41'672 nodes and 66'500 arcs. +[Symmetry] Symmetry computation done. time: 0.0359861 dtime: 0.0207264 +[SAT presolve] num removable Booleans: 812 / 12'615 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:3'202 literals:7'942 vars:2'045 one_side_vars:11 simple_definition:972 singleton_clauses:0 +[SAT presolve] [0.0004875s] clauses:3'202 literals:7'942 vars:2'045 one_side_vars:11 simple_definition:972 singleton_clauses:0 +[SAT presolve] [0.011558s] clauses:984 literals:6'724 vars:1'283 one_side_vars:784 simple_definition:238 singleton_clauses:0 + 1.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=1 + 2.34e-01s 1.44e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=26'982 #fixed_bools=33 #equiv=426 #new_binary_clauses=6'128 + 8.28e-04s 7.88e-05d [MaxClique] Merged 40 constraints with 80 literals into 30 constraints with 60 literals + 1.16e-02s 0.00e+00d [DetectDominanceRelations] + 5.20e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 8.39e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 1.50e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=43 + 1.10e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.92e-03s 3.49e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=733 + 6.27e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 3.45e-03s 4.54e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=1'689 #num_inclusions=74 + 4.80e-03s 4.79e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=20 #num_clauses=865 #num_checked=865 + 8.20e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 1.21e-03s 1.30e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=170 + 3.88e-04s 4.57e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 6.66e-03s 1.13e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 1.17e-03s 5.67e-05d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=733 + 2.15e-03s 3.13e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 7.99e-03s 0.00e+00d [DetectDominanceRelations] + 3.52e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 7.58e-03s 0.00e+00d [DetectDominanceRelations] + 3.25e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.48e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 9.98e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 37'895 nodes and 61'113 arcs. +[Symmetry] Symmetry computation done. time: 0.0175041 dtime: 0.0117834 +[SAT presolve] num removable Booleans: 50 / 11'388 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:884 literals:6'288 vars:1'232 one_side_vars:753 simple_definition:208 singleton_clauses:0 +[SAT presolve] [0.0003567s] clauses:883 literals:6'280 vars:1'232 one_side_vars:753 simple_definition:208 singleton_clauses:0 +[SAT presolve] [0.0014353s] clauses:883 literals:6'280 vars:1'232 one_side_vars:753 simple_definition:208 singleton_clauses:0 + 1.38e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.83e-01s 5.63e-03d [operations_research::sat::CpModelPresolver::Probe] #probed=26'944 #equiv=13 #new_binary_clauses=501 + 5.51e-04s 1.96e-05d [MaxClique] + 1.06e-02s 0.00e+00d [DetectDominanceRelations] + 3.93e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 7.72e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 1.17e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=1 + 1.02e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.92e-03s 3.49e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=733 + 7.43e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 3.46e-03s 4.38e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=1'616 + 5.28e-03s 4.80e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=19 #num_clauses=864 #num_checked=864 + 8.83e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 1.24e-03s 1.05e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=138 + 4.47e-04s 4.86e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 8.31e-03s 1.13e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 1.12e-03s 5.67e-05d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=733 + 2.42e-03s 3.12e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 8.14e-03s 0.00e+00d [DetectDominanceRelations] + 3.38e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 8.12e-03s 0.00e+00d [DetectDominanceRelations] + 3.36e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.66e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 1.05e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 37'880 nodes and 61'089 arcs. +[Symmetry] Symmetry computation done. time: 0.0213272 dtime: 0.0118233 +[SAT presolve] num removable Booleans: 50 / 11'375 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:883 literals:6'280 vars:1'232 one_side_vars:753 simple_definition:208 singleton_clauses:0 +[SAT presolve] [0.0003667s] clauses:883 literals:6'280 vars:1'232 one_side_vars:753 simple_definition:208 singleton_clauses:0 +[SAT presolve] [0.0015563s] clauses:883 literals:6'280 vars:1'232 one_side_vars:753 simple_definition:208 singleton_clauses:0 + 9.80e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.83e-01s 5.52e-03d [operations_research::sat::CpModelPresolver::Probe] #probed=26'944 #new_binary_clauses=408 + 6.15e-04s 1.90e-05d [MaxClique] + 1.16e-02s 0.00e+00d [DetectDominanceRelations] + 4.04e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 7.88e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 1.15e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 1.04e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 1.62e-03s 3.49e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=733 + 6.29e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 2.87e-03s 4.38e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=1'616 + 3.60e-03s 4.80e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=19 #num_clauses=864 #num_checked=864 + 8.14e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 1.85e-03s 1.25e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=162 + 6.10e-04s 4.86e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 9.56e-03s 1.13e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 1.71e-03s 5.67e-05d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=733 + 2.83e-03s 3.12e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 8.97e-03s 0.00e+00d [DetectDominanceRelations] + 3.80e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 3.87e-04s 0.00e+00d [MergeNoOverlap] + 4.55e-04s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 1461 affine relations were detected. + - rule 'TODO bool_xor: remove constraint' was applied 48 times. + - rule 'TODO dual: only one blocking constraint?' was applied 10'837 times. + - rule 'affine: new relation' was applied 1'461 times. + - rule 'at_most_one: removed literals' was applied 4 times. + - rule 'at_most_one: satisfied' was applied 2 times. + - rule 'at_most_one: size one' was applied 4 times. + - rule 'at_most_one: transformed into max clique' was applied 1 time. + - rule 'bool_or: always true' was applied 42 times. + - rule 'bool_or: implications' was applied 1'668 times. + - rule 'bool_or: removed enforcement literal' was applied 768 times. + - rule 'bool_xor: always true' was applied 237 times. + - rule 'bool_xor: one active literal' was applied 658 times. + - rule 'bool_xor: remove false literal' was applied 2'360 times. + - rule 'bool_xor: two active literals' was applied 980 times. + - rule 'duplicate: removed constraint' was applied 44 times. + - rule 'duplicate: removed enforced constraint' was applied 1 time. + - rule 'enforcement: always false' was applied 42 times. + - rule 'enforcement: true literal' was applied 40 times. + - rule 'linear1: x in domain' was applied 47 times. + - rule 'linear2: convert ax + by != cte to clauses' was applied 2'474 times. + - rule 'linear: always true' was applied 47 times. + - rule 'linear: empty' was applied 3 times. + - rule 'linear: fixed or dup variables' was applied 691 times. + - rule 'linear: negative clause' was applied 728 times. + - rule 'linear: positive clause' was applied 42 times. + - rule 'linear: remapped using affine relations' was applied 512 times. + - rule 'presolve: 780 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 3 times. + - rule 'probing: bool_or reduced to implication' was applied 4 times. + - rule 'probing: simplified clauses' was applied 31 times. + - rule 'setppc: removed dominated constraints' was applied 74 times. + +Presolved satisfaction model '': (model_fingerprint: 0x5bd4f0a0d1ade39d) +#Variables: 11'291 (10'604 primary variables) + - 11'291 Booleans in [0,1] +#kBoolAnd: 19 (#enforced: 19) (#literals: 38) +#kBoolOr: 864 (#literals: 6'242) +#kBoolXor: 10'719 +#kLinearN: 733 (#terms: 11'340) +[Symmetry] Graph for symmetry has 34'919 nodes and 61'089 arcs. +[Symmetry] Symmetry computation done. time: 0.0206871 dtime: 0.0116456 + +Preloading model. +#Model 1.63s var:11291/11291 constraints:12335/12335 + +Starting search at 1.63s with 2 workers. +1 full problem subsolver: [default_lp] +1 first solution subsolver: [fj] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + +#Model 12.64s var:11289/11291 constraints:12332/12335 +#Model 22.20s var:11287/11291 constraints:12324/12335 +#1 50.86s default_lp + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 49.23s, 49.23s] 49.23s 0.00ns 49.23s 2 [ 10.06ms, 4.04s] 2.02s 2.01s 4.05s + 'feasibility_pump': 458 [ 3.63ms, 75.12ms] 7.01ms 4.03ms 3.21s 457 [104.37us, 1.43ms] 133.92us 61.05us 61.20ms + 'fj': 111 [179.53ms, 1.14s] 414.16ms 155.19ms 45.97s 111 [ 46.84ms, 122.38ms] 102.17ms 6.34ms 11.34s + 'rins/rens': 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 11'291 12'939 382'590 90 238'675 264'495 2'810'309 2'713'877 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 4 59 11'291 11'228 2'166 1'801 4'889 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 7'974 43'050 12'187 252'834 92'062 1'777 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 27'056 136'182 0 369 4'071 27'914 133 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 0 1 6 1'749 50 37 28 369 42 217 0 0 4'468 20'731 12'939 + +Lp stats Component Iterations AddedCuts OPTIMAL DUAL_F. DUAL_U. + 'default_lp': 60 242'671 7'272 120'984 0 0 + +Lp dimension Final dimension of first component + 'default_lp': 103 rows, 1216 columns, 1537 entries + +Lp debug CutPropag CutEqPropag Adjust Overflow Bad BadScaling + 'default_lp': 0 83 0 0 24'039 0 + +Lp pool Constraints Updates Simplif Merged Shortened Split Strengthened Cuts/Call + 'default_lp': 7'686 294 0 0 0 0 218 7'272/18'184 + +Lp Cut default_lp + CG_FF: 1'491 + CG_K: 325 + CG_KL: 109 + CG_R: 1'027 + MIR_1_FF: 1'187 + MIR_1_K: 125 + MIR_1_KL: 1 + MIR_1_R: 548 + MIR_2_FF: 621 + MIR_2_K: 11 + MIR_2_KL: 15 + MIR_2_R: 135 + MIR_3_FF: 178 + MIR_3_K: 8 + MIR_3_KL: 6 + MIR_3_R: 70 + MIR_4_FF: 108 + MIR_4_K: 4 + MIR_4_KL: 3 + MIR_4_R: 48 + MIR_5_FF: 75 + MIR_5_K: 2 + MIR_5_KL: 1 + MIR_5_R: 24 + MIR_6_FF: 43 + MIR_6_K: 2 + MIR_6_KL: 2 + MIR_6_R: 21 + ZERO_HALF_FF: 660 + ZERO_HALF_K: 35 + ZERO_HALF_KL: 9 + ZERO_HALF_R: 378 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 0/0 0% 5.00e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 9 5 28'665 255'145 0 0 1'269 919'449 + 'fj_restart_compound': 9 5 0 80'579 28'211 26'112 0 1'294'801 + 'fj_restart_compound_obj': 4 2 0 34'679 11'437 11'618 0 570'696 + 'fj_restart_compound_perturb': 9 2 0 70'865 11'719 29'506 0 1'192'480 + 'fj_restart_compound_perturb_obj': 5 2 0 43'560 11'410 16'022 0 699'965 + 'fj_restart_decay': 8 4 22'484 293'645 0 0 403 700'697 + 'fj_restart_decay_compound': 6 2 0 48'201 12'031 18'073 0 818'222 + 'fj_restart_decay_compound_obj': 3 3 0 30'526 16'894 6'798 0 476'860 + 'fj_restart_decay_compound_perturb': 8 8 0 83'446 43'827 19'710 0 1'274'520 + 'fj_restart_decay_obj': 10 3 18'376 366'818 0 0 511 844'565 + 'fj_restart_decay_perturb': 6 4 21'705 223'676 0 0 347 551'580 + 'fj_restart_decay_perturb_obj': 11 3 19'848 402'204 0 0 602 941'322 + 'fj_restart_obj': 4 2 14'709 113'124 0 0 1'617 450'553 + 'fj_restart_perturb': 15 7 40'794 403'505 0 0 2'591 1'465'885 + 'fj_restart_perturb_obj': 4 3 17'984 115'818 0 0 1'084 450'844 + +Solutions (1) Num Rank + 'default_lp': 1 [0,0] + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 1 0 1 + 'fj solution hints': 47 0 47 + 'lp solutions': 0 0 0 + 'pump': 0 0 + +Improving bounds shared Num Sym + 'default_lp': 4 0 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 3'177 0 2'876 2'876 + +LRAT_status: NA +CpSolverResponse summary: +status: OPTIMAL +objective: NA +best_bound: NA +integers: 10518 +booleans: 11291 +conflicts: 12939 +branches: 382590 +propagations: 2810309 +integer_propagations: 2713877 +restarts: 90 +lp_iterations: 242671 +walltime: 50.9234 +usertime: 50.9234 +deterministic_time: 15.479 +gap_integral: 0 +solution_fingerprint: 0x740471355a0aeb8e + diff --git a/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_cpsat.txt new file mode 100644 index 0000000000..69ae5cadb3 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_cpsat.txt @@ -0,0 +1,448 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 1800 log_search_progress: true num_search_workers: 6 + +Initial satisfaction model '': (model_fingerprint: 0x293fd1b4e3008564) +#Variables: 37'222 (34'563 primary variables) + - 37'222 Booleans in [0,1] +#kBoolAnd: 77 (#enforced: 77) (#literals: 154) +#kBoolXor: 33'459 +#kLinear1: 88 +#kLinear2: 5'068 (#enforced: 1'715) +#kLinear3: 1'638 +#kLinearN: 2'496 (#terms: 32'768) + +Starting presolve at 0.20s + 2.54e-02s 0.00e+00d [DetectDominanceRelations] + 2.66e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 2.04e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 4.01e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 3.22e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 110'156 nodes and 175'460 arcs. +[Symmetry] Symmetry computation done. time: 0.113207 dtime: 0.0547028 +[SAT presolve] num removable Booleans: 1'638 / 33'983 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:6'468 literals:16'055 vars:4'133 one_side_vars:23 simple_definition:1'965 singleton_clauses:0 +[SAT presolve] [0.0014511s] clauses:6'468 literals:16'055 vars:4'133 one_side_vars:23 simple_definition:1'965 singleton_clauses:0 +[SAT presolve] [0.0349169s] clauses:2'001 literals:13'750 vars:2'605 one_side_vars:1588 simple_definition:476 singleton_clauses:0 + 4.00e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=2 + 6.74e-01s 3.03e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=71'642 #fixed_bools=54 #equiv=780 #new_binary_clauses=11'270 + 2.14e-03s 1.26e-04d [MaxClique] Merged 73 constraints with 146 literals into 51 constraints with 102 literals + 2.35e-02s 0.00e+00d [DetectDominanceRelations] + 1.55e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=3 #num_dual_strengthening=2 + 1.56e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.98e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=73 + 2.86e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.22e-03s 9.62e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'491 + 1.61e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 1.39e-02s 1.10e-04d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=4'443 #num_inclusions=147 + 1.16e-02s 9.85e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=39 #num_clauses=1'771 #num_checked=1'771 + 1.66e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 3.35e-03s 1.77e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=235 + 9.80e-04s 8.61e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 1.59e-02s 2.81e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 2.96e-03s 1.58e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'491 + 5.54e-03s 6.42e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.32e-02s 0.00e+00d [DetectDominanceRelations] + 1.00e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.12e-02s 0.00e+00d [DetectDominanceRelations] + 9.62e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 5.88e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 2.80e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 102'690 nodes and 165'045 arcs. +[Symmetry] Symmetry computation done. time: 0.0619838 dtime: 0.033603 +[SAT presolve] num removable Booleans: 109 / 31'614 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:1'808 literals:12'922 vars:2'518 one_side_vars:1536 simple_definition:435 singleton_clauses:0 +[SAT presolve] [0.0007825s] clauses:1'807 literals:12'906 vars:2'518 one_side_vars:1536 simple_definition:435 singleton_clauses:0 +[SAT presolve] [0.0033174s] clauses:1'807 literals:12'906 vars:2'518 one_side_vars:1536 simple_definition:435 singleton_clauses:0 + 2.79e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.98e-01s 1.42e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=71'576 #equiv=27 #new_binary_clauses=1'018 + 2.36e-03s 3.93e-05d [MaxClique] + 2.44e-02s 0.00e+00d [DetectDominanceRelations] + 1.09e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.48e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.93e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=1 + 2.93e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.52e-03s 9.62e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'491 + 1.65e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 7.41e-03s 1.06e-04d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=4'298 + 1.23e-02s 9.87e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=37 #num_clauses=1'770 #num_checked=1'770 + 1.58e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 3.87e-03s 1.70e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=228 + 8.54e-04s 9.07e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 1.58e-02s 2.81e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 3.17e-03s 1.58e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'491 + 6.23e-03s 6.42e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.11e-02s 0.00e+00d [DetectDominanceRelations] + 9.63e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.15e-02s 0.00e+00d [DetectDominanceRelations] + 9.58e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 3.87e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 2.80e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 102'661 nodes and 164'999 arcs. +[Symmetry] Symmetry computation done. time: 0.0603624 dtime: 0.0339088 +[SAT presolve] num removable Booleans: 109 / 31'587 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:1'807 literals:12'906 vars:2'518 one_side_vars:1536 simple_definition:435 singleton_clauses:0 +[SAT presolve] [0.0006357s] clauses:1'807 literals:12'906 vars:2'518 one_side_vars:1536 simple_definition:435 singleton_clauses:0 +[SAT presolve] [0.0033996s] clauses:1'807 literals:12'906 vars:2'518 one_side_vars:1536 simple_definition:435 singleton_clauses:0 + 2.89e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.06e-01s 1.40e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=71'576 #new_binary_clauses=822 + 1.69e-03s 3.81e-05d [MaxClique] + 2.16e-02s 0.00e+00d [DetectDominanceRelations] + 9.90e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.35e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.80e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 2.77e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.48e-03s 9.62e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'491 + 1.55e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 6.65e-03s 1.06e-04d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=4'298 + 1.11e-02s 9.87e-05d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=37 #num_clauses=1'770 #num_checked=1'770 + 1.66e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 3.71e-03s 2.53e-05d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=337 + 8.45e-04s 9.07e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 2.10e-02s 2.81e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 3.92e-03s 1.58e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'491 + 6.52e-03s 6.42e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.16e-02s 0.00e+00d [DetectDominanceRelations] + 1.03e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.20e-03s 0.00e+00d [MergeNoOverlap] + 1.51e-03s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 2904 affine relations were detected. + - rule 'TODO bool_xor: remove constraint' was applied 88 times. + - rule 'TODO dual: only one blocking constraint?' was applied 34'826 times. + - rule 'affine: new relation' was applied 2'904 times. + - rule 'at_most_one: removed literals' was applied 7 times. + - rule 'at_most_one: satisfied' was applied 3 times. + - rule 'at_most_one: size one' was applied 7 times. + - rule 'at_most_one: transformed into max clique' was applied 1 time. + - rule 'bool_and: x => x' was applied 1 time. + - rule 'bool_or: always true' was applied 78 times. + - rule 'bool_or: implications' was applied 3'356 times. + - rule 'bool_or: removed enforcement literal' was applied 1'558 times. + - rule 'bool_xor: always true' was applied 450 times. + - rule 'bool_xor: one active literal' was applied 1'217 times. + - rule 'bool_xor: remove false literal' was applied 4'579 times. + - rule 'bool_xor: two active literals' was applied 2'019 times. + - rule 'dual: enforced equivalence' was applied 1 time. + - rule 'duplicate: removed constraint' was applied 74 times. + - rule 'duplicate: removed enforced constraint' was applied 2 times. + - rule 'enforcement: always false' was applied 77 times. + - rule 'enforcement: true literal' was applied 73 times. + - rule 'linear1: x in domain' was applied 86 times. + - rule 'linear2: convert ax + by != cte to clauses' was applied 4'984 times. + - rule 'linear: always true' was applied 86 times. + - rule 'linear: empty' was applied 5 times. + - rule 'linear: fixed or dup variables' was applied 1'272 times. + - rule 'linear: negative clause' was applied 1'484 times. + - rule 'linear: positive clause' was applied 77 times. + - rule 'linear: remapped using affine relations' was applied 1'047 times. + - rule 'presolve: 1434 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 3 times. + - rule 'probing: bool_or reduced to implication' was applied 9 times. + - rule 'probing: simplified clauses' was applied 39 times. + - rule 'setppc: removed dominated constraints' was applied 147 times. + +Presolved satisfaction model '': (model_fingerprint: 0x22aaceeae7f97d76) +#Variables: 31'433 (29'038 primary variables) + - 31'433 Booleans in [0,1] +#kBoolAnd: 37 (#enforced: 37) (#literals: 74) +#kBoolOr: 1'770 (#literals: 12'832) +#kBoolXor: 29'707 +#kLinearN: 2'491 (#terms: 31'501) +[Symmetry] Graph for symmetry has 96'872 nodes and 164'999 arcs. +[Symmetry] Symmetry computation done. time: 0.0643431 dtime: 0.0335614 + +Preloading model. +#Model 4.61s var:31433/31433 constraints:34005/34005 + +Starting search at 4.61s with 6 workers. +4 full problem subsolvers: [default_lp, max_lp, no_lp, quick_restart] +2 first solution subsolvers: [fj, fs_random_no_lp] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + +#Model 10.31s var:31432/31433 constraints:34003/34005 +#Model 11.31s var:31431/31433 constraints:34000/34005 +#Model 13.43s var:31430/31433 constraints:34000/34005 +#Model 13.99s var:31429/31433 constraints:34000/34005 +#Model 14.07s var:31428/31433 constraints:34000/34005 +#Model 15.98s var:31427/31433 constraints:34000/34005 +#Model 27.63s var:31426/31433 constraints:34000/34005 +#Model 29.35s var:31425/31433 constraints:34000/34005 +#Model 29.43s var:31424/31433 constraints:33992/34005 +#Model 77.30s var:31415/31433 constraints:33984/34005 +#Model 91.35s var:31414/31433 constraints:33984/34005 +#Model 241.90s var:31411/31433 constraints:33984/34005 +#Model 262.36s var:31399/31433 constraints:33980/34005 +#Model 276.59s var:31394/31433 constraints:33969/34005 +#Model 276.67s var:31381/31433 constraints:33966/34005 +#Model 282.70s var:31380/31433 constraints:33966/34005 +#Model 282.99s var:31377/31433 constraints:33966/34005 +#Model 291.23s var:31375/31433 constraints:33964/34005 +#Model 334.19s var:31374/31433 constraints:33955/34005 +#Model 337.21s var:31370/31433 constraints:33955/34005 +#Model 337.35s var:31361/31433 constraints:33955/34005 +#Model 341.77s var:31357/31433 constraints:33955/34005 +#Model 346.33s var:31350/31433 constraints:33948/34005 +#Model 346.59s var:31341/31433 constraints:33948/34005 +#Model 346.68s var:31338/31433 constraints:33948/34005 +#Model 349.75s var:31336/31433 constraints:33948/34005 +#Model 350.56s var:31334/31433 constraints:33948/34005 +#Model 351.33s var:31326/31433 constraints:33948/34005 +#Model 352.66s var:31324/31433 constraints:33948/34005 +#Model 355.66s var:31323/31433 constraints:33948/34005 +#Model 356.79s var:31321/31433 constraints:33948/34005 +#Model 357.40s var:31320/31433 constraints:33948/34005 +#Model 357.55s var:31319/31433 constraints:33948/34005 +#Model 366.57s var:31317/31433 constraints:33948/34005 +#Model 368.08s var:31315/31433 constraints:33948/34005 +#Model 368.23s var:31312/31433 constraints:33948/34005 +#Model 368.33s var:31309/31433 constraints:33948/34005 +#Model 369.43s var:31306/31433 constraints:33948/34005 +#Model 369.63s var:31299/31433 constraints:33948/34005 +#Model 370.37s var:31297/31433 constraints:33948/34005 +#Model 376.82s var:31296/31433 constraints:33948/34005 +#Model 378.18s var:31295/31433 constraints:33948/34005 +#Model 378.53s var:31294/31433 constraints:33948/34005 +#Model 424.16s var:31292/31433 constraints:33939/34005 +#Model 444.96s var:31283/31433 constraints:33937/34005 +#Model 460.51s var:31173/31433 constraints:33907/34005 +#Model 470.11s var:31156/31433 constraints:33887/34005 +#Model 474.30s var:31155/31433 constraints:33886/34005 +#Model 475.76s var:31144/31433 constraints:33867/34005 +#Model 475.86s var:31134/31433 constraints:33867/34005 +#Model 476.18s var:31113/31433 constraints:33852/34005 +#Model 476.70s var:31110/31433 constraints:33852/34005 +#Model 476.84s var:31109/31433 constraints:33851/34005 +#Model 476.95s var:31108/31433 constraints:33851/34005 +#Model 479.28s var:31104/31433 constraints:33851/34005 +#Model 480.86s var:31102/31433 constraints:33849/34005 +#Model 482.65s var:31099/31433 constraints:33848/34005 +#Model 483.16s var:31097/31433 constraints:33848/34005 +#Model 483.36s var:31093/31433 constraints:33848/34005 +#Model 483.68s var:31088/31433 constraints:33848/34005 +#Model 489.31s var:31079/31433 constraints:33845/34005 +#Model 489.67s var:31065/31433 constraints:33838/34005 +#Model 491.81s var:31054/31433 constraints:33830/34005 +#Model 496.75s var:31052/31433 constraints:33821/34005 +#Model 497.55s var:31048/31433 constraints:33821/34005 +#Model 499.77s var:31046/31433 constraints:33812/34005 +#Model 501.01s var:31040/31433 constraints:33810/34005 +#Model 501.12s var:31020/31433 constraints:33800/34005 +#Model 502.92s var:31018/31433 constraints:33800/34005 +#Model 505.16s var:31007/31433 constraints:33795/34005 +#Model 505.37s var:31000/31433 constraints:33793/34005 +#Model 505.46s var:30998/31433 constraints:33793/34005 +#Model 505.57s var:30995/31433 constraints:33793/34005 +#Model 508.05s var:30994/31433 constraints:33793/34005 +#Model 508.75s var:30992/31433 constraints:33784/34005 +#Model 513.07s var:30990/31433 constraints:33784/34005 +#Model 514.31s var:30489/31433 constraints:33659/34005 +#Model 514.64s var:30457/31433 constraints:33656/34005 +#Model 518.82s var:30455/31433 constraints:33656/34005 +#Model 519.00s var:30453/31433 constraints:33656/34005 +#Model 519.17s var:30447/31433 constraints:33656/34005 +#Model 519.61s var:30446/31433 constraints:33652/34005 +#Model 519.81s var:30435/31433 constraints:33650/34005 +#Model 521.92s var:30433/31433 constraints:33650/34005 +#Model 522.11s var:30431/31433 constraints:33648/34005 +#Model 529.25s var:30429/31433 constraints:33648/34005 +#Model 529.53s var:30428/31433 constraints:33648/34005 +#Model 531.82s var:30427/31433 constraints:33648/34005 +#Model 532.06s var:30413/31433 constraints:33646/34005 +#Model 532.85s var:30404/31433 constraints:33643/34005 +#Model 533.71s var:30402/31433 constraints:33643/34005 +#Model 536.76s var:30394/31433 constraints:33643/34005 +#Model 536.95s var:30393/31433 constraints:33643/34005 +#Model 539.02s var:30390/31433 constraints:33643/34005 +#Model 540.31s var:30381/31433 constraints:33633/34005 +#Model 547.87s var:30371/31433 constraints:33629/34005 +#Model 548.79s var:30370/31433 constraints:33627/34005 +#Model 550.22s var:30368/31433 constraints:33627/34005 +#Model 550.95s var:30346/31433 constraints:33622/34005 +#Model 551.19s var:30334/31433 constraints:33618/34005 +#Model 551.77s var:30061/31433 constraints:33576/34005 +#Model 552.11s var:30060/31433 constraints:33575/34005 +#Model 552.87s var:30002/31433 constraints:33572/34005 +#Model 552.96s var:29735/31433 constraints:33498/34005 +#Model 553.15s var:29688/31433 constraints:33489/34005 +#Model 553.25s var:29592/31433 constraints:33447/34005 +#Model 553.32s var:29580/31433 constraints:33418/34005 +#Model 553.43s var:29572/31433 constraints:33413/34005 +#Model 553.54s var:29565/31433 constraints:33413/34005 +#Model 554.43s var:29564/31433 constraints:33413/34005 +#Model 554.52s var:29563/31433 constraints:33413/34005 +#Model 554.62s var:29547/31433 constraints:33411/34005 +#Model 554.71s var:29546/31433 constraints:33411/34005 +#Model 554.86s var:29538/31433 constraints:33408/34005 +#Model 555.47s var:29511/31433 constraints:33405/34005 +#Model 557.40s var:29506/31433 constraints:33393/34005 +#Model 558.22s var:29489/31433 constraints:33387/34005 +#Model 558.56s var:29214/31433 constraints:33346/34005 compo:29213,1 +#Done 558.59s fs_random_no_lp + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 9.23m, 9.23m] 9.23m 0.00ns 9.23m 2 [ 20.83ms, 32.33s] 16.18s 16.16s 32.35s + 'feasibility_pump': 3191 [ 13.27ms, 271.63ms] 27.49ms 10.56ms 1.46m 3190 [282.20us, 6.04ms] 374.59us 111.38us 1.19s + 'fj': 354 [472.47ms, 2.32s] 901.78ms 302.27ms 5.32m 354 [100.73ms, 201.15ms] 107.02ms 11.29ms 37.89s + 'fs_random_no_lp': 1 [ 9.23m, 9.23m] 9.23m 0.00ns 9.23m 2 [ 10.83ms, 41.44s] 20.73s 20.71s 41.45s + 'max_lp': 1 [ 9.23m, 9.23m] 9.23m 0.00ns 9.23m 2 [ 26.36ms, 35.69s] 17.86s 17.83s 35.71s + 'no_lp': 1 [ 9.23m, 9.23m] 9.23m 0.00ns 9.23m 2 [ 10.83ms, 40.57s] 20.29s 20.28s 40.58s + 'quick_restart': 1 [ 9.23m, 9.23m] 9.23m 0.00ns 9.23m 2 [ 20.08ms, 32.92s] 16.47s 16.45s 32.94s + 'rins/rens': 3192 [ 23.22ms, 135.48ms] 43.63ms 10.76ms 2.32m 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 31'433 82'901 1'786'936 263 1'026'036 1'159'673 24'889'280 22'672'666 + 'fs_random_no_lp': 31'433 679'683 2'356'344 427 733'266 1'441'278 108'877'389 97'436'554 + 'max_lp': 31'433 16'319 3'133'520 107 2'291'085 2'419'904 19'592'665 22'581'257 + 'no_lp': 31'433 696'726 2'265'972 1'873 745'098 1'469'936 108'031'291 94'680'568 + 'quick_restart': 31'433 9'550 2'967'067 544 2'080'864 2'192'746 18'401'152 18'356'556 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 1'868 6'105 31'433 23'460 27'860 5'304 4'525 + 'fs_random_no_lp': 3'691 4'209 31'433 23'533 32'520 25'876 5'904 + 'max_lp': 3'294 5'225 31'433 22'914 23'918 2'959 951 + 'no_lp': 1'922 1'654 31'433 27'857 44'986 35'241 6'271 + 'quick_restart': 1'884 6'127 31'433 23'422 28'184 3'251 1'168 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 56'871 369'205 85'671 1'421'303 678'990 15'941 + 'fs_random_no_lp': 514'891 5'296'708 707'328 15'455'250 12'378'708 96'444 + 'max_lp': 10'199 43'688 9'598 190'236 0 5'079 + 'no_lp': 500'986 3'812'296 658'568 14'282'782 11'364'203 91'350 + 'quick_restart': 5'082 18'573 5'610 96'623 0 3'229 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 166'580 764'955 4 6'406 55'739 114'159 949 + 'fs_random_no_lp': 96'058 716'150 120 10'057 153'261 62'136 3'358 + 'max_lp': 263'915 967'499 3 3'516 20'907 188'926 294 + 'no_lp': 101'451 660'341 530 11'381 150'464 69'971 2'448 + 'quick_restart': 239'578 846'298 30 3'166 17'754 167'783 202 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 6'615 7'312 429 15'634 596 256 307 6'406 2'192 6'930 0 0 34'411 146'436 82'901 + 'fs_random_no_lp': 49'315 11'885 788 94'330 5'160 679 2'114 10'057 4'512 12'720 0 0 462'873 1'473'277 679'683 + 'max_lp': 2'872 4'535 427 5'006 191 50 73 3'516 1'499 2'321 0 0 0 21'327 16'319 + 'no_lp': 28'404 12'505 610 89'122 6'235 1'558 2'228 11'381 3'031 10'448 0 0 495'066 1'458'650 696'726 + 'quick_restart': 1'754 1'983 429 3'196 74 56 33 3'166 1'830 933 0 0 0 8'052 9'550 + +Lp stats Component Iterations AddedCuts OPTIMAL DUAL_F. DUAL_U. + 'default_lp': 107 1'128'732 26'190 511'345 0 0 + 'max_lp': 73 292'299 40'930 60'118 17'953 54 + 'quick_restart': 107 594'479 68'002 239'240 0 0 + +Lp dimension Final dimension of first component + 'default_lp': 282 rows, 1216 columns, 17121 entries + 'max_lp': 2637 rows, 8563 columns, 31001 entries + 'quick_restart': 121 rows, 1216 columns, 2255 entries + +Lp debug CutPropag CutEqPropag Adjust Overflow Bad BadScaling + 'default_lp': 0 432 0 0 168'854 0 + 'max_lp': 0 9 7 0 525'020 0 + 'quick_restart': 0 1'926 0 0 416'980 0 + +Lp pool Constraints Updates Simplif Merged Shortened Split Strengthened Cuts/Call + 'default_lp': 27'045 3'314 0 0 6 0 876 26'190/59'282 + 'max_lp': 12'600 3'151 0 0 314 0 626 40'930/81'908 + 'quick_restart': 48'857 10'748 0 0 0 0 2'531 68'002/147'511 + +Lp Cut default_lp max_lp quick_restart + CG_FF: 5'401 987 14'800 + CG_K: 1'163 127 3'406 + CG_KL: 399 42 1'190 + CG_R: 5'700 783 16'274 + Clique: - 1'501 - + MIR_1_FF: 2'980 2'457 8'643 + MIR_1_K: 297 105 839 + MIR_1_KL: 4 - 31 + MIR_1_R: 1'400 804 3'970 + MIR_1_RLT: - 1'782 - + MIR_2_FF: 1'631 2'804 2'878 + MIR_2_K: 44 28 113 + MIR_2_KL: 33 28 63 + MIR_2_R: 439 446 828 + MIR_3_FF: 670 1'266 780 + MIR_3_K: 24 12 48 + MIR_3_KL: 13 21 20 + MIR_3_R: 254 310 471 + MIR_4_FF: 387 527 359 + MIR_4_K: 15 10 35 + MIR_4_KL: 16 7 19 + MIR_4_R: 183 167 291 + MIR_5_FF: 261 241 188 + MIR_5_K: 5 8 19 + MIR_5_KL: 10 5 5 + MIR_5_R: 135 113 183 + MIR_6_FF: 163 125 117 + MIR_6_K: 12 1 11 + MIR_6_KL: 6 2 3 + MIR_6_R: 110 72 149 + ZERO_HALF_FF: 2'243 8'323 5'422 + ZERO_HALF_K: 91 255 261 + ZERO_HALF_KL: 22 54 107 + ZERO_HALF_R: 2'079 17'517 6'479 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 0/0 0% 5.00e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 26 7 127'660 680'123 0 0 5'758 3'022'165 + 'fj_restart_compound': 31 7 0 191'516 84'525 49'099 0 4'010'766 + 'fj_restart_compound_obj': 18 10 0 159'824 111'816 19'439 0 2'901'403 + 'fj_restart_compound_perturb': 29 9 0 203'358 107'547 45'041 0 3'966'517 + 'fj_restart_compound_perturb_obj': 14 8 0 121'869 97'341 10'731 0 2'270'938 + 'fj_restart_decay': 35 11 189'110 1'312'127 0 0 1'725 3'942'478 + 'fj_restart_decay_compound': 17 8 0 140'383 97'334 18'590 0 2'634'190 + 'fj_restart_decay_compound_obj': 14 4 0 98'327 47'283 22'913 0 1'902'677 + 'fj_restart_decay_compound_perturb': 10 7 0 100'552 83'984 6'541 0 1'764'338 + 'fj_restart_decay_compound_perturb_obj': 9 5 0 79'668 62'159 7'864 0 1'466'046 + 'fj_restart_decay_obj': 9 4 63'435 338'653 0 0 442 1'080'811 + 'fj_restart_decay_perturb': 19 9 134'011 699'807 0 0 806 2'183'939 + 'fj_restart_decay_perturb_obj': 21 10 153'079 776'445 0 0 1'097 2'498'796 + 'fj_restart_obj': 31 9 161'559 827'232 0 0 6'000 3'687'612 + 'fj_restart_perturb': 57 16 296'033 1'496'297 0 0 20'794 6'823'752 + 'fj_restart_perturb_obj': 14 9 151'949 401'520 0 0 5'696 2'195'259 + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 0 0 0 + 'fj solution hints': 125 0 125 + 'lp solutions': 225 3'192 221 + 'pump': 0 0 + +Improving bounds shared Num Sym + 'default_lp': 195 0 + 'fs_random_no_lp': 2'659 0 + 'max_lp': 52 0 + 'no_lp': 190 0 + 'quick_restart': 198 0 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 12'768 7'772 34'188 39'967 + 'fs_random_no_lp': 10'509 7'194 39'877 39'967 + 'max_lp': 11'200 7'425 39'967 39'967 + 'no_lp': 7'907 7'177 39'781 39'967 + 'quick_restart': 18'213 7'639 39'470 39'967 + +LRAT_status: NA +CpSolverResponse summary: +status: INFEASIBLE +objective: NA +best_bound: NA +integers: 29848 +booleans: 31433 +conflicts: 679683 +branches: 2356344 +propagations: 108877389 +integer_propagations: 97436554 +restarts: 427 +lp_iterations: 0 +walltime: 559.108 +usertime: 559.108 +deterministic_time: 222.189 +gap_integral: 0 + diff --git a/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nocol_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nocol_cpsat.txt new file mode 100644 index 0000000000..b9b6ec12c9 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nocol_cpsat.txt @@ -0,0 +1,297 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 1800 log_search_progress: true num_search_workers: 3 + +Initial satisfaction model '': (model_fingerprint: 0xdcd640ef5d03b5fb) +#Variables: 29'542 (27'363 primary variables) + - 29'542 Booleans in [0,1] +#kBoolAnd: 77 (#enforced: 77) (#literals: 154) +#kBoolXor: 25'779 +#kLinear1: 88 +#kLinear2: 5'068 (#enforced: 1'715) +#kLinear3: 1'638 +#kLinearN: 2'016 (#terms: 25'088) + +Starting presolve at 0.10s + 2.16e-02s 0.00e+00d [DetectDominanceRelations] + 2.00e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 2.35e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 4.25e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 3.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 88'920 nodes and 141'776 arcs. +[Symmetry] Symmetry computation done. time: 0.0941407 dtime: 0.0452301 +[SAT presolve] num removable Booleans: 1'638 / 27'445 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:6'468 literals:16'055 vars:4'133 one_side_vars:23 simple_definition:1'965 singleton_clauses:0 +[SAT presolve] [0.0011824s] clauses:6'468 literals:16'055 vars:4'133 one_side_vars:23 simple_definition:1'965 singleton_clauses:0 +[SAT presolve] [0.027527s] clauses:2'014 literals:13'748 vars:2'605 one_side_vars:1588 simple_definition:464 singleton_clauses:0 + 2.75e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=1 + 4.80e-01s 1.35e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=56'616 #fixed_bools=3 #equiv=182 #new_binary_clauses=3'376 + 2.28e-03s 1.29e-04d [MaxClique] + 1.82e-02s 0.00e+00d [DetectDominanceRelations] + 1.42e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=3 #num_dual_strengthening=2 + 1.05e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.60e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=54 + 3.28e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.92e-03s 7.23e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'016 + 1.88e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 8.09e-03s 9.41e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=4'024 #num_inclusions=163 + 7.83e-03s 1.01e-04d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=73 #num_clauses=1'774 #num_checked=1'774 + 1.44e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 4.72e-03s 1.21e-06d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=21 + 1.03e-03s 4.64e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 2.37e-02s 2.10e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 2.57e-03s 1.20e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'016 + 4.25e-03s 6.41e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 1.72e-02s 0.00e+00d [DetectDominanceRelations] + 8.03e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.35e-02s 0.00e+00d [DetectDominanceRelations] + 8.91e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 5.22e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 3.08e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 82'484 nodes and 133'227 arcs. +[Symmetry] Symmetry computation done. time: 0.0601267 dtime: 0.0264297 +[SAT presolve] num removable Booleans: 109 / 25'731 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:1'846 literals:12'963 vars:2'597 one_side_vars:1584 simple_definition:494 singleton_clauses:0 +[SAT presolve] [0.0017689s] clauses:1'846 literals:12'963 vars:2'597 one_side_vars:1584 simple_definition:494 singleton_clauses:0 +[SAT presolve] [0.0060954s] clauses:1'846 literals:12'963 vars:2'597 one_side_vars:1584 simple_definition:494 singleton_clauses:0 + 2.88e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.47e-01s 1.25e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=56'613 #fixed_bools=1 #equiv=35 #new_binary_clauses=2'266 + 3.49e-03s 1.09e-04d [MaxClique] Merged 72 constraints with 144 literals into 71 constraints with 142 literals + 2.09e-02s 0.00e+00d [DetectDominanceRelations] + 8.98e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.43e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.70e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 3.02e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 4.92e-03s 7.23e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'016 + 1.63e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 2.70e-02s 9.05e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=3'859 + 1.65e-02s 1.01e-04d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=69 #num_clauses=1'774 #num_checked=1'774 + 3.38e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 4.20e-03s 1.16e-06d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=25 + 7.63e-04s 5.12e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 1.63e-02s 2.10e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 3.21e-03s 1.20e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'016 + 4.68e-03s 6.41e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.33e-02s 0.00e+00d [DetectDominanceRelations] + 9.78e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 2.03e-02s 0.00e+00d [DetectDominanceRelations] + 1.02e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 4.57e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 2.55e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 82'418 nodes and 133'088 arcs. +[Symmetry] Symmetry computation done. time: 0.071574 dtime: 0.027327 +[SAT presolve] num removable Booleans: 109 / 25'695 +[SAT presolve] num trivial clauses: 0 +[SAT presolve] [0s] clauses:1'843 literals:12'957 vars:2'590 one_side_vars:1579 simple_definition:489 singleton_clauses:0 +[SAT presolve] [0.0011321s] clauses:1'843 literals:12'957 vars:2'590 one_side_vars:1579 simple_definition:489 singleton_clauses:0 +[SAT presolve] [0.0045916s] clauses:1'843 literals:12'957 vars:2'590 one_side_vars:1579 simple_definition:489 singleton_clauses:0 + 3.55e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 5.29e-01s 1.22e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=56'612 #equiv=4 #new_binary_clauses=2'070 + 3.00e-03s 1.00e-04d [MaxClique] Merged 69 constraints with 138 literals into 67 constraints with 134 literals + 2.33e-02s 0.00e+00d [DetectDominanceRelations] + 9.99e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 1.65e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 2.79e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] #duplicates=2 + 3.70e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 6.07e-03s 7.23e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'015 + 1.37e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 9.00e-03s 9.05e-05d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=3'854 + 1.52e-02s 1.00e-04d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] #num_amos=65 #num_clauses=1'774 #num_checked=1'774 + 3.25e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 5.28e-03s 8.45e-07d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] #num_tested_pairs=16 + 1.18e-03s 5.05e-05d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 2.14e-02s 2.10e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 4.15e-03s 1.20e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'015 + 6.41e-03s 6.41e-05d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.68e-02s 0.00e+00d [DetectDominanceRelations] + 1.02e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 1.90e-03s 0.00e+00d [MergeNoOverlap] + 2.78e-03s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 1319 affine relations were detected. + - rule 'TODO bool_xor: remove constraint' was applied 87 times. + - rule 'TODO dual: only one blocking constraint?' was applied 34'987 times. + - rule 'affine: new relation' was applied 1'319 times. + - rule 'at_most_one: removed literals' was applied 3 times. + - rule 'at_most_one: satisfied' was applied 1 time. + - rule 'at_most_one: size one' was applied 3 times. + - rule 'at_most_one: transformed into max clique' was applied 2 times. + - rule 'bool_and: x => x' was applied 1 time. + - rule 'bool_or: always true' was applied 77 times. + - rule 'bool_or: implications' was applied 3'352 times. + - rule 'bool_or: removed enforcement literal' was applied 1'558 times. + - rule 'bool_xor: always true' was applied 158 times. + - rule 'bool_xor: one active literal' was applied 1'069 times. + - rule 'bool_xor: remove false literal' was applied 3'188 times. + - rule 'bool_xor: two active literals' was applied 1'019 times. + - rule 'dual: enforced equivalence' was applied 1 time. + - rule 'duplicate: removed constraint' was applied 56 times. + - rule 'duplicate: removed enforced constraint' was applied 1 time. + - rule 'enforcement: always false' was applied 77 times. + - rule 'enforcement: true literal' was applied 73 times. + - rule 'linear1: x in domain' was applied 86 times. + - rule 'linear2: convert ax + by != cte to clauses' was applied 4'984 times. + - rule 'linear: always true' was applied 86 times. + - rule 'linear: fixed or dup variables' was applied 1'072 times. + - rule 'linear: negative clause' was applied 1'484 times. + - rule 'linear: positive clause' was applied 77 times. + - rule 'linear: remapped using affine relations' was applied 420 times. + - rule 'presolve: 1236 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 3 times. + - rule 'probing: bool_or reduced to implication' was applied 4 times. + - rule 'probing: simplified clauses' was applied 18 times. + - rule 'setppc: removed dominated constraints' was applied 163 times. + +Presolved satisfaction model '': (model_fingerprint: 0x4718cb189117fe7d) +#Variables: 25'536 (23'583 primary variables) + - 25'536 Booleans in [0,1] +#kBoolAnd: 65 (#enforced: 65) (#literals: 130) +#kBoolOr: 1'774 (#literals: 12'819) +#kBoolXor: 23'479 +#kLinearN: 2'015 (#terms: 24'081) +[Symmetry] Graph for symmetry has 78'403 nodes and 133'066 arcs. +[Symmetry] Symmetry computation done. time: 0.0487213 dtime: 0.027019 + +Preloading model. +#Model 4.17s var:25536/25536 constraints:27333/27333 + +Starting search at 4.17s with 3 workers. +2 full problem subsolvers: [default_lp, no_lp] +1 first solution subsolver: [fj] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + +#Model 20.84s var:25535/25536 constraints:27333/27333 +#Model 22.12s var:25534/25536 constraints:27333/27333 +#Model 25.23s var:25533/25536 constraints:27330/27333 +#Model 66.51s var:25532/25536 constraints:27328/27333 +#Model 102.26s var:25530/25536 constraints:27324/27333 +#Model 104.49s var:25529/25536 constraints:27324/27333 +#Model 124.37s var:25528/25536 constraints:27324/27333 +#Model 325.11s var:25524/25536 constraints:27321/27333 +#Model 678.88s var:25523/25536 constraints:27321/27333 +#Model 1212.02s var:25521/25536 constraints:27317/27333 +#Model 1294.95s var:25514/25536 constraints:27289/27333 +#Model 1308.90s var:25507/25536 constraints:27285/27333 +#Model 1310.70s var:25493/25536 constraints:27276/27333 +#Model 1313.06s var:25490/25536 constraints:27274/27333 +#Model 1314.81s var:25463/25536 constraints:27252/27333 +#Model 1316.07s var:25460/25536 constraints:27250/27333 +#Model 1317.23s var:25456/25536 constraints:27248/27333 +#Model 1317.96s var:25451/25536 constraints:27246/27333 +#Model 1318.63s var:25447/25536 constraints:27244/27333 +#Model 1318.91s var:25423/25536 constraints:27225/27333 +#Done 1318.92s no_lp + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 21.91m, 21.91m] 21.91m 0.00ns 21.91m 2 [ 9.94ms, 2.06m] 1.03m 1.03m 2.06m + 'feasibility_pump': 6228 [ 4.94ms, 206.27ms] 10.27ms 6.59ms 1.07m 6227 [204.94us, 389.92us] 204.97us 2.34us 1.28s + 'fj': 837 [233.13ms, 2.98s] 744.43ms 301.17ms 10.38m 837 [ 51.69ms, 109.13ms] 102.06ms 3.34ms 1.42m + 'no_lp': 1 [ 21.91m, 21.91m] 21.91m 0.00ns 21.91m 2 [ 9.68ms, 3.13m] 1.56m 1.56m 3.13m + 'rins/rens': 257 [ 79.29ms, 7.48s] 2.44s 1.91s 10.43m 161 [214.89us, 100.18ms] 81.51ms 35.88ms 13.12s + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 25'536 1'507'569 4'572'352 5'203 1'149'700 2'684'639 118'358'640 82'604'354 + 'no_lp': 25'536 2'250'709 6'235'989 7'411 1'577'896 3'859'630 190'230'301 140'403'919 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 94 486 25'536 24'956 3'440 97'411 13'930 + 'no_lp': 291 486 25'536 24'759 3'338 94'293 6'407 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 1'094'925 10'685'789 1'132'138 34'700'538 28'708'893 189'412 + 'no_lp': 1'685'758 17'549'587 3'102'094 51'005'796 42'360'938 311'412 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 179'325 1'506'265 44 10'422 155'614 105'009 2'796 + 'no_lp': 212'206 1'815'676 15 15'421 238'424 110'962 4'828 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 57'605 404 80 184'692 10'850 5'708 4'720 10'422 952 15'734 0 0 1'119'269 3'393'611 1'507'569 + 'no_lp': 75'950 987 179 303'193 14'676 10'349 8'219 15'421 4'723 66'246 0 0 1'658'049 5'213'545 2'250'709 + +Lp stats Component Iterations AddedCuts OPTIMAL DUAL_F. DUAL_U. + 'default_lp': 62 2'039'649 2'230 2'002'907 0 0 + +Lp dimension Final dimension of first component + 'default_lp': 2 rows, 27 columns, 30 entries + +Lp debug CutPropag CutEqPropag Adjust Overflow Bad BadScaling + 'default_lp': 0 2 0 0 2'420 0 + +Lp pool Constraints Updates Simplif Merged Shortened Split Strengthened Cuts/Call + 'default_lp': 2'354 121 0 0 0 0 28 2'230/20'210 + +Lp Cut default_lp + CG_FF: 691 + CG_K: 1 + CG_KL: 1 + CG_R: 10 + MIR_1_FF: 61 + MIR_1_K: 15 + MIR_1_R: 37 + MIR_2_FF: 1'382 + MIR_2_KL: 5 + MIR_2_R: 12 + MIR_3_FF: 2 + MIR_3_R: 1 + ZERO_HALF_FF: 1 + ZERO_HALF_R: 11 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 257/257 52% 9.91e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 30 10 110'204 858'006 0 0 2'137 3'271'075 + 'fj_restart_compound': 33 12 0 266'494 123'927 71'128 0 4'921'011 + 'fj_restart_compound_obj': 64 20 0 494'061 204'877 144'272 0 9'312'478 + 'fj_restart_compound_perturb': 43 19 0 377'943 194'040 91'799 0 6'666'585 + 'fj_restart_compound_perturb_obj': 65 16 0 491'581 165'416 162'847 0 9'058'740 + 'fj_restart_decay': 22 10 108'450 831'011 0 0 455 2'254'368 + 'fj_restart_decay_compound': 110 21 0 795'817 218'567 288'262 0 14'933'485 + 'fj_restart_decay_compound_obj': 47 21 0 414'123 214'859 99'243 0 7'384'418 + 'fj_restart_decay_compound_perturb': 48 17 0 388'854 175'508 106'299 0 7'129'003 + 'fj_restart_decay_compound_perturb_obj': 67 22 0 537'840 226'607 154'966 0 9'869'365 + 'fj_restart_decay_obj': 29 12 131'774 1'095'016 0 0 558 2'917'905 + 'fj_restart_decay_perturb': 72 14 176'652 2'686'059 0 0 1'515 6'687'148 + 'fj_restart_decay_perturb_obj': 55 16 183'782 2'060'602 0 0 1'089 5'285'882 + 'fj_restart_obj': 19 13 132'196 563'120 0 0 601 2'283'946 + 'fj_restart_perturb': 58 23 242'837 1'663'454 0 0 2'822 6'426'912 + 'fj_restart_perturb_obj': 75 21 230'716 2'090'905 0 0 5'393 7'981'107 + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 0 0 0 + 'fj solution hints': 259 0 259 + 'lp solutions': 0 0 0 + 'pump': 6'227 257 + +Improving bounds shared Num Sym + 'default_lp': 16 0 + 'no_lp': 166 0 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 12'632 14'358 2'364 2'380 + 'no_lp': 18'878 9'222 2'380 2'380 + +LRAT_status: NA +CpSolverResponse summary: +status: INFEASIBLE +objective: NA +best_bound: NA +integers: 23927 +booleans: 25536 +conflicts: 2250709 +branches: 6235989 +propagations: 190230301 +integer_propagations: 140403919 +restarts: 7411 +lp_iterations: 0 +walltime: 1319.14 +usertime: 1319.14 +deterministic_time: 411.21 +gap_integral: 0 + diff --git a/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nosb_cpsat.txt b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nosb_cpsat.txt new file mode 100644 index 0000000000..1c22a822a9 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/logs/sat_sb_k2_c2_nosb_cpsat.txt @@ -0,0 +1,150 @@ + +Starting CP-SAT solver v9.15.6755 +Parameters: max_time_in_seconds: 1800 log_search_progress: true num_search_workers: 3 + +Initial satisfaction model '': (model_fingerprint: 0x46511a00894224bc) +#Variables: 33'792 (31'296 primary variables) + - 33'792 Booleans in [0,1] +#kBoolXor: 31'744 +#kLinearN: 2'496 (#terms: 32'768) + +Starting presolve at 0.11s + 1.75e-02s 0.00e+00d [DetectDominanceRelations] + 1.63e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 2.24e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ExtractEncodingFromLinear] + 4.80e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateColumns] + 3.04e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] +[Symmetry] Graph for symmetry has 100'800 nodes and 160'768 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 2.57942 dtime: 1.00055 +[Symmetry] #generators: 47, average support size: 3431.4 +[Symmetry] 1404 orbits on 28816 variables with sizes: 1024,1024,512,512,448,448,448,448,128,128,... +[Symmetry] Found orbitope of size 904 x 2 + 4.07e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 6.12e-01s 1.04e-02d [operations_research::sat::CpModelPresolver::Probe] #probed=67'584 + 9.80e-04s 0.00e+00d [MaxClique] + 1.92e-02s 0.00e+00d [DetectDominanceRelations] + 1.72e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 + 1.52e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessAtMostOneAndLinear] + 3.98e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraints] + 4.20e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements] + 6.30e-03s 9.83e-05d [operations_research::sat::CpModelPresolver::DetectDominatedLinearConstraints] #relevant_constraints=2'496 + 1.33e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectDifferentVariables] + 1.82e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::ProcessSetPPC] #relevant_constraints=2'496 + 1.09e-02s 0.00e+00d [operations_research::sat::CpModelPresolver::TransformClausesToExactlyOne] + 1.35e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::DetectEncodedComplexDomains] + 4.02e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::FindAlmostIdenticalLinearConstraints] + 2.47e-04s 0.00e+00d [operations_research::sat::CpModelPresolver::FindBigAtMostOneAndLinearOverlap] + 1.86e-02s 2.98e-03d [operations_research::sat::CpModelPresolver::FindBigVerticalLinearOverlap] + 3.67e-03s 1.64e-04d [operations_research::sat::CpModelPresolver::FindBigHorizontalLinearOverlap] #linears=2'496 + 1.93e-03s 0.00e+00d [operations_research::sat::CpModelPresolver::MergeClauses] + 2.77e-02s 0.00e+00d [DetectDominanceRelations] + 1.17e-01s 0.00e+00d [operations_research::sat::CpModelPresolver::PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1 + 9.90e-04s 0.00e+00d [MergeNoOverlap] + 1.42e-03s 0.00e+00d [MergeNoOverlap2D] + +Presolve summary: + - 0 affine relations were detected. + - rule 'TODO dual: only one blocking constraint?' was applied 6'144 times. + - rule 'presolve: 0 unused variables removed.' was applied 1 time. + - rule 'presolve: iteration' was applied 1 time. + +Presolved satisfaction model '': (model_fingerprint: 0x46511a00894224bc) +#Variables: 33'792 (31'296 primary variables) + - 33'792 Booleans in [0,1] +#kBoolXor: 31'744 +#kLinearN: 2'496 (#terms: 32'768) +[Symmetry] Graph for symmetry has 100'800 nodes and 160'768 arcs. +[Symmetry] Time limit reached: Some automorphisms were found, but probably not all. +[Symmetry] Symmetry computation done. time: 3.24533 dtime: 1.00055 +[Symmetry] #generators: 47, average support size: 3431.4 +[Symmetry] 1404 orbits on 28816 variables with sizes: 1024,1024,512,512,448,448,448,448,128,128,... +[Symmetry] Found orbitope of size 904 x 2 + +Preloading model. +#Model 7.94s var:33792/33792 constraints:34240/34240 + +Starting search at 7.94s with 3 workers. +2 full problem subsolvers: [default_lp, no_lp] +1 first solution subsolver: [fj] +2 interleaved subsolvers: [feasibility_pump, rins/rens] +2 helper subsolvers: [neighborhood_helper, synchronization_agent] + + +Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime + 'default_lp': 1 [ 29.87m, 29.87m] 29.87m 0.00ns 29.87m 2 [ 9.15ms, 14.37m] 7.19m 7.19m 14.37m + 'feasibility_pump': 8402 [ 1.68ms, 290.89ms] 13.06ms 8.48ms 1.83m 8379 [211.58us, 211.58us] 211.58us 0.00ns 1.77s + 'fj': 1348 [117.81ms, 2.33s] 623.28ms 280.71ms 14.00m 1348 [ 30.99ms, 110.67ms] 102.42ms 3.84ms 2.30m + 'no_lp': 1 [ 29.87m, 29.87m] 29.87m 0.00ns 29.87m 2 [ 9.15ms, 11.06m] 5.53m 5.53m 11.06m + 'rins/rens': 311 [ 77.25ms, 10.85s] 2.70s 2.33s 14.01m 189 [ 2.97ms, 100.41ms] 89.10ms 25.69ms 16.84s + +Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag + 'default_lp': 33'792 13'015'659 35'371'469 7'180 7'429'289 20'545'668 437'660'595 152'969'672 + 'no_lp': 33'792 9'905'128 29'871'208 12'729 6'188'928 16'211'913 355'660'170 144'103'345 + +SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses + 'default_lp': 0 0 33'792 33'792 0 151'668 14'319 + 'no_lp': 0 0 33'792 33'792 0 214'850 14'272 + +SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed + 'default_lp': 8'364'978 90'852'657 0 437'891'730 384'900'394 1'545'684 + 'no_lp': 5'928'380 60'641'479 0 301'101'699 261'318'842 1'268'080 + +Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts + 'default_lp': 1'631'118 12'979'732 0 38'058 455'352 1'160'288 1'323 + 'no_lp': 1'378'939 11'077'654 0 42'169 539'860 1'058'394 1'742 + +Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts + 'default_lp': 0 0 0 1'513'221 134'370 27'170 32'463 38'058 0 26'227 0 0 11'116'681 33'284'288 13'015'659 + 'no_lp': 0 0 0 1'229'230 108'988 22'069 38'850 42'169 0 20'418 0 0 8'240'288 24'163'569 9'905'128 + +LNS stats Improv/Calls Closed Difficulty TimeLimit + 'rins/rens': 311/311 52% 9.88e-01 0.10 + +LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed + 'fj_restart': 61 21 314'983 1'642'545 0 0 549 6'579'601 + 'fj_restart_compound': 57 19 0 321'725 214'854 53'281 0 8'568'366 + 'fj_restart_compound_obj': 137 26 0 623'489 295'566 163'531 0 18'357'940 + 'fj_restart_compound_perturb': 143 35 0 709'014 394'355 150'969 0 19'510'325 + 'fj_restart_compound_perturb_obj': 171 31 0 781'581 367'461 204'065 0 22'630'732 + 'fj_restart_decay': 82 22 363'215 2'914'116 0 0 549 7'802'685 + 'fj_restart_decay_compound': 51 15 0 275'093 175'477 49'625 0 7'535'793 + 'fj_restart_decay_compound_obj': 94 31 0 517'341 335'534 90'034 0 13'840'811 + 'fj_restart_decay_compound_perturb': 89 25 0 485'365 288'126 93'060 0 12'750'788 + 'fj_restart_decay_compound_perturb_obj': 43 27 0 353'164 291'586 26'725 0 7'478'292 + 'fj_restart_decay_obj': 71 24 382'329 2'535'119 0 0 472 6'982'285 + 'fj_restart_decay_perturb': 73 25 385'771 2'608'787 0 0 477 7'218'544 + 'fj_restart_decay_perturb_obj': 37 22 314'326 1'320'497 0 0 237 4'057'513 + 'fj_restart_obj': 96 32 480'365 2'584'380 0 0 865 10'331'194 + 'fj_restart_perturb': 40 18 256'168 1'089'249 0 0 352 4'452'256 + 'fj_restart_perturb_obj': 103 24 370'867 2'718'195 0 0 978 10'642'885 + +Solution repositories Added Queried Synchro + 'alternative_path': 0 0 0 + 'best_solutions': 0 0 0 + 'fj solution hints': 389 0 389 + 'lp solutions': 0 0 0 + 'pump': 8'401 311 + +Clauses shared #Exported #Imported #BinaryRead #BinaryTotal + 'default_lp': 30'442 40'721 0 0 + 'no_lp': 40'580 26'313 0 0 + +LRAT_status: NA +CpSolverResponse summary: +status: UNKNOWN +objective: NA +best_bound: NA +integers: 32768 +booleans: 33792 +conflicts: 9905128 +branches: 29871208 +propagations: 355660170 +integer_propagations: 144103345 +restarts: 12729 +lp_iterations: 0 +walltime: 1800.25 +usertime: 1800.25 +deterministic_time: 1682.54 +gap_integral: 0 + diff --git a/research/line-system-510-signing-nonexistence/tools/delsarte_lp.py b/research/line-system-510-signing-nonexistence/tools/delsarte_lp.py new file mode 100644 index 0000000000..3a41fb03d6 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/tools/delsarte_lp.py @@ -0,0 +1,149 @@ +"""Delsarte LP checks for idea 3: 510 lines in R^30 with |cos| in {0, 1/4}. + +Exact rational arithmetic (fractions.Fraction) for every reported number; +scipy's LP is used only to find the optimum, which is then re-derived exactly. + +Part A: the fixed distance distribution forced by the W(7,2) doubled pattern + (per line: 253 orthogonal lines, 256 lines at |cos| = 1/4) against + every Gegenbauer inequality of even degree 2..KMAX. +Part B: the plain LP bound max N for lines in R^n with angles {90, arccos a}. +Part C: same LP with the extra tight-frame equality (degree 2 = 0), which every + saturated system satisfies (README section 4, equality case). + +Run: py -3.12 delsarte_lp.py (seconds). Appends to progress.log. +""" +from fractions import Fraction as Fr +import datetime +import json +import os +import sys + +import numpy as np +from scipy.optimize import linprog + +HERE = os.path.dirname(os.path.abspath(__file__)) +LOG = os.path.join(HERE, "progress.log") +KMAX = 60 + + +def log(msg): + line = f"[{datetime.datetime.now():%Y-%m-%d %H:%M:%S}] {msg}" + print(line) + with open(LOG, "a", encoding="utf-8") as f: + f.write(line + "\n") + + +def gegenbauer_normalised(n, kmax, t): + """Q_k(t) for k = 0..kmax on S^{n-1}, normalised Q_k(1) = 1, exact.""" + lam = Fr(n - 2, 2) + c = [Fr(1), 2 * lam * t] + c1 = [Fr(1), 2 * lam] + for k in range(1, kmax): + c.append((2 * (k + lam) * t * c[k] - (k + 2 * lam - 1) * c[k - 1]) / (k + 1)) + c1.append((2 * (k + lam) * c1[k] - (k + 2 * lam - 1) * c1[k - 1]) / (k + 1)) + return [c[k] / c1[k] for k in range(kmax + 1)] + + +def part_a(n, a, n_orth, n_ang): + q0 = gegenbauer_normalised(n, KMAX, Fr(0)) + qa = gegenbauer_normalised(n, KMAX, a) + rows = [] + worst = None + for k in range(2, KMAX + 1, 2): + val = 1 + n_orth * q0[k] + n_ang * qa[k] + rows.append((k, val)) + if worst is None or val < worst[1]: + worst = (k, val) + return rows, worst + + +def lp_bound(n, a, tight_frame): + q0 = gegenbauer_normalised(n, KMAX, Fr(0)) + qa = gegenbauer_normalised(n, KMAX, a) + ks = list(range(2, KMAX + 1, 2)) + # variables x = (A0, Aa) >= 0 ; maximise A0 + Aa + # constraint per k: -(q0 A0 + qa Aa) <= 1 + A_ub, b_ub, A_eq, b_eq = [], [], [], [] + for k in ks: + if tight_frame and k == 2: + A_eq.append([float(q0[k]), float(qa[k])]) + b_eq.append(-1.0) + else: + A_ub.append([-float(q0[k]), -float(qa[k])]) + b_ub.append(1.0) + res = linprog([-1, -1], A_ub=A_ub, b_ub=b_ub, + A_eq=A_eq or None, b_eq=b_eq or None, + bounds=[(0, None), (0, None)], method="highs") + if res.status != 0: + return None + # exact re-derivation: the optimum of a 2-variable LP is a vertex where + # two constraints are tight (or one constraint and a bound). + cand_rows = [(k, q0[k], qa[k], "eq" if (tight_frame and k == 2) else "ub") for k in ks] + best = None + lines = [(r[1], r[2]) for r in cand_rows] + [("A0=0",), ("Aa=0",)] + + def feasible(A0, Aa): + if A0 < 0 or Aa < 0: + return False + for k, c0, ca, kind in cand_rows: + v = 1 + c0 * A0 + ca * Aa + if kind == "eq" and v != 0: + return False + if v < 0: + return False + return True + + def solve2(r1, r2): + # each r: (c0, ca) meaning 1 + c0 A0 + ca Aa = 0, or bound + def eq(r): + if r == ("A0=0",): + return (Fr(1), Fr(0), Fr(0)) + if r == ("Aa=0",): + return (Fr(0), Fr(1), Fr(0)) + return (r[0], r[1], Fr(-1)) + a1, b1, c1 = eq(r1) + a2, b2, c2 = eq(r2) + det = a1 * b2 - a2 * b1 + if det == 0: + return None + return ((c1 * b2 - c2 * b1) / det, (a1 * c2 - a2 * c1) / det) + + # restrict to rows near the float optimum to keep it quick + for i in range(len(lines)): + for j in range(i + 1, len(lines)): + p = solve2(lines[i], lines[j]) + if p is None or not feasible(*p): + continue + val = 1 + p[0] + p[1] + if best is None or val > best[0]: + best = (val, p) + return best, -res.fun + 1 + + +def main(): + n, a = 30, Fr(1, 4) + log("=== delsarte_lp.py start: n=30, |cos| in {0, 1/4}, even degrees 2..%d ===" % KMAX) + + rows, worst = part_a(n, a, 253, 256) + log("Part A (fixed distribution 1 + 253 + 256 = 510):") + for k, v in rows[:8]: + log(f" k={k:2d} 1+253Q_k(0)+256Q_k(1/4) = {v} (~{float(v):.6g})") + log(f" worst over k<= {KMAX}: k={worst[0]} value {float(worst[1]):.6g} -> " + + ("ALL >= 0: LP does not kill the object" if worst[1] >= 0 else "NEGATIVE: object does not exist")) + + out = {"part_a": {str(k): str(v) for k, v in rows}} + for tf in (False, True): + best, fl = lp_bound(n, a, tf) + tag = "C (with tight-frame equality)" if tf else "B (plain LP)" + log(f"Part {tag}: N <= {best[0]} = {float(best[0]):.4f} (float LP {fl:.4f}); vertex A0={best[1][0]}, A1/4={best[1][1]}") + out["part_" + ("c" if tf else "b")] = {"N_max": str(best[0]), "A0": str(best[1][0]), "Aa": str(best[1][1])} + + # absolute / relative bounds for comparison + log(f" absolute bound (3 inner products 0, +-a on lines): C(n+2,3)={n*(n+1)*(n+2)//6}") + with open(os.path.join(HERE, "delsarte_lp_result.json"), "w", encoding="utf-8") as f: + json.dump(out, f, indent=1) + log("=== delsarte_lp.py done; results in delsarte_lp_result.json ===") + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/line-system-510-signing-nonexistence/tools/frame_reduction.py b/research/line-system-510-signing-nonexistence/tools/frame_reduction.py new file mode 100644 index 0000000000..ce1ac3e376 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/tools/frame_reduction.py @@ -0,0 +1,188 @@ +"""Idea 3: exact checks of the frame reduction + instance sizes (no solving). + +Object O(k'): saturated uniform system on W(2k'-1,2), multiplicity m = 2^(5-k'), +unit lines, |cos| in {0, 1/4}, N = m(4^k'-1) lines in R^T, T = m(2^k'-1). +k'=4 is the 510-line object of line-system-saturation section 11.1; k'=3,2,1 are its +descendants under Proposition D1 (descent at one label merges q, q+p: m doubles). + +Frame reduction (argument in REPORT.md section 2): by saturation the T lines +with labels in a fixed generator L are pairwise orthogonal, an orthonormal +frame e_1..e_T; every other unit line has u.e_c in {0, +-1/4} and norm 1, so +u = (1/4) * (+-1 on exactly 16 frame coordinates). Its support is fixed by the +labels: the m twins of each x in L with b(x,p) = 1. This script checks the +combinatorial facts exactly and counts the sizes of two encodings: + E1 = direct +-1 signing S of the blown-up non-collinearity graph, S^2 = 60S+256I + E2 = frame-reduced sign bits with XOR auxiliaries (what OPB file would hold) +With --write-opb K it writes the E2 instance for k' = K as an OPB file (it does +NOT run any solver). + +Run: py -3.12 frame_reduction.py [--write-opb 2] +""" +import datetime +import itertools +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +LOG = os.path.join(HERE, "progress.log") + + +def log(msg): + line = f"[{datetime.datetime.now():%Y-%m-%d %H:%M:%S}] {msg}" + print(line) + with open(LOG, "a", encoding="utf-8") as f: + f.write(line + "\n") + + +def b(p, q, k): + s = 0 + for i in range(k): + s ^= ((p >> (2 * i)) & 1) & ((q >> (2 * i + 1)) & 1) + s ^= ((p >> (2 * i + 1)) & 1) & ((q >> (2 * i)) & 1) + return s + + +def build(k): + m = 2 ** (5 - k) + pts = list(range(1, 4 ** k)) + # generator L = span of the even coordinates (totally isotropic, dim k) + L = [p for p in pts if all(((p >> (2 * i + 1)) & 1) == 0 for i in range(k))] + assert len(L) == 2 ** k - 1 + Lset = set(L) + coords = [(x, j) for x in L for j in range(m)] # frame lines + cidx = {c: i for i, c in enumerate(coords)} + T = len(coords) + others = [p for p in pts if p not in Lset] + supp = {} + for p in others: + s = [cidx[(x, j)] for x in L if b(x, p, k) for j in range(m)] + supp[p] = s + return m, pts, L, others, supp, T + + +def check(k): + m, pts, L, others, supp, T = build(k) + N = m * len(pts) + assert T == m * (2 ** k - 1) and N == m * (4 ** k - 1) + sizes = {len(s) for s in supp.values()} + # classes by functional f_p = b(., p)|_L + cls = {} + for p in others: + key = tuple(b(x, p, k) for x in L) + cls.setdefault(key, []).append(p) + ok_class = all(len(v) == 2 ** k for v in cls.values()) and len(cls) == 2 ** k - 1 + # inside a class: collinear iff f(x) = f(y) where p = p0 + x + ok_inside = True + for key, members in cls.items(): + for p, q in itertools.combinations(members, 2): + same_supp = supp[p] == supp[q] + ok_inside &= same_supp + # within each class the two collinearity groups have 16 vectors each + ok_groups = True + for key, members in cls.items(): + p0 = members[0] + g0 = [q for q in members if q == p0 or b(p0, q, k) == 0] + ok_groups &= (len(g0) * m == 16) and all(b(x, y, k) == 0 for x, y in itertools.combinations(g0, 2)) + inter = set() + keys = list(cls) + for k1, k2 in itertools.combinations(keys, 2): + inter.add(len(set(supp[cls[k1][0]]) & set(supp[cls[k2][0]]))) + # per-line distance distribution + p = pts[0] + orth = (m - 1) + m * sum(1 for q in pts if q != p and b(p, q, k) == 0) + ang = m * sum(1 for q in pts if b(p, q, k) == 1) + log(f"k'={k}: m={m}, N={N} lines in R^{T}; non-frame lines {len(others)*m}; " + f"support sizes {sorted(sizes)}; classes {len(cls)} x {2**k} points " + f"(ok={ok_class}, same support inside class={ok_inside}, Hadamard-16 groups={ok_groups}); " + f"cross-class support intersections {sorted(inter)}; per line: {orth} orthogonal + {ang} at 1/4") + # sizes of encodings + nv = len(others) * m + pairs_in = len(cls) * (2 ** k * m) * (2 ** k * m - 1) // 2 + pairs_x = (len(cls) * (len(cls) - 1) // 2) * (2 ** k * m) ** 2 + ov = 8 if k >= 2 else 0 + e2_bits = nv * 16 + e2_xor = pairs_in * 16 + pairs_x * ov + adj_edges = N * ang // 2 + common = ang // 2 # common neighbours of an adjacent pair (k'=4: 128) + e1_pairs = N * (N - 1) // 2 + log(f" E1 (direct signing): {adj_edges} edge-sign bits, {e1_pairs} pair constraints, " + f"~{adj_edges*common + (e1_pairs-adj_edges)*ang:.3g} product terms") + log(f" E2 (frame-reduced): {e2_bits} sign bits, {pairs_in} in-class + {pairs_x} cross-class pair constraints, " + f"{e2_xor} XOR auxiliaries") + return dict(m=m, N=N, T=T, cls=cls, supp=supp, L=L, others=others, + pairs=(pairs_in, pairs_x), e2=(e2_bits, e2_xor)) + + +def write_opb(k, path): + """E2 for k': x[v,c] sign bit of line v at frame coordinate c (value (-1)^x). + Pair constraint for lines v, w with common support I: + sum_{c in I} y_c = |I|/2 (orthogonal: twins, collinear labels) + sum_{c in I} y_c = |I|/2 - 2 + 4z (|cos| = 1/4: non-collinear labels) + with y_c = x[v,c] XOR x[w,c] (4 linear inequalities each). + Gauge: x = 0 on a spanning forest of the line/coordinate incidence graph.""" + m, pts, L, others, supp, T = build(k) + lines = [(p, j) for p in others for j in range(m)] + var = {} + + def v(name): + if name not in var: + var[name] = len(var) + 1 + return var[name] + + cons = [] + # gauge by union-find + parent = {} + + def find(a): + while parent.setdefault(a, a) != a: + parent[a] = parent[parent[a]] + a = parent[a] + return a + + fixed = 0 + for li, (p, j) in enumerate(lines): + for c in supp[p]: + ra, rb = find(("l", li)), find(("c", c)) + if ra != rb: + parent[ra] = rb + cons.append(f"+1 x{v(('x', li, c))} = 0 ;") + fixed += 1 + for (i1, (p, j)), (i2, (q, jj)) in itertools.combinations(enumerate(lines), 2): + I = sorted(set(supp[p]) & set(supp[q])) + if not I: + continue + ys = [] + for c in I: + a, bb, y = v(("x", i1, c)), v(("x", i2, c)), v(("y", i1, i2, c)) + # y >= a - b, y >= b - a, y <= a + b, y <= 2 - a - b + cons += [f"+1 x{y} -1 x{a} +1 x{bb} >= 0 ;", + f"+1 x{y} +1 x{a} -1 x{bb} >= 0 ;", + f"-1 x{y} +1 x{a} +1 x{bb} >= 0 ;", + f"-1 x{y} -1 x{a} -1 x{bb} >= -2 ;"] + ys.append(y) + orth = (p == q) or b(p, q, k) == 0 + lhs = " ".join(f"+1 x{y}" for y in ys) + if orth: + cons.append(f"{lhs} = {len(I)//2} ;") + else: + z = v(("z", i1, i2)) + cons.append(f"{lhs} -4 x{z} = {len(I)//2 - 2} ;") + with open(path, "w", encoding="ascii") as f: + f.write(f"* #variable= {len(var)} #constraint= {len(cons)}\n") + f.write(f"* idea3 frame-reduced instance E2, k'={k}, m={2**(5-k)}; gauge-fixed bits {fixed}\n") + f.write("\n".join(cons) + "\n") + log(f" wrote {os.path.basename(path)}: {len(var)} variables, {len(cons)} constraints, {fixed} gauge-fixed (NOT solved)") + + +def main(): + log("=== frame_reduction.py start (exact combinatorics, no solver) ===") + for k in (1, 2, 3, 4): + check(k) + if "--write-opb" in sys.argv: + k = int(sys.argv[sys.argv.index("--write-opb") + 1]) + write_opb(k, os.path.join(HERE, f"e2_k{k}.opb")) + log("=== frame_reduction.py done ===") + + +if __name__ == "__main__": + main() diff --git a/research/line-system-510-signing-nonexistence/tools/sat_k2.py b/research/line-system-510-signing-nonexistence/tools/sat_k2.py new file mode 100644 index 0000000000..b0ef1714c0 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/tools/sat_k2.py @@ -0,0 +1,143 @@ +"""Idea 3, decisive small test: does the k'=2 descendant exist? +120 unit lines in R^24, labels W(3,2) with multiplicity 8, |cos| in {0, 1/4}, +saturated. Frame-reduced encoding E2 (REPORT.md section 3), solved with CP-SAT. + +If INFEASIBLE: the 510-line object in R^30 cannot exist (descent, REPORT.md section 2). +If FEASIBLE: the solution is rebuilt as exact integer vectors and every pairwise +product is re-checked; the vectors go to sat_k2_solution.json. + +Run: py -3.12 sat_k2.py [time_limit_seconds=1800] [workers=8] +Progress lines go to progress.log every 60 s; CP-SAT's own log to sat_k2_cpsat.log. +""" +import datetime +import itertools +import json +import os +import sys +import threading +import time + +from ortools.sat.python import cp_model + +from frame_reduction import b, build + +HERE = os.path.dirname(os.path.abspath(__file__)) +LOG = os.path.join(HERE, "progress.log") +K = 2 + + +def log(msg): + line = f"[{datetime.datetime.now():%Y-%m-%d %H:%M:%S}] {msg}" + print(line, flush=True) + with open(LOG, "a", encoding="utf-8") as f: + f.write(line + "\n") + + +def main(): + limit = float(sys.argv[1]) if len(sys.argv) > 1 else 1800.0 + workers = int(sys.argv[2]) if len(sys.argv) > 2 else 8 + nclasses = int(sys.argv[3]) if len(sys.argv) > 3 else None + m, pts, L, others, supp, T = build(K) + if nclasses is not None: + # sub-test: keep only the first nclasses classes p0 + L (a necessary condition) + keys = sorted({tuple(b(xx, p, K) for xx in L) for p in others})[:nclasses] + others = [p for p in others if tuple(b(xx, p, K) for xx in L) in keys] + log(f" sub-test: only {nclasses} of {2**K - 1} classes, {len(others)} points kept") + suf = f"_c{nclasses}" if nclasses else "" + lines = [(p, j) for p in others for j in range(m)] + model = cp_model.CpModel() + x = {} + for li, (p, j) in enumerate(lines): + for c in supp[p]: + x[li, c] = model.NewBoolVar(f"x{li}_{c}") + # gauge: x = 0 on a spanning forest of the line/coordinate incidence graph + parent = {} + + def find(a): + while parent.setdefault(a, a) != a: + parent[a] = parent[parent[a]] + a = parent[a] + return a + + fixed = 0 + for li, (p, j) in enumerate(lines): + for c in supp[p]: + ra, rb = find(("l", li)), find(("c", c)) + if ra != rb: + parent[ra] = rb + model.Add(x[li, c] == 0) + fixed += 1 + npairs = 0 + for (i1, (p, _)), (i2, (q, _)) in itertools.combinations(enumerate(lines), 2): + I = sorted(set(supp[p]) & set(supp[q])) + if not I: + continue + ys = [] + for c in I: + y = model.NewBoolVar("") + model.AddBoolXOr([x[i1, c], x[i2, c], y.Not()]) # y = x1 xor x2 + ys.append(y) + if p == q or b(p, q, K) == 0: + model.Add(sum(ys) == len(I) // 2) + else: + z = model.NewBoolVar("") + model.Add(sum(ys) == len(I) // 2 - 2 + 4 * z) + npairs += 1 + log(f"=== sat_k2.py start: k'={K}, {len(lines)} non-frame lines in R^{T}, {len(x)} sign bits, " + f"{npairs} pair constraints, {fixed} gauge-fixed; CP-SAT {workers} workers, limit {limit:.0f} s ===") + + solver = cp_model.CpSolver() + solver.parameters.max_time_in_seconds = limit + solver.parameters.num_search_workers = workers + solver.parameters.log_search_progress = True + cplog = open(os.path.join(HERE, f"sat_k2{suf}_cpsat.log"), "w", encoding="utf-8") + solver.log_callback = lambda s: (cplog.write(s + "\n"), cplog.flush()) + + t0 = time.time() + done = threading.Event() + + def heartbeat(): + while not done.wait(60): + log(f" sat_k2 running, {time.time()-t0:.0f} s elapsed (limit {limit:.0f} s)") + + threading.Thread(target=heartbeat, daemon=True).start() + status = solver.Solve(model) + done.set() + cplog.close() + name = solver.StatusName(status) + log(f" CP-SAT status {name} after {time.time()-t0:.1f} s") + + if status in (cp_model.OPTIMAL, cp_model.FEASIBLE): + # exact rebuild: 4*u as integer vectors in the frame basis + vecs = [] + for c in range(T): + e = [0] * T + e[c] = 4 + vecs.append(("frame", c, e)) + for li, (p, j) in enumerate(lines): + e = [0] * T + for c in supp[p]: + e[c] = -1 if solver.Value(x[li, c]) else 1 + vecs.append((p, j, e)) + lab = [L[v[1] // m] if v[0] == "frame" else v[0] for v in vecs] + bad = 0 + for (a, va), (bb, vb) in itertools.combinations(list(zip(lab, [v[2] for v in vecs])), 2): + dot = sum(s * t for s, t in zip(va, vb)) + want_orth = a == bb or b(a, bb, K) == 0 + if (want_orth and dot != 0) or (not want_orth and abs(dot) != 4): + bad += 1 + norms_ok = all(sum(t * t for t in v[2]) == 16 for v in vecs) + log(f" exact check of {len(vecs)} lines: norms ok={norms_ok}, bad pairs={bad}") + with open(os.path.join(HERE, f"sat_k2{suf}_solution.json"), "w", encoding="utf-8") as f: + json.dump({"note": "4*u in the frame basis; label per line", "labels": lab, + "vectors": [v[2] for v in vecs]}, f) + log(" RESULT: FEASIBLE" + (" (sub-test only: says nothing decisive)" if nclasses else ": 120-line descendant EXISTS (k'=2 does not kill the 510 object)")) + elif status == cp_model.INFEASIBLE: + log(" RESULT: INFEASIBLE -> no 120-line descendant -> the 510-line object in R^30 does not exist") + else: + log(" RESULT: UNKNOWN (time limit reached, no decision)") + log("=== sat_k2.py done ===") + + +if __name__ == "__main__": + main() diff --git a/research/line-system-510-signing-nonexistence/tools/sat_sb.py b/research/line-system-510-signing-nonexistence/tools/sat_sb.py new file mode 100644 index 0000000000..803e4c8031 --- /dev/null +++ b/research/line-system-510-signing-nonexistence/tools/sat_sb.py @@ -0,0 +1,198 @@ +"""Idea 3: frame-reduced CP-SAT with symmetry breaking and Hadamard structure. + +Same object as sat_k2.py (REPORT.md sections 2-3), with three additions: + 1. Symmetry breaking by lex-leader constraints x <=lex g(x) for a set of + automorphisms g, all w.r.t. one row-major variable order (lines, then coords), + which keeps them valid simultaneously: + - negating a line -> its first entry is + (x = 0) + - negating a coordinate-> its first entry is + + - swapping two twin lines (same label) -> rows in lex order + - swapping two twin frame coordinates -> columns in lex order + 2./3. Hadamard structure as redundant constraints: in every class the two + collinearity groups are 16 x 16 Hadamard matrices, so their COLUMNS are also + pairwise orthogonal (H^T H = 16 I). Classes interact only on their shared + 8 coordinates; that is left to the solver. +The spanning-forest gauge of sat_k2.py is NOT used (it is not compatible with 1). + +Run: py -3.12 sat_sb.py K [time_limit_s=1800] [workers=6] [nclasses, 0=all] [flags: nosb,nocol] + K = 1: control, 48 lines in R^16 (3 unbiased bases; known to exist) + K = 2: 120 lines in R^24 (decides the 510 object) +""" +import datetime +import itertools +import json +import os +import sys +import threading +import time + +from ortools.sat.python import cp_model + +from frame_reduction import b, build + +HERE = os.path.dirname(os.path.abspath(__file__)) +LOG = os.path.join(HERE, "progress.log") + + +def log(msg): + line = f"[{datetime.datetime.now():%Y-%m-%d %H:%M:%S}] {msg}" + print(line, flush=True) + with open(LOG, "a", encoding="utf-8") as f: + f.write(line + "\n") + + +def xor(model, a, c): + y = model.NewBoolVar("") + model.AddBoolXOr([a, c, y.Not()]) # y = a xor c + return y + + +def lex_leq(model, A, B): + """A <=lex B for equal-length lists of bool vars (0 < 1).""" + e = None # "prefix equal so far"; None means true + for i, (a, c) in enumerate(zip(A, B)): + if e is None: + model.AddImplication(a, c) + else: + model.Add(a <= c).OnlyEnforceIf(e) + if i == len(A) - 1: + break + d = xor(model, a, c) + e2 = model.NewBoolVar("") + if e is None: + model.Add(e2 == 1 - d) + else: + model.Add(e2 <= e) + model.Add(e2 <= 1 - d) + model.Add(e2 >= e - d) + e = e2 + + +def main(): + K = int(sys.argv[1]) + limit = float(sys.argv[2]) if len(sys.argv) > 2 else 1800.0 + workers = int(sys.argv[3]) if len(sys.argv) > 3 else 6 + nclasses = int(sys.argv[4]) if len(sys.argv) > 4 and sys.argv[4] != "0" else None + flags = sys.argv[5].split(",") if len(sys.argv) > 5 else [] + use_sb, use_col = "nosb" not in flags, "nocol" not in flags + m, pts, L, others, supp, T = build(K) + key = {p: tuple(b(xx, p, K) for xx in L) for p in others} + keys = sorted(set(key.values())) + if nclasses is not None: + keys = keys[:nclasses] + others = [p for p in others if key[p] in keys] + suf = f"_k{K}" + (f"_c{nclasses}" if nclasses else "") + "".join("_" + f for f in flags) + lines = [(p, j) for p in others for j in range(m)] + model = cp_model.CpModel() + x = {} + for li, (p, j) in enumerate(lines): + for c in supp[p]: + x[li, c] = model.NewBoolVar(f"x{li}_{c}") + + # pair constraints (rows of the Gram matrix) + npairs = 0 + for (i1, (p, _)), (i2, (q, _)) in itertools.combinations(enumerate(lines), 2): + I = sorted(set(supp[p]) & set(supp[q])) + if not I: + continue + ys = [xor(model, x[i1, c], x[i2, c]) for c in I] + if p == q or b(p, q, K) == 0: + model.Add(sum(ys) == len(I) // 2) + else: + z = model.NewBoolVar("") + model.Add(sum(ys) == len(I) // 2 - 2 + 4 * z) + npairs += 1 + + # 2./3. Hadamard column orthogonality inside every collinearity group + ncol = 0 + for kk in (keys if use_col else []): + members = [p for p in others if key[p] == kk] + p0 = members[0] + groups = [[q for q in members if q == p0 or b(p0, q, K) == 0]] + groups.append([q for q in members if q not in groups[0]]) + for g in groups: + rows = [li for li, (p, j) in enumerate(lines) if p in g] + assert len(rows) == 16 + S = supp[g[0]] + for c1, c2 in itertools.combinations(S, 2): + model.Add(sum(xor(model, x[r, c1], x[r, c2]) for r in rows) == 8) + ncol += 1 + + # 1. symmetry breaking (lex-leader, row-major order) + nsb = 0 + for li, (p, j) in (enumerate(lines) if use_sb else []): # line negation + model.Add(x[li, min(supp[p])] == 0) + nsb += 1 + for c in (range(T) if use_sb else []): # coordinate negation + first = next((li for li, (p, j) in enumerate(lines) if c in supp[p]), None) + if first is not None: + model.Add(x[first, c] == 0) + nsb += 1 + for li, (p, j) in (enumerate(lines) if use_sb else []): # twin lines: rows lex ordered + if j + 1 < m: + S = sorted(supp[p]) + lex_leq(model, [x[li, c] for c in S], [x[li + 1, c] for c in S]) + nsb += 1 + for c in (range(T) if use_sb else []): # twin frame coords: columns lex ordered + if (c + 1) % m != 0: + rows = [li for li, (p, j) in enumerate(lines) if c in supp[p]] + if rows: + lex_leq(model, [x[r, c] for r in rows], [x[r, c + 1] for r in rows]) + nsb += 1 + + log(f"=== sat_sb.py start: k'={K}{' sub-test '+str(nclasses)+' classes' if nclasses else ''}, " + f"{len(lines)} non-frame lines in R^{T}, {len(x)} sign bits, {npairs} pair + {ncol} column constraints, " + f"{nsb} symmetry-breaking constraints, flags {flags}; CP-SAT {workers} workers, limit {limit:.0f} s ===") + + solver = cp_model.CpSolver() + solver.parameters.max_time_in_seconds = limit + solver.parameters.num_search_workers = workers + solver.parameters.log_search_progress = True + cplog = open(os.path.join(HERE, f"sat_sb{suf}_cpsat.log"), "w", encoding="utf-8") + solver.log_callback = lambda s: (cplog.write(s + "\n"), cplog.flush()) + t0 = time.time() + done = threading.Event() + + def heartbeat(): + while not done.wait(60): + log(f" sat_sb{suf} running, {time.time()-t0:.0f} s elapsed (limit {limit:.0f} s)") + + threading.Thread(target=heartbeat, daemon=True).start() + status = solver.Solve(model) + done.set() + cplog.close() + log(f" CP-SAT status {solver.StatusName(status)} after {time.time()-t0:.1f} s") + + if status in (cp_model.OPTIMAL, cp_model.FEASIBLE): + vecs, lab = [], [] + for c in range(T): + e = [0] * T + e[c] = 4 + vecs.append(e) + lab.append(L[c // m]) + for li, (p, j) in enumerate(lines): + e = [0] * T + for c in supp[p]: + e[c] = -1 if solver.Value(x[li, c]) else 1 + vecs.append(e) + lab.append(p) + bad = 0 + for (a, va), (bb, vb) in itertools.combinations(list(zip(lab, vecs)), 2): + dot = sum(s * t for s, t in zip(va, vb)) + want_orth = a == bb or b(a, bb, K) == 0 + if (want_orth and dot != 0) or (not want_orth and abs(dot) != 4): + bad += 1 + norms_ok = all(sum(t * t for t in v) == 16 for v in vecs) + log(f" exact check of {len(vecs)} lines (4u, integer): norms ok={norms_ok}, bad pairs={bad}") + with open(os.path.join(HERE, f"sat_sb{suf}_solution.json"), "w", encoding="utf-8") as f: + json.dump({"note": "4*u in the frame basis; label per line", "labels": lab, "vectors": vecs}, f) + log(f" RESULT: FEASIBLE ({'sub-test only' if nclasses else 'full object exists'})") + elif status == cp_model.INFEASIBLE: + log(" RESULT: INFEASIBLE" + (" -> 510-line object does not exist" if K >= 2 else " (control FAILED: bug)")) + else: + log(" RESULT: UNKNOWN (time limit reached, no decision)") + log("=== sat_sb.py done ===") + + +if __name__ == "__main__": + main() diff --git a/research/line-system-510-signing-nonexistence/verify.py b/research/line-system-510-signing-nonexistence/verify.py new file mode 100644 index 0000000000..c61a615b8e --- /dev/null +++ b/research/line-system-510-signing-nonexistence/verify.py @@ -0,0 +1,180 @@ +"""Exact checks for the non-existence of the 510-line signing (line-system-saturation section 11.1). + +Standard library only. Every finite fact used by the proof in README.md is checked +exhaustively, plus a positive control (the k'=1 rung, 48 lines in R^16, built explicitly) +and the Delsarte inequalities showing that the two-point LP cannot decide the question. + + python3 -B research/line-system-510-signing-nonexistence/verify.py +""" +from fractions import Fraction as Fr +import itertools +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(HERE)) +FAILS = [] + + +def check(name, ok, detail=""): + print(("PASS " if ok else "FAIL ") + name + (f" ({detail})" if detail else "")) + if not ok: + FAILS.append(name) + + +def b(p, q, k): + """Standard symplectic form on F2^(2k), pairs (2i, 2i+1).""" + s = 0 + for i in range(k): + s ^= ((p >> (2 * i)) & 1) & ((q >> (2 * i + 1)) & 1) + s ^= ((p >> (2 * i + 1)) & 1) & ((q >> (2 * i)) & 1) + return s + + +# ---------------------------------------------------------------- 0. the open question we answer +def check_input(): + with open(os.path.join(ROOT, "research/line-system-saturation/README.md"), encoding="utf-8") as f: + text = f.read() + check("input: section 11.1 states the 510-vertex signing S^2 = 60S + 256I as OPEN", + "510-vertex signing" in text and "S² = 60S + 256I" in text) + + +# ---------------------------------------------------------------- 1. frame form of the 120-line rung +def check_frame_form(): + k, m = 2, 8 + pts = range(1, 16) + # coordinates (x1, y1, x2, y2) = bits (0, 1, 2, 3); L = , a = x1, b = x2 + a, bb = 0b0001, 0b0100 + L = [a, bb, a ^ bb] + check("L is totally isotropic", all(b(p, q, k) == 0 for p in L for q in L)) + check("labels and dimension", len(L) * m == 24 and len(pts) * m == 120) + y1 = lambda p: (p >> 1) & 1 + y2 = lambda p: (p >> 3) & 1 + x1 = lambda p: p & 1 + x2 = lambda p: (p >> 2) & 1 + supp_ok = all((b(a, p, k), b(bb, p, k)) == (y1(p), y2(p)) for p in pts) + check("b(a,p) = y1(p), b(b,p) = y2(p)", supp_ok) + # every non-frame label is non-orthogonal to exactly 2 frame labels = 16 frame lines + others = [p for p in pts if p not in L] + check("each non-frame line meets 16 frame lines", + all(sum(b(x, p, k) for x in L) * m == 16 for p in others)) + K1 = [p for p in others if (y1(p), y2(p)) == (1, 1)] # support A u B + K2 = [p for p in others if (y1(p), y2(p)) == (1, 0)] # support A u C + check("supports: K1 on A u B, K2 on A u C", + all(b(a, p, k) and b(bb, p, k) and not b(a ^ bb, p, k) for p in K1) + and all(b(a, p, k) and not b(bb, p, k) and b(a ^ bb, p, k) for p in K2) + and len(K1) == 4 and len(K2) == 4) + check("cross collinearity b(p,q) = x1(p) + x1(q) + x2(q)", + all(b(p, q, k) == x1(p) ^ x1(q) ^ x2(q) for p in K1 for q in K2)) + check("K1 collinear iff x1+x2 equal", + all(b(p, q, k) == (x1(p) ^ x2(p) ^ x1(q) ^ x2(q)) for p in K1 for q in K1 if p != q)) + P0 = [p for p in K1 if x1(p) == 0] + check("the two points of P0 are non-collinear", len(P0) == 2 and b(P0[0], P0[1], k) == 1) + groups = {} + for p in K1: + groups.setdefault(x1(p) ^ x2(p), []).append(p) + check("each K1 collinearity group has one point of P0 and one of P1", + all(sorted(x1(p) for p in g) == [0, 1] for g in groups.values())) + + +# ---------------------------------------------------------------- 2. finite lemmas of Step 3 +def check_lemmas(): + S = list(itertools.product((1, -1), repeat=4)) + # (a) a row m with m.s = +-1 for all s in {+-1}^4: entries are forced into {0,+-1} + # (flip one coordinate: 2 m_i in {0, +-2}); among those, exactly one non-zero entry. + rows = [mm for mm in itertools.product((0, 1, -1), repeat=4) + if all(abs(sum(u * v for u, v in zip(mm, s))) == 1 for s in S)] + check("(a) linear maps {+-1}^4 -> {+-1}^4 have rows with one non-zero entry", + len(rows) == 8 and all(sum(1 for t in mm if t) == 1 for mm in rows)) + # (b) the 8 lines s (mod sign); partitions into 4 + 4 with all cross |s.t| = 2 + lines = [s for s in S if s[0] == 1] + dot = lambda s, t: sum(u * v for u, v in zip(s, t)) + parts = [] + for U in itertools.combinations(range(8), 4): + V = [i for i in range(8) if i not in U] + if all(abs(dot(lines[i], lines[j])) == 2 for i in U for j in V): + parts.append(U) + par = lambda s: sum(1 for t in s if t < 0) % 2 + ok = len(parts) == 2 and all(len({par(lines[i]) for i in U}) == 1 for U in parts) + ok &= all(dot(lines[i], lines[j]) == 0 for U in parts for i, j in itertools.combinations(U, 2)) + check("(b) only the parity split works, and each parity class is pairwise orthogonal", ok, + f"{len(parts)} ordered splits") + # inner products in S0 = {(s, Ms)} are 2 s.t for a signed permutation M + M = [(2, 1), (0, -1), (3, 1), (1, -1)] + emb = lambda s: tuple(s) + tuple(sgn * s[i] for i, sgn in M) + check("(a') (s,Ms).(t,Mt) = 2 s.t for a signed permutation M", + all(dot(emb(s), emb(t)) == 2 * dot(s, t) for s in S for t in S)) + + +# ---------------------------------------------------------------- 3. the contradiction (Step 4) +def check_contradiction(): + bad = [(d, t) for d in (8, -8) for t in range(-8, 9, 2) if abs(d + t) == 4 and abs(d - t) == 4] + check("Step 4: no t with |8d+t| = |8d-t| = 4", not bad) + # twins on one A-direction: (e, w), (e', w2) orthogonal with e' = +-e forces w2 = -+w + S8 = list(itertools.product((1, -1), repeat=8)) + w = S8[37] + forced = [w2 for w2 in S8 if 8 + sum(u * v for u, v in zip(w, w2)) == 0] + check("Step 4: twin with the same A-part has B-part -w", forced == [tuple(-u for u in w)]) + + +# ---------------------------------------------------------------- 4. positive control: the k'=1 rung +def check_control(): + """48 lines in R^16: frame + Sylvester rows + bent-shifted Sylvester rows (labels of W(1,2)).""" + xs = list(range(16)) + pc = lambda v: bin(v).count("1") & 1 + f = lambda x: ((x & 1) & ((x >> 1) & 1)) ^ (((x >> 2) & 1) & ((x >> 3) & 1)) # bent + frame = [[4 if c == r else 0 for c in xs] for r in xs] + H = [[(-1) ** pc(a & x) for x in xs] for a in xs] + Hb = [[(-1) ** (pc(a & x) ^ f(x)) for x in xs] for a in xs] + vecs = [(0, v) for v in frame] + [(1, v) for v in H] + [(2, v) for v in Hb] + + def violations(vs): + bad = 0 + for (la, u), (lb, v) in itertools.combinations(vs, 2): + d = sum(s * t for s, t in zip(u, v)) + bad += (d != 0) if la == lb else (abs(d) != 4) + return bad + + check("control: 48 lines in R^16 with |cos| in {0,1/4} exist (exact)", + violations(vecs) == 0 and all(sum(t * t for t in v) == 16 for _, v in vecs)) + broken = [(l, list(v)) for l, v in vecs] + broken[20][1][3] *= -1 + check("failure control: one flipped sign is rejected", violations(broken) > 0) + unbent = vecs[:32] + [(2, v) for v in H] + check("failure control: two copies of the same basis are rejected", violations(unbent) > 0) + + +# ---------------------------------------------------------------- 5. Delsarte inequalities +def gegenbauer(n, kmax, t): + lam = Fr(n - 2, 2) + c, c1 = [Fr(1), 2 * lam * t], [Fr(1), 2 * lam] + for k in range(1, kmax): + c.append((2 * (k + lam) * t * c[k] - (k + 2 * lam - 1) * c[k - 1]) / (k + 1)) + c1.append((2 * (k + lam) * c1[k] - (k + 2 * lam - 1) * c1[k - 1]) / (k + 1)) + return [c[k] / c1[k] for k in range(kmax + 1)] + + +def check_delsarte(): + for n, a0, a1 in [(30, 253, 256), (28, 123, 128), (24, 55, 64), (16, 15, 32)]: + q0, qa = gegenbauer(n, 40, Fr(0)), gegenbauer(n, 40, Fr(1, 4)) + vals = [1 + a0 * q0[k] + a1 * qa[k] for k in range(2, 41, 2)] + check(f"Delsarte: R^{n}, distribution 1+{a0}+{a1}: degree 2 = 0, degrees 4..40 > 0", + vals[0] == 0 and all(v > 0 for v in vals[1:])) + + +def main(): + check_input() + check_frame_form() + check_lemmas() + check_contradiction() + check_control() + check_delsarte() + if FAILS: + print(f"FAIL {len(FAILS)} check(s)") + return 1 + print("PASS_LINE_SYSTEM_510_SIGNING_NONEXISTENCE_FINITE_FACTS") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From 0723ddc960cde24d55a78ddb2994d5caadc99d94 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:18:04 +0300 Subject: [PATCH 2/2] Check that M is a signed permutation and tighten Steps 3-4 of the 510-line proof Review of #5347: enumerate all 4096 one-entry-per-row signed maps; only the 384 signed permutations leave +-1 vectors in S0^perp, which must hold 8 lines. README adds the trace argument for dim S0 = 4 and states Step 4 as two disjoint solution sets. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../README.md | 23 +++++++++++------ .../verify.py | 25 +++++++++++++++---- 2 files changed, 36 insertions(+), 12 deletions(-) diff --git a/research/line-system-510-signing-nonexistence/README.md b/research/line-system-510-signing-nonexistence/README.md index d2bf443ba4..d4c2c9c0f1 100644 --- a/research/line-system-510-signing-nonexistence/README.md +++ b/research/line-system-510-signing-nonexistence/README.md @@ -36,16 +36,21 @@ P₀–Q₁ and P₁–Q₀ products are ±4. Each collinearity group of K₁ is one point of P₀ and one of P₁. The two points of P₀ are non-collinear. **Step 3 (A-parts).** Let U_i, V_i be the A-parts of P_i, Q_i, with N_i = Σ_{U_i} uuᵀ. Hadamard columns are -orthogonal, so N₀ + N₁ = 32I = M₀ + M₁. From U₀ ⟂ V₀, U₁ ⟂ V₁ and the full rank of the sums, all four -dimensions are 4, S₀ := span U₀ = (span U₁)^⊥ and V₁ ⊆ S₀. -(a) A 4-space holds at most 16 vectors of {±1}⁸. U₀ and V₁ both span S₀ and share no line (products ±4, not -±8). So S₀ holds exactly 8 lines and is the graph of a signed permutation, with (s, Ms)·(t, Mt) = 2 s·t. +orthogonal, so N₀ + N₁ = 32I = M₀ + M₁. Put S_i = span U_i. For x ⟂ S₁, N₁x = 0 gives N₀x = 32x, so +S₀ = S₁^⊥ and N₀ = 32·P_{S₀}; taking traces, 16·8 = 32·dim S₀, so dim S₀ = dim S₁ = 4. In the same way +U₀ ⟂ V₀ and U₁ ⟂ V₁ give span V₀ = S₁ and span V₁ = S₀. +(a) A k-space holds at most 2^k vectors of {±1}⁸ (project to an information set). U₀ and V₁ both span S₀ and +share no line (products ±4, not ±8), so S₀ holds exactly 8 lines, and likewise S₁ = S₀^⊥ (spanned by U₁ and +V₀). In this equality case S₀ = {(s, Ms)} on an information set, with each row of M having a single ±1 entry. +Of the 4⁴·2⁴ = 4096 such maps, the 3712 that are not signed permutations leave no ±1 vector in S₀^⊥ (checked); +so M is a signed permutation, and (s, Ms)·(t, Mt) = 2 s·t. (b) Cross products ±4 force odd Hamming distance, so U₀ is one parity class: 4 pairwise orthogonal directions. (c) A point's group partner has A-parts in S₀^⊥, so each point of P₀ uses each direction exactly twice. **Step 4 (contradiction).** The two lines of p ∈ P₀ on a direction e are twins, so they are (e, w) and (e, −w) -up to sign. Take a line (±e, w′) of the other point p′ ∈ P₀; it exists by (c). Non-collinearity needs -|±8 + w·w′| = |±8 − w·w′| = 4, so w·w′ = 0 and both values equal 8. Contradiction. ∎ +up to sign. Take a line (±e, w′) of the other point p′ ∈ P₀; it exists by (c). Non-collinearity with both +twins needs |8 + x| = 4 and |8 − x| = 4 for x = ±w·w′. The first gives x ∈ {−4, −12} and the second +x ∈ {4, 12}; no x satisfies both. Contradiction. ∎ The proof uses only two classes sharing one block. This is why the two-class CP-SAT sub-test below is already infeasible. @@ -55,7 +60,8 @@ infeasible. `verify.py` (registered, about 1 s, standard library only) checks: - that #2244 states the question as open; - the Step 2 combinatorics exhaustively on W(3,2); -- lemmas (a) and (b) by enumeration, and the Step 4 arithmetic; +- lemmas (a) and (b) by enumeration, including that M is a signed permutation (all 4096 one-entry-per-row + signed maps: only the 384 signed permutations leave ±1 vectors in S₀^⊥), and the Step 4 arithmetic; - a positive control: the k′ = 1 rung exists, 48 lines in ℝ¹⁶ (frame + Sylvester H₁₆ + bent-shifted H₁₆) built and checked exactly, plus two failure controls; - the Delsarte inequalities. For each rung the forced distance distribution passes every Gegenbauer @@ -94,6 +100,9 @@ Structured versions are in `TASK.json`. ## Credit +James Reed (jwr404) reviewed the proof and supplied the signed-permutation step of (a), the dimension count of +Step 3 and the cleaner form of Step 4. + The question, the descent proposition, Theorem G and the counts used here are from `line-system-saturation` (#2244). This package adds the frame reduction, the hand proof and the checks. Prepared for Mark (Matarener) with substantial Claude (Anthropic) assistance. Apache-2.0. diff --git a/research/line-system-510-signing-nonexistence/verify.py b/research/line-system-510-signing-nonexistence/verify.py index c61a615b8e..f4c85f1cc7 100644 --- a/research/line-system-510-signing-nonexistence/verify.py +++ b/research/line-system-510-signing-nonexistence/verify.py @@ -99,11 +99,26 @@ def check_lemmas(): ok &= all(dot(lines[i], lines[j]) == 0 for U in parts for i, j in itertools.combinations(U, 2)) check("(b) only the parity split works, and each parity class is pairwise orthogonal", ok, f"{len(parts)} ordered splits") - # inner products in S0 = {(s, Ms)} are 2 s.t for a signed permutation M - M = [(2, 1), (0, -1), (3, 1), (1, -1)] - emb = lambda s: tuple(s) + tuple(sgn * s[i] for i, sgn in M) - check("(a') (s,Ms).(t,Mt) = 2 s.t for a signed permutation M", - all(dot(emb(s), emb(t)) == 2 * dot(s, t) for s in S for t in S)) + # (a') M is forced to be a signed permutation: S1 = S0^perp must also hold exactly 8 lines (U1 and V0 span it + # and share none), and among all 4^4 * 2^4 one-entry-per-row signed maps only the signed permutations leave + # any +-1 vector in S0^perp. For those, (s,Ms).(t,Mt) = 2 s.t. + S8 = list(itertools.product((1, -1), repeat=8)) + tally = {} + perm_ok = True + for cols in itertools.product(range(4), repeat=4): + for sg in itertools.product((1, -1), repeat=4): + emb = lambda s: tuple(s) + tuple(sg[r] * s[cols[r]] for r in range(4)) + basis = [emb(s) for s in ((1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0), (0, 0, 0, 1))] + inside = {emb(s) for s in S} + perp = [v for v in S8 if all(dot(v, w) == 0 for w in basis)] + is_perm = len(set(cols)) == 4 + key = (is_perm, len(inside) // 2, len(perp) // 2) + tally[key] = tally.get(key, 0) + 1 + if is_perm: + perm_ok &= all(dot(emb(s), emb(t)) == 2 * dot(s, t) for s in S for t in S) + check("(a') S0 and S0^perp both hold 8 lines only for the 384 signed permutations (3712 other maps: 0)", + tally == {(True, 8, 8): 384, (False, 8, 0): 3712}, str(sorted(tally.items()))) + check("(a') (s,Ms).(t,Mt) = 2 s.t for every signed permutation M", perm_ok) # ---------------------------------------------------------------- 3. the contradiction (Step 4)