diff --git a/research/connector-c5-certificate/.gitattributes b/research/connector-c5-certificate/.gitattributes new file mode 100644 index 0000000000..9018e3d7b5 --- /dev/null +++ b/research/connector-c5-certificate/.gitattributes @@ -0,0 +1,2 @@ +# Preserve raw native transcripts, including their progress-line padding. +logs/*.txt -whitespace diff --git a/research/connector-c5-certificate/.gitignore b/research/connector-c5-certificate/.gitignore new file mode 100644 index 0000000000..cd31df98bc --- /dev/null +++ b/research/connector-c5-certificate/.gitignore @@ -0,0 +1,6 @@ +artifacts/*.cnf +artifacts/*.drat +artifacts/*.bdrat +artifacts/*.lrat +__pycache__/ +.coverage diff --git a/research/connector-c5-certificate/ATTEMPTS.md b/research/connector-c5-certificate/ATTEMPTS.md new file mode 100644 index 0000000000..44b3775caf --- /dev/null +++ b/research/connector-c5-certificate/ATTEMPTS.md @@ -0,0 +1,42 @@ +# Bounded visit record + +Start: 2026-10-29 19:07:50 UTC; deadline: 19:52:50 UTC. +Author: Alexander Richard Towell, substantial OpenAI Codex assistance. + +1. Refreshed PR searches, current contribution rules and the latest fifty + top-level handoff comments (with up to five replies each). No overlapping + characteristic-five certificate was found within that bounded coverage. + Posted one claim, linked in visit.json. This is not a global novelty search. +2. Established pinned PySAT and independently built C checkers within ten + minutes. Exported the 4,278-variable/52,672-clause formula. The solver + reported UNSAT in 157.646 seconds. Its binary proof was copied from its + temporary file; optional ASCII expansion also completed, but is not archived. +3. DRAT-trim verified the complete binary trace in 215.749 seconds. Its + trimmed ASCII trace is 276,652,282 bytes, compressed to 38,506,051 bytes. + A separate trimmed-trace replay verified in 103.756 seconds. Larger raw + traces and intermediate LRAT files are ignored runtime files, not required + public inputs. The archived replay regenerates LRAT from the trimmed proof. +4. The first wrapper failed its SAT negative control: the original LRAT checker + accepted a fake empty-clause derivation. The separate AI reviewer caught + this concrete false acceptance. An independent reproduction confirmed it. + Earlier positive LRAT output from that checker is not relied on. +5. One evidence-driven pivot: resolve the checker prerequisite rather than + remove the control. A minimal local guard trial rejected the fake proof and + checked the full target. Refreshing the checker repository then found the + already reported issue42 and haskiindahouse's pending PR43, which supplies + the same mathematical correction. The final packet uses PR43's exact + unchanged source and credits it; no new checker bug or fix is claimed. +6. The complete archived replay with PR43 source passed under Python -O: + DRAT checking/conversion 108.550 seconds, LRAT checking 15.91 seconds, + three native rejecting controls and two predecessor-control modes passed. + The written encoding bridge was separately reviewed; no mathematical + blocker was found. This is AI review, not human review. +7. A tiny integration test exposed buffering in the pinned PySAT proof stream. + The optional generator now explicitly flushes C stdio before copying its + binary file; the real tiny-UNSAT test passes. It is a POSIX/Linux adapter, + not a change to the certificate or a second research investigation. + +The search domain was one specified CNF, with deterministic solver defaults +and a 480-second stopping limit. No characteristic-six/seven search, deeper +block search, selected-frontier replay or repository-wide suite was run. +See RESULT.json and the final replay logs for publication-ready verification. diff --git a/research/connector-c5-certificate/CITATION.cff b/research/connector-c5-certificate/CITATION.cff new file mode 100644 index 0000000000..015fdba37a --- /dev/null +++ b/research/connector-c5-certificate/CITATION.cff @@ -0,0 +1,12 @@ +cff-version: 1.2.0 +message: "Cite this scoped certificate contribution and retain the predecessor attribution in NOTICE." +title: "Checked characteristic-five six-source connector exclusion" +type: software +version: 0.1.0 +date-released: 2026-10-29 +authors: + - family-names: Towell + given-names: Alexander Richard + orcid: "https://orcid.org/0000-0001-6443-9897" +license: Apache-2.0 +abstract: "A checked finite refutation for the weight-two/six relaxation of an existing six-source depth-two connector exclusion, with a written encoding bridge, exact source pins, and rejecting controls. Third-party MIT-licensed checker sources retain their notices. Substantial OpenAI Codex assistance." diff --git a/research/connector-c5-certificate/LICENSE b/research/connector-c5-certificate/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/connector-c5-certificate/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/connector-c5-certificate/NOTICE b/research/connector-c5-certificate/NOTICE new file mode 100644 index 0000000000..2560c76793 --- /dev/null +++ b/research/connector-c5-certificate/NOTICE @@ -0,0 +1,33 @@ +Owned contribution: Alexander Richard Towell, with substantial OpenAI Codex +assistance in construction, implementation, verification, and one separate +AI review. Licensed Apache-2.0, except the third-party checker files below. + +Josie Elliston's PR6141 (with disclosed Claude Code assistance) supplied the +SAT encoding, characteristic-five/six solver findings, and original controls. +vendor/search_sat.py and vendor/verify.py are exact unchanged copies from +d192172f57b10647ddcff9410c69d48ac06862c1. The added contribution is a checked +characteristic-five refutation, its encoding bridge, and reproducible replay. + +Nick Petalas supplied PR4231/4248's connector interface, depth and deletion +machinery and earlier bounds. vendor/connector-depth-blocks-README.md is an +unchanged Apache-2.0 source copy. Credit zxv, apoursh, Ross Richardson and the +retained connector lineage as described in that source and PR6141. + +The sequential-counter algorithm is the Knuth/Alex Healy irredundant variant +used in PySAT, following the Sinz cardinality-encoding lineage; no new counter +algorithm is claimed. PySAT and CaDiCaL retain their respective authorship. + +vendor/drat-trim/{drat-trim.c,lrat-check.c,LICENSE} are unchanged files from +marijnheule/drat-trim at 2e3b2dc0ecf938addbd779d42877b6ed69d9a985. +These files retain their MIT license and Marijn Heule/Nathan Wetzler notices. +The LRAT checker carries its additional 2017-2023 Marijn Heule notice. + +vendor/lrat-check-pr43.c is an exact unchanged copy from haskiindahouse's +pending drat-trim PR43, commit 0ca925b4f5b4ed04d02d830807cfd614483e7320. +It fixes the already reported empty-clause acceptance issue42. This packet +reuses that correction and retains a native rejecting regression; neither +the original bug nor the fix is claimed as a new discovery here. + +One AI reviewer checked the written encoding implication and scoped code. +AI review is not human peer review. C certificate checking is not a Lean +kernel proof, a novelty assessment, or verification of integer multiplication. diff --git a/research/connector-c5-certificate/PLAN.md b/research/connector-c5-certificate/PLAN.md new file mode 100644 index 0000000000..fd0046d767 --- /dev/null +++ b/research/connector-c5-certificate/PLAN.md @@ -0,0 +1,55 @@ +# Characteristic-five connector certificate + +Alexander Richard Towell, with substantial OpenAI Codex assistance. + +Start: 2026-10-29 19:07:50 UTC. Setup deadline: 19:17:50 UTC. +Investigation ends by 19:37:50 UTC; final handoff deadline: 19:52:50 UTC. +Workspace base: b6892c8f8c7e060031f8b103f5a8c4bcc7ac8690. + +## Proposition and scope + +No length-30 word with six letters each occurring five times realizes all +nonzero binary six-vectors as sums of two prefix-count vectors modulo five. +The predecessor reports UNSAT already for the sixteen masks of weights 2 and 6. +This visit certifies that finite relaxation and audits the implication from +admissible words to the CNF. It does not change kappa or exclude other interfaces. + +Source: CrocSwap/integer-mult-bounds PR6141, head +d192172f57b10647ddcff9410c69d48ac06862c1. Pinned python-sat 1.9.dev15. +The inherited floor-word and depth-two interface is PR4231/4248. + +## Implementation and verification plan + +- [x] Preserve exact predecessor generator and its positive-word checker. +- [x] Establish a proof-producing SAT backend and independently built drat-trim + within ten minutes; run a tiny UNSAT/SAT check before the target. +- [x] Export deterministic DIMACS for k=6,c=5,weights={2,6}; record exact hashes, + tool versions, clause counts, runtime, and a proof with a bounded solver run. +- [x] Replay the proof with drat-trim; reject empty/corrupt proofs and a + satisfiable CNF control. Audit encoding soundness, especially cardinality + auxiliary variables, coordinate relabeling, and repeated boundaries. +- [x] Package reproducible commands, written implication, tests, source/tool pins, + explicit limitations and one independent scoped AI review if a result is ready. +- [x] Refresh overlap before any public submission; preserve a clean committed + local packet even if certificate generation or verification times out. + +## Success and stopping rules + +Success needs both independent proof replay and a justified encoding bridge. +No unrestricted theorem follows merely from a solver verdict. Stop at the setup +deadline without a viable environment; otherwise bound each expensive run and +reserve the final fifteen minutes. Do not start characteristic seven or another +research problem. Proof logging may be much slower than the reported 160-second +unlogged solve. A failed attempt is recorded as inconclusive, not an impossibility. + +## Review focus + +Reject a proof for a different CNF; do not accept a checker message without its +exit status; do not treat the empty trace on a satisfiable formula as evidence; +retain s=t readouts and the boundary-zero replacement; establish that sequential +counter auxiliaries can be assigned for every valid word. + +Outcome: both archived replays pass with exact existing LRAT PR43 source. +The known issue42 was reproduced and its correction reused; see ATTEMPTS.md. +Normal and optimized nineteen-test suites pass. Publication and closing pins +are recorded separately after the verified source commit. diff --git a/research/connector-c5-certificate/PROOF.md b/research/connector-c5-certificate/PROOF.md new file mode 100644 index 0000000000..b1900a3e4b --- /dev/null +++ b/research/connector-c5-certificate/PROOF.md @@ -0,0 +1,94 @@ +# From a connector word to the certified finite formula + +Alexander Richard Towell, with substantial OpenAI Codex assistance. + +## Claim and dependencies + +Let w be a word of length 30 on six symbols, each appearing five times. +Let q_t(j) count occurrences of symbol j before boundary t, 0 <= t <= 30. +There is no such word for which every binary vector of weight two or six +is congruent to q_s+q_t modulo five for some boundaries s,t. Consequently +there is no depth-two block realizing all 63 nonzero binary vectors in +the PR4231/4248 interface. No other connector interface or characteristic +is covered; no supplier admission or multiplication exponent follows. + +The finite formula is Josie Elliston's PR6141 generator, pinned at +d192172f57b10647ddcff9410c69d48ac06862c1, with python-sat 1.9.dev15, +k=6, c=5, weight pruning enabled and mask weights {2,6}. +The certificate checker establishes only UNSAT of the exact recorded formula. +The following written implication connects it to the claim. It is not a +Lean/kernel formalization. Tool, compiler and hardware correctness remain +part of the computational trust base. + +The LRAT checker used for the final replay includes the exact existing PR43 +correction (head 0ca925b4f5b4ed04d02d830807cfd614483e7320) by haskiindahouse. +The uncorrected checker at 2e3b2dc falsely accepts a fake refutation of a SAT +formula (known issue42); its successful output is not evidence relied on here. +This correction is not a complete audit of either C checker. The separate +DRAT checker verifies the full pinned trace as well. + +## Symmetry, boundaries and weight pruning + +Relabel the six symbols in order of first occurrence. This preserves the +word counts and permutes the full sets of weight-two and weight-six masks. +Thus it suffices to consider words whose first occurrences are increasing. +For any boundary equal to 30, replace it by zero, since q_30=(5,...,5) +is zero modulo five. Reorder the two boundaries to obtain 0 <= s <= t < 30. +Repeated boundaries s=t remain allowed. For every realizing pair, +sum_j(q_s(j)+q_t(j))=s+t, so s+t is congruent to the mask's weight modulo +five. Thus pruning other pairs never discards a possible realization. + +## Assigning the non-cardinality variables + +Set x[p,j] true exactly when w[p]=j. Each position has exactly one symbol. +Set e[t,j,v] true exactly when q_t(j) is congruent to v modulo five. +This satisfies all one-hot residue clauses, initial residues and transitions. +Set f[p,j] true exactly when j has occurred in positions 0 through p. +The defining recurrence is f[p,j] iff x[p,j] or f[p-1,j], with a false +predecessor at p=0. Increasing first occurrences satisfy the symmetry clauses. + +For each mask of weight two or six, select a realizing boundary pair after +the preceding reductions. Set its y[mask,s,t] true and every other selector +false (alternatively, set all realizing selectors true). The mask disjunction +is satisfied. If e[s,j,v] is true, realization forces +e[t,j,(mask_j-v) mod 5], exactly as required by each selector implication. +All other selector implications have false antecedents. + +## Constructive cardinality extension + +For each source, PySAT encodes at-most-five true x-literals and at-most-25 +true negated x-literals. Together these say exactly five occurrences. The +generator's sequential-counter clauses are compared, in order and with actual +variable IDs, against the following independent construction by checks.py. +Every target cardinality clause must match; no unnamed counter is ignored. + +For literals u_0,...,u_(n-1) with total at most r, the interior counter has +variables y[k,j] for 0 <= k < r and 0 <= j < n-r. Assign y[k,j] true iff +at least k+1 of u_0,...,u_(j+k) are true. The clauses are: + +1. u_j implies y[0,j]. +2. y[k,j] implies y[k,j+1], whenever the latter index exists. +3. u_(j+k+1) and y[k,j] imply y[k+1,j], for k < r-1. +4. u_(j+r) and y[r-1,j] cannot both be true. + +The first three follow by counting prefixes. The fourth would require at +least r+1 true input literals, contradicting the assumed bound. This gives +a satisfying extension for each counter. The target uses (n,r)=(30,5) +and (30,25); both are interior cases covered by this construction. +The anonymous variable ranges for different counters are disjoint, and +separate from x/e/f/y. Therefore the extensions combine with the assignments +above to satisfy every clause of the target CNF. + +## Conclusion and evidence levels + +If a word with the claimed realizations existed, the preceding assignments +would satisfy the recorded CNF. A successful checked refutation of that exact +CNF contradicts this. UNSAT for the sixteen selected masks also excludes a +word realizing all 63 masks, since the latter is a stronger requirement. + +The counter interpretation and word-to-CNF bridge are written proofs, supported +by executable clause comparison and finite exhaustive controls. The DRAT/LRAT +replay is a checked finite refutation using C checkers, not a Lean proof or a +formal proof of the full integer-multiplication theorem. AI review is separate +from human peer review and repository acceptance. PR6141's reported characteristic +six exclusion and the open characteristic seven case are not checked here. diff --git a/research/connector-c5-certificate/README.md b/research/connector-c5-certificate/README.md new file mode 100644 index 0000000000..a44cc63d59 --- /dev/null +++ b/research/connector-c5-certificate/README.md @@ -0,0 +1,105 @@ +# Checked characteristic-five connector exclusion + +Alexander Richard Towell, with substantial OpenAI Codex assistance. + +This packet adds a replayable finite certificate to +[Josie Elliston's PR6141](https://github.com/CrocSwap/integer-mult-bounds/pull/6141). +The mathematical exclusion was already reported there using SAT solver output. +Our contribution is checked evidence, the written word-to-CNF implication, +and reproducible failure controls. No new multiplication exponent is claimed. + +## Exact scope + +No length-30 word on six sources, each occurring five times, realizes every +nonzero binary six-vector as the sum of two prefix-count vectors modulo five. +Already the sixteen masks of weights two and six cannot all be realized. +This is the unchanged unsigned dirty connector's depth-two block model from +PR4231/4248. Repeated boundaries and boundary zero are permitted. It does not +exclude deeper blocks, arbitrary floor words, other characteristics or interfaces. + +[PROOF.md](PROOF.md) gives the written reduction to the certified formula. +It explains symmetry, pruning, endpoint replacement, and a constructive meaning +for every anonymous cardinality variable. The two C checkers establish the +finite refutation; this is not a Lean proof or human peer review. + +## Reproduce + +Tested on Linux x86_64, Python 3.13.15 and GCC 13.3; requires Python 3.10 +or newer, GCC and about 2 GB temporary disk space. +Install the exact dependencies in a virtual environment, then run from this +directory: + +```sh +python -m pip install -r requirements.txt +python -O reproduce.py +python -m unittest -q test_checks test_reproduce test_native test_generate +``` + +Expected: JSON status `PASS_CONNECTOR_C5_CERTIFICATE`, both `s VERIFIED` and +`c VERIFIED`, twelve counter blocks checked, and three native rejecting +controls. Source corruption must additionally fail in normal and optimized +Python. The reproduction regenerates the exact 4,278-variable/52,672-clause +formula, authenticates vendored checker sources, builds them, verifies the +trimmed DRAT, converts it to temporary LRAT and checks that independently. +It also replays the predecessor's original positive-word controls in both +Python modes. It never reruns the SAT search. + +The compressed proof is approximately 37 MiB; decompressed DRAT is 264 MiB. +Conversion creates a larger temporary LRAT file. Allow several minutes on a +typical host; the wrapper bounds each native check at 300 seconds. + +## Provenance and verification + +Predecessor generator: `d192172f57b10647ddcff9410c69d48ac06862c1`. +Upstream main inspected: `a5bff3bf133e482541c09eba4e773884bdb2b1b7`. +PySAT: `1.9.dev15`; proof-producing solver: CaDiCaL 1.9.5. +DRAT-trim source: `2e3b2dc0ecf938addbd779d42877b6ed69d9a985`. +LRAT-check source: haskiindahouse's pending +[PR43](https://github.com/marijnheule/drat-trim/pull/43), exact head +`0ca925b4f5b4ed04d02d830807cfd614483e7320`. +[SOURCES.json](SOURCES.json) pins every vendored file and decompressed payload. +Compression headers are not proof-relevant; raw payload hashes are checked. +Source copies and all third-party licenses remain unchanged. + +The original logged solve took approximately 158 seconds. Its complete binary +trace passed DRAT-trim. The original LRAT checker falsely accepted a fake +refutation of a satisfiable formula, reproducing the already reported +[issue42](https://github.com/marijnheule/drat-trim/issues/42). Its positive +output is not relied on. The corrected checker from PR43 rejects that control +and verifies the full target, including fresh LRAT from the archived trimmed +DRAT. This is use of a predecessor correction, not a new checker fix or a +general audit of either checker. Other known malformed-input issues are not +resolved. The exact +commands and results are retained in `logs/` and the final result record. +Finite controls cover all 116 small floor words in three declared parameter +cases, constructive counter extensions and a satisfiable weight-two-only +relaxation of the target. These controls support the written bridge; they are +not its unrestricted proof. See [NOTICE](NOTICE) for detailed attribution. + +## Regenerate the search evidence (optional) + +```sh +timeout 480 python generate.py /tmp/new-connector-c5-run +gcc -std=c99 -O2 vendor/drat-trim/drat-trim.c -o /tmp/drat-trim +/tmp/drat-trim /tmp/new-connector-c5-run/instance.cnf \ + /tmp/new-connector-c5-run/proof.bdrat -i -l /tmp/new-trimmed.drat +``` + +This repeats the costly search with proof logging; it is unnecessary for +certificate replay. Search stopping rule: solve the single pinned instance +or stop after 480 seconds. The solver's deterministic default configuration +was used; no random restarts, larger domain, or characteristic-seven run was +requested. Generated proof bytes need not be identical to this archived trace. +The pinned PySAT native stream needs a C stdio flush before its binary proof +is copied; the optional generator uses POSIX `fflush(NULL)` and tests it on +a tiny actual refutation. Its Linux/POSIX scope is explicit. + +## Open next questions + +The characteristic-six exclusion in PR6141 still needs a checked certificate; +its reported unlogged solve is substantially slower, so budget it separately. +An elementary proof from the weight-two and all-ones constraints would remove +the SAT-encoding/tool trust. Characteristic seven remains outside this visit; +refresh current claims before pursuing it. None of these is an automatic next +cycle. This contribution is ready for scoped external review once the recorded +verification and final code review are complete; acceptance is separate. diff --git a/research/connector-c5-certificate/RESULT.json b/research/connector-c5-certificate/RESULT.json new file mode 100644 index 0000000000..f0c1590b05 --- /dev/null +++ b/research/connector-c5-certificate/RESULT.json @@ -0,0 +1,95 @@ +{ + "status": "checked_finite_refutation", + "claim": "No six-source depth-two restored floor word in characteristic five; already weights two and six cannot all be realized.", + "kind": "Independent verification of PR6141, not a new exclusion claim or kappa.", + "domain": { + "sources": 6, + "characteristic": 5, + "word_length": 30, + "occurrences_per_source": 5, + "mask_weights": [ + 2, + 6 + ], + "masks": 16 + }, + "cnf": { + "variables": 4278, + "clauses": 52672, + "sha256": "2524b48a6ce92066d11be057dd615aac3144988bc73b292901ac17f5302a90bf" + }, + "verification": { + "optimized_archived_replay": { + "clauses": 52672, + "counter_blocks": 12, + "drat_checker_stdout": "\nc parsing input formula with 4278 variables and 52672 clauses\n\nc finished parsing\n\nc detected empty clause; start verification via backward checking\n\nc 33372 of 52672 clauses in core \n\nc 752154 of 769426 lemmas in core using 112379287 resolution steps\n\nc 0 RAT lemmas in core; 0 redundant literals in core lemmas\n\ns VERIFIED\n\nc verification time: 108.550 seconds\n", + "lrat_checker_stdout": "c parsed a formula with 4278 variables and 52672 clauses\nc VERIFIED\nc allocated 1024 1799901 42780\nc Added clauses = 804826. Deleted clauses = 804151. Max live clauses = 63691\nc verification time = 15.91 secs\n", + "native_rejection_controls": 3, + "predecessor_modes": 2, + "status": "PASS_CONNECTOR_C5_CERTIFICATE", + "variables": 4278 + }, + "unit_tests_per_mode": 19, + "modes": [ + "normal", + "optimized" + ], + "small_floor_words": 116, + "counter_extension_assignments": 2568, + "checks_py_unit_coverage_percent": 100, + "proof": "Written word-to-CNF implication plus DRAT and corrected LRAT finite replay", + "kernel_formalization": false, + "human_review": false, + "ai_reviewers": 1, + "known_checker_dependency": "haskiindahouse PR43, pinned unchanged; known issue42 guard correction, not a general checker audit", + "normal_archived_replay": { + "clauses": 52672, + "counter_blocks": 12, + "drat_checker_stdout": "\nc parsing input formula with 4278 variables and 52672 clauses\n\nc finished parsing\n\nc detected empty clause; start verification via backward checking\n\nc 33372 of 52672 clauses in core \n\nc 752154 of 769426 lemmas in core using 112379287 resolution steps\n\nc 0 RAT lemmas in core; 0 redundant literals in core lemmas\n\ns VERIFIED\n\nc verification time: 172.029 seconds\n", + "lrat_checker_stdout": "c parsed a formula with 4278 variables and 52672 clauses\nc VERIFIED\nc allocated 1024 1799901 42780\nc Added clauses = 804826. Deleted clauses = 804151. Max live clauses = 63691\nc verification time = 19.71 secs\n", + "native_rejection_controls": 3, + "predecessor_modes": 2, + "status": "PASS_CONNECTOR_C5_CERTIFICATE", + "variables": 4278 + }, + "combined_python_line_coverage_percent": 93, + "coverage_missing": "generate.py: flush-error and __main__ guard; reproduce.py: selected failure branches and script-level failure handler, with actual corruption failure separately exercised in subprocesses." + }, + "environment": { + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39", + "python": "3.13.15", + "gcc": "13.3.0", + "python_sat": "1.9.dev15" + }, + "search": { + "instances": 1, + "seed": null, + "seed_policy": "No explicit randomization parameter; pinned CaDiCaL195 default configuration", + "stopping_rule": "480 seconds for the single target instance", + "solve_seconds": 157.64589767088182 + }, + "limitations": [ + "Characteristic six and seven not checked", + "No deeper-block or arbitrary-floor-word exclusion", + "No native/physical supplier admission or selected frontier change", + "Both C checker implementations and toolchain remain computational trust; PR43 is pending upstream", + "Known malformed-hint issues in the C checker are not repaired", + "Finite controls are not the unrestricted written encoding proof" + ], + "publication": { + "status": "ready_for_submission", + "accepted": false, + "archival_status": "not_yet_archived" + }, + "attribution": { + "author": "Alexander Richard Towell", + "ai_assistance": "Substantial OpenAI Codex assistance", + "predecessors": [ + "Josie Elliston PR6141", + "Nick Petalas PR4231/4248 and connector lineage", + "haskiindahouse drat-trim PR43", + "Marijn Heule and Nathan Wetzler", + "PySAT, CaDiCaL, Sinz and Knuth/Alex Healy counter lineage" + ] + } +} diff --git a/research/connector-c5-certificate/REVIEW.md b/research/connector-c5-certificate/REVIEW.md new file mode 100644 index 0000000000..3fcf1dc92e --- /dev/null +++ b/research/connector-c5-certificate/REVIEW.md @@ -0,0 +1,30 @@ +# Scoped AI review and response + +One separately tasked OpenAI Codex reviewer inspected PLAN.md, PROOF.md, +checks.py, its tests, the pinned generator and connector definitions, then +the replay/generation wrappers and checker acceptance paths. + +The reviewer found no blocker in the written word-to-CNF implication. It +checked first-occurrence relabeling, weight pruning, boundary 30 to zero, +padding to two readouts, repeated boundaries, all twelve counter blocks and +the disjoint auxiliary IDs 181 through 1680. Independent exact regeneration +matched the 4,278-variable/52,672-clause formula and its recorded SHA256. + +The review found a critical dependency failure: uncorrected lrat-check accepted +CNF `p cnf 1 1 / 1 0` with fake LRAT `2 0 1 0`. The wrapper failed closed; +no successful overall result was reported from that attempt. + +Response: retain the rejecting control, reproduce the failure, and use the +exact existing correction in haskiindahouse's drat-trim PR43, pinned at +0ca925b4f5b4ed04d02d830807cfd614483e7320. Native tests reproduce the known +original failure, verify rejection by the corrected checker, accept a genuine +tiny refutation and reject an empty proof. The full target was replayed with +the corrected source. Original vendor files are unchanged; no novel checker +fix is claimed. The author performed the final verification of this response; +a second reviewer or repeated whole-branch AI review was not used. + +Scope: written implication and scoped code review supported by finite controls. +Neither reviewer nor author establishes formal correctness of the C checkers, +general malformed-input safety, human peer review, novelty, or the full +integer-multiplication theorem. DRAT verification and corrected LRAT verification +remain distinct recorded computational evidence. diff --git a/research/connector-c5-certificate/SOURCES.json b/research/connector-c5-certificate/SOURCES.json new file mode 100644 index 0000000000..1a52414211 --- /dev/null +++ b/research/connector-c5-certificate/SOURCES.json @@ -0,0 +1,57 @@ +{ + "workspace_base": "b6892c8f8c7e060031f8b103f5a8c4bcc7ac8690", + "upstream_main": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "predecessor_head": "d192172f57b10647ddcff9410c69d48ac06862c1", + "predecessor_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6141", + "checker_head": "2e3b2dc0ecf938addbd779d42877b6ed69d9a985", + "checker_repository": "https://github.com/marijnheule/drat-trim", + "counter_reference": "https://github.com/pysathq/pysat/blob/5c6d801fb1fae958f6504af5692fa26b807c8e76/cardenc/seqcounter.hh", + "vendored_files": [ + { + "path": "vendor/connector-depth-blocks-README.md", + "sha256": "0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331" + }, + { + "path": "vendor/drat-trim/LICENSE", + "sha256": "71ab2a9dc5a294ad8fba4ccb8c45aaa8a439596d314a2a046ac9b62266872a18" + }, + { + "path": "vendor/drat-trim/drat-trim.c", + "sha256": "d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee" + }, + { + "path": "vendor/drat-trim/lrat-check.c", + "sha256": "bf07c2ac96b9035da1ebcc578cb95e956a2b795629d613154cdb307f8a8f4a95" + }, + { + "path": "vendor/search_sat.py", + "sha256": "3d4f11fed6b59830b47ad43c0746627ccbbb5ba571d32e5fe1a502e8decb15f3" + }, + { + "path": "vendor/verify.py", + "sha256": "569194e1577692f6049dedc13aeecdeb321152b3a77a143990a8c8fcba53f87f" + }, + { + "path": "vendor/lrat-check-pr43.c", + "sha256": "5be448c56add986683794c536161a54c39ab13cc42228f045cdf8071e3bfcf5b" + } + ], + "payloads": [ + { + "name": "instance.cnf", + "archive": "artifacts/instance.cnf.gz", + "bytes": 972233, + "sha256": "2524b48a6ce92066d11be057dd615aac3144988bc73b292901ac17f5302a90bf" + }, + { + "name": "trimmed.drat", + "archive": "artifacts/trimmed.drat.gz", + "bytes": 276652282, + "sha256": "47f4fb2d78e06ac0320a1b14e68404c82691827b3511adab82cc40126c40402f" + } + ], + "corrected_lrat_head": "0ca925b4f5b4ed04d02d830807cfd614483e7320", + "corrected_lrat_author": "haskiindahouse", + "corrected_lrat_url": "https://github.com/marijnheule/drat-trim/pull/43", + "known_lrat_issue": "https://github.com/marijnheule/drat-trim/issues/42" +} diff --git a/research/connector-c5-certificate/artifacts/instance.cnf.gz b/research/connector-c5-certificate/artifacts/instance.cnf.gz new file mode 100644 index 0000000000..ce45517563 Binary files /dev/null and b/research/connector-c5-certificate/artifacts/instance.cnf.gz differ diff --git a/research/connector-c5-certificate/artifacts/trimmed.drat.gz b/research/connector-c5-certificate/artifacts/trimmed.drat.gz new file mode 100644 index 0000000000..b1233d0d30 Binary files /dev/null and b/research/connector-c5-certificate/artifacts/trimmed.drat.gz differ diff --git a/research/connector-c5-certificate/checks.py b/research/connector-c5-certificate/checks.py new file mode 100644 index 0000000000..c9d8d8972a --- /dev/null +++ b/research/connector-c5-certificate/checks.py @@ -0,0 +1,130 @@ +"""Constructive audit of the predecessor's anonymous cardinality variables. + +Owned code: Alexander Richard Towell, substantial OpenAI Codex assistance. +Apache-2.0. The reconstructed counter is Knuth's irredundant sequential +encoding as implemented by PySAT; this is not a new cardinality algorithm. +""" +from pathlib import Path +import importlib.util + + +def build_instance(k=6, c=5, weights=frozenset({2, 6})): + path = Path(__file__).parent / 'vendor' / 'search_sat.py' + spec = importlib.util.spec_from_file_location('pinned_connector_search', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + cnf, pool, _ = module.build(k, c, True, weights) + return cnf, pool + + +def at_most(literals, bound, top): + """Return clauses, last ID, and constructive semantics for counter variables. + + y[k,j] means >= k+1 true literals among literals[:j+k+1]. This meaning + satisfies every clause whenever the whole input has <= bound true literals. + This routine covers 1 <= bound < len(literals)-1, the only target cases. + """ + if not 1 <= bound < len(literals) - 1: + raise ValueError('counter bound outside audited interior domain') + variables = {} + meaning = [] + clauses = [] + + def y(k, j): + nonlocal top + if (k, j) not in variables: + top += 1 + variables[k, j] = top + meaning.append((top, tuple(literals[:j + k + 1]), k + 1)) + return variables[k, j] + + rows = len(literals) - bound + for j in range(rows): + clauses.append([-literals[j], y(0, j)]) + for k in range(bound - 1): + a = y(k, j) + if j < rows - 1: + clauses.append([-a, y(k, j + 1)]) + clauses.append([-literals[j + k + 1], -a, y(k + 1, j)]) + a = y(bound - 1, j) + if j < rows - 1: + clauses.append([-a, y(bound - 1, j + 1)]) + clauses.append([-literals[j + bound], -a]) + return clauses, top, meaning + + +def satisfied(clauses, assignment): + return all(any(assignment[abs(x)] == (x > 0) for x in clause) + for clause in clauses) + + +def audit_counter_bridge(cnf, pool): + """Compare every target cardinality clause with the explained construction.""" + k, c = 6, 5 + length = k * c + offset = length * (1 + k * (k - 1) // 2) + top = length * k + for j in range(k): + xs = [pool.id(('x', p, j)) for p in range(length)] + for literals, bound in [([-x for x in xs], length - c), (xs, c)]: + clauses, top, _ = at_most(literals, bound, top) + if cnf.clauses[offset:offset + len(clauses)] != clauses: + raise ValueError('cardinality bridge differs from pinned generator') + offset += len(clauses) + return k + + +def normalize(word): + """Relabel by first occurrence, as allowed by the invariant mask family.""" + labels = {} + return [labels.setdefault(x, len(labels)) for x in word] + + +def word_assignment(word, k, c, pool): + """Construct every variable from a canonical floor word; no SAT solver.""" + if len(word) != k * c or any(word.count(j) != c for j in range(k)): + raise ValueError('not a floor word') + if normalize(word) != list(word): + raise ValueError('word must be relabeled by first occurrence') + counts = [0] * k + prefixes = [tuple(counts)] + for j in word: + counts[j] += 1 + prefixes.append(tuple(counts)) + assignment = {} + for var, obj in pool.id2obj.items(): + match obj: + case ('x', p, j): + value = word[p] == j + case ('e', t, j, v): + value = prefixes[t][j] % c == v + case ('f', p, j): + value = prefixes[p + 1][j] > 0 + case ('y', mask, s, t): + value = all((prefixes[s][j] + prefixes[t][j]) % c == + ((mask >> j) & 1) for j in range(k)) + case _: + raise ValueError('unexpected generator variable') + assignment[var] = value + top = len(word) * k + for j in range(k): + xs = [pool.id(('x', p, j)) for p in range(len(word))] + for literals, bound in [([-x for x in xs], len(word) - c), (xs, c)]: + _, top, meaning = at_most(literals, bound, top) + for var, prefix, threshold in meaning: + assignment[var] = sum(assignment[abs(x)] == (x > 0) + for x in prefix) >= threshold + return assignment + + +def covers(word, k, c, weights): + """Literal integer-prefix check, independent of CNF and its variables.""" + counts = [0] * k + prefixes = [tuple(counts)] + for j in word: + counts[j] += 1 + prefixes.append(tuple(counts)) + seen = {tuple((a + b) % c for a, b in zip(s, t)) + for i, s in enumerate(prefixes) for t in prefixes[i:]} + return all(tuple((mask >> j) & 1 for j in range(k)) in seen + for mask in range(1, 1 << k) if mask.bit_count() in weights) diff --git a/research/connector-c5-certificate/generate.py b/research/connector-c5-certificate/generate.py new file mode 100644 index 0000000000..022e2c2f4f --- /dev/null +++ b/research/connector-c5-certificate/generate.py @@ -0,0 +1,61 @@ +"""Regenerate the target and binary DRAT with pinned python-sat (costly). + +This is not needed for archived LRAT replay. Proof bytes may vary across +solver/compiler versions; correctness comes from replay against the exact CNF. +""" +import argparse +import ctypes +import hashlib +import json +import shutil +import time +from importlib.metadata import version +from pathlib import Path + +from checks import build_instance, audit_counter_bridge + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('output', type=Path, help='new or empty output directory') + args = parser.parse_args() + if version('python-sat') != '1.9.dev15': + raise SystemExit('requires python-sat==1.9.dev15') + args.output.mkdir(parents=True, exist_ok=True) + if any(args.output.iterdir()): + raise SystemExit('output directory must be empty') + from pysat.solvers import Solver + cnf, pool = build_instance() + audit_counter_bridge(cnf, pool) + cnf_path = args.output / 'instance.cnf' + cnf.to_file(str(cnf_path)) + start = time.monotonic() + with Solver(name='cadical195', bootstrap_with=cnf.clauses, with_proof=True) as s: + if s.solve(): + raise SystemExit('unexpected SAT; no exclusion established') + solve_seconds = time.monotonic() - start + # Python's flush does not flush the native wrapper's separate FILE*. + # fflush(NULL) is the POSIX/C interface for flushing output streams. + libc = ctypes.CDLL(None) + libc.fflush.argtypes = [ctypes.c_void_p] + libc.fflush.restype = ctypes.c_int + if libc.fflush(None) != 0: + raise OSError('native proof stream flush failed') + # Pinned PySAT wrapper exposes its binary proof file here. Avoid + # get_proof(), which expands the trace into millions of Python strings. + proof = s.solver.prfile + proof.flush() + proof.seek(0) + with (args.output / 'proof.bdrat').open('wb') as out: + shutil.copyfileobj(proof, out) + receipt = {'solver': 'cadical195', 'python_sat': version('python-sat'), + 'solve_seconds': solve_seconds, 'variables': cnf.nv, + 'clauses': len(cnf.clauses), + 'sha256': {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in [cnf_path, args.output / 'proof.bdrat']}} + (args.output / 'generation.json').write_text(json.dumps(receipt, indent=2) + '\n') + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/connector-c5-certificate/logs/claim.json b/research/connector-c5-certificate/logs/claim.json new file mode 100644 index 0000000000..710ed026ac --- /dev/null +++ b/research/connector-c5-certificate/logs/claim.json @@ -0,0 +1 @@ +{"data":{"addDiscussionComment":{"comment":{"id":"DC_kwDOU-508s4BJiJp","url":"https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19276393"}}}} \ No newline at end of file diff --git a/research/connector-c5-certificate/logs/coverage.txt b/research/connector-c5-certificate/logs/coverage.txt new file mode 100644 index 0000000000..abd9b53dc9 --- /dev/null +++ b/research/connector-c5-certificate/logs/coverage.txt @@ -0,0 +1,7 @@ +Name Stmts Miss Cover Missing +-------------------------------------------- +checks.py 92 0 100% +generate.py 43 2 95% 43, 61 +reproduce.py 85 13 85% 35, 41, 45, 53, 58, 66, 78, 82, 87, 101, 113-115 +-------------------------------------------- +TOTAL 220 15 93% diff --git a/research/connector-c5-certificate/logs/drat-trim.txt b/research/connector-c5-certificate/logs/drat-trim.txt new file mode 100644 index 0000000000..ba9444b526 --- /dev/null +++ b/research/connector-c5-certificate/logs/drat-trim.txt @@ -0,0 +1,9 @@ + c turning on binary mode checking + c parsing input formula with 4278 variables and 52672 clauses + c finished parsing, read 346843737 bytes from proof file + c detected empty clause; start verification via backward checking + c 33290 of 52672 clauses in core + c 769425 of 2801469 lemmas in core using 113364941 resolution steps + c 0 RAT lemmas in core; 0 redundant literals in core lemmas + s VERIFIED + c verification time: 215.749 seconds diff --git a/research/connector-c5-certificate/logs/generation.txt b/research/connector-c5-certificate/logs/generation.txt new file mode 100644 index 0000000000..1628c8feac --- /dev/null +++ b/research/connector-c5-certificate/logs/generation.txt @@ -0,0 +1,3 @@ +{"variables": 4278, "clauses": 52672, "sha256": "2524b48a6ce92066d11be057dd615aac3144988bc73b292901ac17f5302a90bf", "python": "3.13.15", "python_sat": "1.9.dev15"} +SAT False elapsed 157.64589767088182 +{"lines": 5600439, "bytes": 872354535, "sha256": "4dfe0c811cf769c2095f2a566b358db07222269c84d626d4f799dce08083d3c5", "elapsed": 234.7951138948556} diff --git a/research/connector-c5-certificate/logs/lrat-check.txt b/research/connector-c5-certificate/logs/lrat-check.txt new file mode 100644 index 0000000000..6c396d9698 --- /dev/null +++ b/research/connector-c5-certificate/logs/lrat-check.txt @@ -0,0 +1,5 @@ +c parsed a formula with 4278 variables and 52672 clauses +c VERIFIED +c allocated 1024 1799901 42780 +c Added clauses = 822097. Deleted clauses = 821420. Max live clauses = 66534 +c verification time = 21.32 secs diff --git a/research/connector-c5-certificate/logs/lrat-fixed-target.txt b/research/connector-c5-certificate/logs/lrat-fixed-target.txt new file mode 100644 index 0000000000..79184b7619 --- /dev/null +++ b/research/connector-c5-certificate/logs/lrat-fixed-target.txt @@ -0,0 +1,5 @@ +c parsed a formula with 4278 variables and 52672 clauses +c VERIFIED +c allocated 1024 1799901 42780 +c Added clauses = 822097. Deleted clauses = 821420. Max live clauses = 66534 +c verification time = 18.54 secs diff --git a/research/connector-c5-certificate/logs/reproduce-fixed-optimized.json b/research/connector-c5-certificate/logs/reproduce-fixed-optimized.json new file mode 100644 index 0000000000..485dbc3cf2 --- /dev/null +++ b/research/connector-c5-certificate/logs/reproduce-fixed-optimized.json @@ -0,0 +1 @@ +{"clauses": 52672, "counter_blocks": 12, "drat_checker_stdout": "\nc parsing input formula with 4278 variables and 52672 clauses\n\nc finished parsing\n\nc detected empty clause; start verification via backward checking\n\nc 33372 of 52672 clauses in core \n\nc 752154 of 769426 lemmas in core using 112379287 resolution steps\n\nc 0 RAT lemmas in core; 0 redundant literals in core lemmas\n\ns VERIFIED\n\nc verification time: 97.384 seconds\n", "lrat_checker_stdout": "c parsed a formula with 4278 variables and 52672 clauses\nc VERIFIED\nc allocated 1024 1799901 42780\nc Added clauses = 804826. Deleted clauses = 804151. Max live clauses = 63691\nc verification time = 16.30 secs\n", "native_rejection_controls": 3, "predecessor_modes": 2, "status": "PASS_CONNECTOR_C5_CERTIFICATE", "variables": 4278} diff --git a/research/connector-c5-certificate/logs/reproduce-fixed-optimized.stderr b/research/connector-c5-certificate/logs/reproduce-fixed-optimized.stderr new file mode 100644 index 0000000000..e69de29bb2 diff --git a/research/connector-c5-certificate/logs/reproduce-normal.json b/research/connector-c5-certificate/logs/reproduce-normal.json new file mode 100644 index 0000000000..72d54a48b9 --- /dev/null +++ b/research/connector-c5-certificate/logs/reproduce-normal.json @@ -0,0 +1 @@ +{"clauses": 52672, "counter_blocks": 12, "drat_checker_stdout": "\nc parsing input formula with 4278 variables and 52672 clauses\n\nc finished parsing\n\nc detected empty clause; start verification via backward checking\n\nc 33372 of 52672 clauses in core \n\nc 752154 of 769426 lemmas in core using 112379287 resolution steps\n\nc 0 RAT lemmas in core; 0 redundant literals in core lemmas\n\ns VERIFIED\n\nc verification time: 172.029 seconds\n", "lrat_checker_stdout": "c parsed a formula with 4278 variables and 52672 clauses\nc VERIFIED\nc allocated 1024 1799901 42780\nc Added clauses = 804826. Deleted clauses = 804151. Max live clauses = 63691\nc verification time = 19.71 secs\n", "native_rejection_controls": 3, "predecessor_modes": 2, "status": "PASS_CONNECTOR_C5_CERTIFICATE", "variables": 4278} diff --git a/research/connector-c5-certificate/logs/reproduce-normal.stderr b/research/connector-c5-certificate/logs/reproduce-normal.stderr new file mode 100644 index 0000000000..aa216a6711 --- /dev/null +++ b/research/connector-c5-certificate/logs/reproduce-normal.stderr @@ -0,0 +1,2 @@ +/tmp/connector-c5-env-20261029/lib/python3.13/site-packages/coverage/inorout.py:558: CoverageWarning: Module generate was never imported. (module-not-imported); see https://coverage.readthedocs.io/en/7.17.0/messages.html#warning-module-not-imported + self.warn(f"Module {pkg} was never imported.", slug="module-not-imported") diff --git a/research/connector-c5-certificate/logs/reproduce-optimized.json b/research/connector-c5-certificate/logs/reproduce-optimized.json new file mode 100644 index 0000000000..e69de29bb2 diff --git a/research/connector-c5-certificate/logs/reproduce-optimized.stderr b/research/connector-c5-certificate/logs/reproduce-optimized.stderr new file mode 100644 index 0000000000..6ce9039f80 --- /dev/null +++ b/research/connector-c5-certificate/logs/reproduce-optimized.stderr @@ -0,0 +1 @@ +FAIL: satisfiable formula falsely refuted diff --git a/research/connector-c5-certificate/logs/reproduce-pr43-optimized.json b/research/connector-c5-certificate/logs/reproduce-pr43-optimized.json new file mode 100644 index 0000000000..4900ab36a8 --- /dev/null +++ b/research/connector-c5-certificate/logs/reproduce-pr43-optimized.json @@ -0,0 +1 @@ +{"clauses": 52672, "counter_blocks": 12, "drat_checker_stdout": "\nc parsing input formula with 4278 variables and 52672 clauses\n\nc finished parsing\n\nc detected empty clause; start verification via backward checking\n\nc 33372 of 52672 clauses in core \n\nc 752154 of 769426 lemmas in core using 112379287 resolution steps\n\nc 0 RAT lemmas in core; 0 redundant literals in core lemmas\n\ns VERIFIED\n\nc verification time: 108.550 seconds\n", "lrat_checker_stdout": "c parsed a formula with 4278 variables and 52672 clauses\nc VERIFIED\nc allocated 1024 1799901 42780\nc Added clauses = 804826. Deleted clauses = 804151. Max live clauses = 63691\nc verification time = 15.91 secs\n", "native_rejection_controls": 3, "predecessor_modes": 2, "status": "PASS_CONNECTOR_C5_CERTIFICATE", "variables": 4278} diff --git a/research/connector-c5-certificate/logs/reproduce-pr43-optimized.stderr b/research/connector-c5-certificate/logs/reproduce-pr43-optimized.stderr new file mode 100644 index 0000000000..e69de29bb2 diff --git a/research/connector-c5-certificate/logs/tests-normal.txt b/research/connector-c5-certificate/logs/tests-normal.txt new file mode 100644 index 0000000000..bebc07c58b --- /dev/null +++ b/research/connector-c5-certificate/logs/tests-normal.txt @@ -0,0 +1,4 @@ +---------------------------------------------------------------------- +Ran 19 tests in 1.558s + +OK diff --git a/research/connector-c5-certificate/logs/tests-optimized.txt b/research/connector-c5-certificate/logs/tests-optimized.txt new file mode 100644 index 0000000000..bbe1764460 --- /dev/null +++ b/research/connector-c5-certificate/logs/tests-optimized.txt @@ -0,0 +1,4 @@ +---------------------------------------------------------------------- +Ran 19 tests in 1.486s + +OK diff --git a/research/connector-c5-certificate/logs/trimmed-check.txt b/research/connector-c5-certificate/logs/trimmed-check.txt new file mode 100644 index 0000000000..45d43c16c4 --- /dev/null +++ b/research/connector-c5-certificate/logs/trimmed-check.txt @@ -0,0 +1,8 @@ + c parsing input formula with 4278 variables and 52672 clauses + c finished parsing + c detected empty clause; start verification via backward checking + c 33372 of 52672 clauses in core + c 752154 of 769426 lemmas in core using 112379287 resolution steps + c 0 RAT lemmas in core; 1395199 redundant literals in core lemmas + s VERIFIED + c verification time: 103.756 seconds diff --git a/research/connector-c5-certificate/reproduce.py b/research/connector-c5-certificate/reproduce.py new file mode 100644 index 0000000000..adf48fdd7d --- /dev/null +++ b/research/connector-c5-certificate/reproduce.py @@ -0,0 +1,115 @@ +"""Replay the archived finite refutation; never rerun the expensive SAT search.""" +import gzip +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from importlib.metadata import version +from pathlib import Path + +from checks import audit_counter_bridge, build_instance + +ROOT = Path(__file__).resolve().parent + + +def digest(path): + value = hashlib.sha256() + with path.open('rb') as stream: + for block in iter(lambda: stream.read(1024 * 1024), b''): + value.update(block) + return value.hexdigest() + + +def accepted(result, marker): + return result.returncode == 0 and marker in result.stdout.splitlines() + + +def run(command, timeout=300): + return subprocess.run(command, capture_output=True, text=True, timeout=timeout) + + +def require(result, marker): + if not accepted(result, marker): + raise ValueError('native replay did not verify: ' + result.stdout[-2000:] + + result.stderr[-2000:]) + + +def main(): + if version('python-sat') != '1.9.dev15': + raise ValueError('requires python-sat==1.9.dev15') + manifest = json.loads((ROOT / 'SOURCES.json').read_text()) + for row in manifest['vendored_files']: + if digest(ROOT / row['path']) != row['sha256']: + raise ValueError('source pin mismatch: ' + row['path']) + with tempfile.TemporaryDirectory(prefix='connector-c5-replay-') as directory: + temp = Path(directory) + for row in manifest['payloads']: + destination = temp / row['name'] + with gzip.open(ROOT / row['archive'], 'rb') as src, destination.open('wb') as dst: + shutil.copyfileobj(src, dst) + if digest(destination) != row['sha256']: + raise ValueError('certificate payload mismatch: ' + row['name']) + cnf, pool = build_instance() + audit_counter_bridge(cnf, pool) + cnf.to_file(str(temp / 'regenerated.cnf')) + if (temp / 'regenerated.cnf').read_bytes() != (temp / 'instance.cnf').read_bytes(): + raise ValueError('pinned generator does not reproduce certified formula') + for name, flags in [('drat-trim', []), ('lrat-check', ['-DLONGTYPE'])]: + source = (ROOT / 'vendor/lrat-check-pr43.c' if name == 'lrat-check' else + ROOT / 'vendor/drat-trim/drat-trim.c') + compiled = run(['gcc', '-std=c99', *flags, '-O2', + str(source), + '-o', str(temp / name)], 60) + if compiled.returncode: + raise ValueError('checker compilation failed: ' + compiled.stderr) + drat = run([str(temp / 'drat-trim'), str(temp / 'instance.cnf'), + str(temp / 'trimmed.drat'), '-L', str(temp / 'proof.lrat')]) + require(drat, 's VERIFIED') + executable = temp / 'lrat-check' + actual = run([str(executable), str(temp / 'instance.cnf'), str(temp / 'proof.lrat')]) + require(actual, 'c VERIFIED') + + # A genuine refutation is required, not merely an UNSAT verdict or file. + (temp / 'empty.lrat').write_text('') + empty = run([str(executable), str(temp / 'instance.cnf'), str(temp / 'empty.lrat')]) + if accepted(empty, 'c VERIFIED'): + raise ValueError('empty certificate accepted') + (temp / 'fake.lrat').write_text('52673 0 1 0\n') + fake = run([str(executable), str(temp / 'instance.cnf'), str(temp / 'fake.lrat')]) + if accepted(fake, 'c VERIFIED'): + raise ValueError('unsupported empty-clause derivation accepted') + (temp / 'sat.cnf').write_text('p cnf 1 1\n1 0\n') + (temp / 'sat-fake.lrat').write_text('2 0 1 0\n') + sat = run([str(executable), str(temp / 'sat.cnf'), str(temp / 'sat-fake.lrat')]) + if accepted(sat, 'c VERIFIED'): + raise ValueError('satisfiable formula falsely refuted') + + # Replay the predecessor's original word controls without modifying it. + stage = temp / 'predecessor' + package = stage / 'research/connector-six-source-small-char' + interface = stage / 'research/connector-depth-blocks' + package.mkdir(parents=True) + interface.mkdir(parents=True) + shutil.copyfile(ROOT / 'vendor/verify.py', package / 'verify.py') + shutil.copyfile(ROOT / 'vendor/connector-depth-blocks-README.md', interface / 'README.md') + for flags in [[], ['-O']]: + result = run([sys.executable, *flags, '-B', str(package / 'verify.py')], 60) + if result.returncode or not any(line.startswith('PASS_CONNECTOR_SIX_SOURCE_SMALL_CHAR ') + for line in result.stdout.splitlines()): + raise ValueError('predecessor control replay failed') + print(json.dumps({'status': 'PASS_CONNECTOR_C5_CERTIFICATE', + 'variables': cnf.nv, 'clauses': len(cnf.clauses), + 'counter_blocks': 12, 'native_rejection_controls': 3, + 'predecessor_modes': 2, + 'drat_checker_stdout': drat.stdout, + 'lrat_checker_stdout': actual.stdout}, sort_keys=True)) + + +if __name__ == '__main__': + try: + main() + except (ValueError, OSError, subprocess.SubprocessError) as error: + print('FAIL: ' + str(error), file=sys.stderr) + raise SystemExit(2) diff --git a/research/connector-c5-certificate/requirements.txt b/research/connector-c5-certificate/requirements.txt new file mode 100644 index 0000000000..dc77fc84b9 --- /dev/null +++ b/research/connector-c5-certificate/requirements.txt @@ -0,0 +1,2 @@ +python-sat==1.9.dev15 +six==1.17.0 diff --git a/research/connector-c5-certificate/test_checks.py b/research/connector-c5-certificate/test_checks.py new file mode 100644 index 0000000000..f1bd1e4a02 --- /dev/null +++ b/research/connector-c5-certificate/test_checks.py @@ -0,0 +1,79 @@ +import itertools +import unittest + +from checks import (at_most, satisfied, audit_counter_bridge, build_instance, + normalize, word_assignment, covers) + + +class EncodingTests(unittest.TestCase): + def test_constructive_counter_extension(self): + for n in range(2, 9): + for bound in range(1, n - 1): + literals = list(range(1, n + 1)) + clauses, top, meaning = at_most(literals, bound, n) + for bits in itertools.product((False, True), repeat=n): + assignment = dict(zip(literals, bits)) + for var, prefix, threshold in meaning: + assignment[var] = sum(assignment[abs(x)] == (x > 0) + for x in prefix) >= threshold + self.assertEqual(satisfied(clauses, assignment), sum(bits) <= bound) + self.assertEqual(len(assignment), top) + + def test_target_matches_predecessor(self): + cnf, pool = build_instance() + self.assertEqual((cnf.nv, len(cnf.clauses)), (4278, 52672)) + self.assertEqual(audit_counter_bridge(cnf, pool), 6) + + def test_bad_counter_clause_rejected(self): + cnf, pool = build_instance() + cnf.clauses[480][0] *= -1 + with self.assertRaises(ValueError): + audit_counter_bridge(cnf, pool) + + def test_wrong_signed_extension_rejected(self): + clauses, _, meaning = at_most([-1, -2, -3, -4], 2, 4) + a = {1: False, 2: False, 3: True, 4: True} + for var, prefix, threshold in meaning: + a[var] = sum(a[abs(x)] == (x > 0) for x in prefix) >= threshold + self.assertTrue(satisfied(clauses, a)) + a[meaning[0][0]] = not a[meaning[0][0]] + self.assertFalse(satisfied(clauses, a)) + + def test_exhaustive_small_floor_words(self): + for k, c in [(2, 2), (2, 3), (3, 2)]: + weights = frozenset(range(1, k + 1)) + cnf, pool = build_instance(k, c, weights) + for word in itertools.product(range(k), repeat=k * c): + if any(word.count(j) != c for j in range(k)): + continue + word = normalize(word) + a = word_assignment(word, k, c, pool) + self.assertEqual(satisfied(cnf.clauses, a), covers(word, k, c, weights)) + + def test_target_relaxation_has_constructive_sat_word(self): + word = [j for j in range(6) for _ in range(5)] + cnf, pool = build_instance(6, 5, {2}) + self.assertTrue(covers(word, 6, 5, {2})) + self.assertTrue(satisfied(cnf.clauses, word_assignment(word, 6, 5, pool))) + self.assertFalse(covers(word, 6, 5, {2, 6})) + + def test_invalid_word_rejected(self): + _, pool = build_instance(2, 2, {1, 2}) + for word in [[0, 0, 0, 1], [1, 1, 0, 0]]: + with self.assertRaises(ValueError): + word_assignment(word, 2, 2, pool) + + def test_invalid_counter_domain_rejected(self): + for bound in [0, 3, 4]: + with self.assertRaises(ValueError): + at_most([1, 2, 3, 4], bound, 4) + + def test_unexpected_variable_rejected(self): + _, pool = build_instance(2, 2, {1, 2}) + pool.id(('unrecognized',)) + with self.assertRaises(ValueError): + word_assignment([0, 0, 1, 1], 2, 2, pool) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/connector-c5-certificate/test_generate.py b/research/connector-c5-certificate/test_generate.py new file mode 100644 index 0000000000..f9645db2d0 --- /dev/null +++ b/research/connector-c5-certificate/test_generate.py @@ -0,0 +1,51 @@ +import contextlib +import io +import json +import sys +import tempfile +import unittest +from pathlib import Path +from unittest.mock import patch + +from pysat.formula import CNF + +import generate + + +class GenerationTests(unittest.TestCase): + def test_binary_proof_writer_on_real_tiny_unsat(self): + cnf = CNF(from_clauses=[[1, 2], [1, -2], [-1, 2], [-1, -2]]) + with tempfile.TemporaryDirectory() as directory: + output = Path(directory) / 'run' + with patch.object(sys, 'argv', ['generate.py', str(output)]), \ + patch.object(generate, 'build_instance', return_value=(cnf, None)), \ + patch.object(generate, 'audit_counter_bridge'), \ + contextlib.redirect_stdout(io.StringIO()): + generate.main() + receipt = json.loads((output / 'generation.json').read_text()) + self.assertEqual((receipt['variables'], receipt['clauses']), (2, 4)) + self.assertGreater((output / 'proof.bdrat').stat().st_size, 0) + self.assertEqual((output / 'instance.cnf').read_text().splitlines()[0], 'p cnf 2 4') + + def test_nonempty_directory_and_version_rejected(self): + with tempfile.TemporaryDirectory() as directory: + Path(directory, 'existing').touch() + for version in ['1.9.dev15', 'other']: + with patch.object(sys, 'argv', ['generate.py', directory]), \ + patch.object(generate, 'version', return_value=version), \ + self.assertRaises(SystemExit): + generate.main() + + def test_sat_does_not_produce_exclusion(self): + cnf = CNF(from_clauses=[[1]]) + with tempfile.TemporaryDirectory() as directory: + with patch.object(sys, 'argv', ['generate.py', str(Path(directory) / 'run')]), \ + patch.object(generate, 'build_instance', return_value=(cnf, None)), \ + patch.object(generate, 'audit_counter_bridge'), \ + self.assertRaises(SystemExit): + generate.main() + self.assertFalse((Path(directory) / 'run/proof.bdrat').exists()) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/connector-c5-certificate/test_native.py b/research/connector-c5-certificate/test_native.py new file mode 100644 index 0000000000..a0cc4fbeec --- /dev/null +++ b/research/connector-c5-certificate/test_native.py @@ -0,0 +1,59 @@ +"""Native regression for known drat-trim issue42 and predecessor fix PR43.""" +import subprocess +import tempfile +import unittest +from pathlib import Path + +from reproduce import accepted + +ROOT = Path(__file__).resolve().parent + + +class NativeCheckerTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.directory = tempfile.TemporaryDirectory() + cls.temp = Path(cls.directory.name) + for name, source in [('original', ROOT / 'vendor/drat-trim/lrat-check.c'), + ('corrected', ROOT / 'vendor/lrat-check-pr43.c')]: + built = subprocess.run(['gcc', '-std=c99', '-DLONGTYPE', '-O2', str(source), + '-o', str(cls.temp / name)], + capture_output=True, text=True, timeout=60) + if built.returncode: + raise RuntimeError(built.stderr) + (cls.temp / 'sat.cnf').write_text('p cnf 1 1\n1 0\n') + (cls.temp / 'fake.lrat').write_text('2 0 1 0\n') + (cls.temp / 'no-hint.lrat').write_text('2 0 0\n') + (cls.temp / 'unsat.cnf').write_text('p cnf 2 4\n1 2 0\n1 -2 0\n-1 2 0\n-1 -2 0\n') + (cls.temp / 'valid.lrat').write_text('5 1 0 1 2 0\n6 0 5 3 4 0\n') + (cls.temp / 'empty.lrat').write_text('') + + @classmethod + def tearDownClass(cls): + cls.directory.cleanup() + + def check(self, checker, cnf, proof): + return subprocess.run([str(self.temp / checker), str(self.temp / cnf), + str(self.temp / proof)], + capture_output=True, text=True, timeout=20) + + def test_original_false_acceptance_is_reproduced(self): + # Known issue42, not a claim of a newly discovered vulnerability. + self.assertTrue(accepted(self.check('original', 'sat.cnf', 'fake.lrat'), 'c VERIFIED')) + + def test_corrected_checker_rejects_fake_refutations(self): + for proof in ['fake.lrat', 'no-hint.lrat']: + result = self.check('corrected', 'sat.cnf', proof) + self.assertFalse(accepted(result, 'c VERIFIED')) + self.assertEqual(result.returncode, 1) + self.assertIn('c NOT VERIFIED', result.stdout) + + def test_corrected_checker_accepts_valid_refutation(self): + self.assertTrue(accepted(self.check('corrected', 'unsat.cnf', 'valid.lrat'), 'c VERIFIED')) + + def test_corrected_checker_rejects_empty_proof(self): + self.assertFalse(accepted(self.check('corrected', 'unsat.cnf', 'empty.lrat'), 'c VERIFIED')) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/connector-c5-certificate/test_reproduce.py b/research/connector-c5-certificate/test_reproduce.py new file mode 100644 index 0000000000..ee3bd7cadd --- /dev/null +++ b/research/connector-c5-certificate/test_reproduce.py @@ -0,0 +1,42 @@ +import subprocess +import shutil +import sys +import tempfile +import unittest +from pathlib import Path + +from reproduce import accepted + + +class AcceptanceTests(unittest.TestCase): + def test_exact_success(self): + self.assertTrue(accepted(subprocess.CompletedProcess([], 0, 'c VERIFIED\n', ''), + 'c VERIFIED')) + + def test_exit_status_and_exact_line_required(self): + for status, output in [(1, 'c VERIFIED\n'), (0, 'c NOT VERIFIED\n'), + (0, 'prefix c VERIFIED\n'), (0, '')]: + self.assertFalse(accepted(subprocess.CompletedProcess([], status, output, ''), + 'c VERIFIED')) + + def test_cli_rejects_source_corruption_in_both_modes(self): + root = Path(__file__).resolve().parent + with tempfile.TemporaryDirectory() as directory: + stage = Path(directory) + for name in ['reproduce.py', 'checks.py', 'SOURCES.json']: + shutil.copyfile(root / name, stage / name) + shutil.copytree(root / 'vendor', stage / 'vendor', + ignore=shutil.ignore_patterns('__pycache__')) + with (stage / 'vendor/search_sat.py').open('a') as stream: + stream.write('\n# deliberately corrupted source pin\n') + for flags in [[], ['-O']]: + result = subprocess.run([sys.executable, *flags, '-B', + str(stage / 'reproduce.py')], + capture_output=True, text=True, timeout=20) + self.assertEqual(result.returncode, 2) + self.assertEqual(result.stdout, '') + self.assertIn('source pin mismatch', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/connector-c5-certificate/vendor/connector-depth-blocks-README.md b/research/connector-c5-certificate/vendor/connector-depth-blocks-README.md new file mode 100644 index 0000000000..5d5b4a5b96 --- /dev/null +++ b/research/connector-c5-certificate/vendor/connector-depth-blocks-README.md @@ -0,0 +1,195 @@ +# Unsigned connector: depth blocks reach the floor for k ≤ 2c + +Take the unsigned dirty connector over a ring of characteristic c ≥ 2, with k +immutable sources and all 2^k − 1 nonzero binary-mask outputs. Every legal word +needs at least c(k + 2^k − 1) complete calls +([#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231)). Let N(c) +be the largest k at which that floor is attained. This package shows: + +- **Theorem A** (proof, checked for c ≤ 7): N(c) ≥ 2c for every c ≥ 2. + Concatenated two-source blocks give the floor word. This improves #4231's + run walk, which reaches k ≤ c. +- **Lemma C** (proof, exhaustive control at k = 3): a block whose masks are + all single prefixes has at most two sources. Beating 2c with blocks needs a + depth-d block with more than 2d sources. +- **Characteristic four** (finite certificate plus proof): an explicit + 36-event walk attains the floor of 2,080 calls at k = 9. With the deletion + lemma and a counting bound, **9 ≤ N(4) ≤ 21**. This answers part of + #4231's open question 1, which asked where the c = 4 floor first fails. +- **Counting** (proof): N(c) is below the first k with + C(ck + c − 1, c) < 2^k − 1. That k is 7, 14, 22, 30, 38, 47, 56, 65 for + c = 2..9. + +At c = 2, Theorem A is sharp: #943 shows that five sources fail. At c = 3 it +gives n ≤ 6, the range proved in +[#4232](https://github.com/CrocSwap/integer-mult-bounds/pull/4232). At c = 4 +the nine-source walk shows that blocks are not optimal. + +The claims are a scoped proof plus a finite certificate. There is no new κ, no +selected-frontier change and no multiplication theorem. + +## 1. Interface and prefix criterion + +The interface is #4231's. R is a nonzero unital ring of characteristic c. The +rows are k read-only sources x_j, outputs y_m for m = 1, …, 2^k − 1 and one +borrowed dirty connector z. For arbitrary R-linear maps B_j and A_m, the word +must implement + +```text +y_m += sum_(j: bit_j(m)=1) A_m B_j x_j, x_j and z unchanged. +``` + +The only calls are `B_j: z += B_j x_j` and `A_m: y_m += A_m z`. Signed calls, +extra connectors, scaling, frame changes and free copies are not admitted. + +#4231 proves the floor: B_j and A_m each occur a positive multiple of c times. +A floor word therefore has a source walk w of length ck that uses each source +exactly c times. Let q_t ∈ (Z/c)^k count source events modulo c after t steps. +If A_m reads at boundaries t_1 ≤ … ≤ t_c, output m receives +A_m(c·z0 + Σ_j (Σ_i q_(t_i))_j B_j x_j). Since c·z0 = 0, the word is correct +exactly when + +```text +q_(t_1) + ... + q_(t_c) = m in (Z/c)^k for every nonzero mask m. +``` + +z is restored because each B_j x_j is added c times. This is the c-fold form of +#4232's triple criterion. Integer coefficients act through Z/c, the prime +subring of R, so no commutation of A_m with B_j is used. + +## 2. Theorem A: N(c) ≥ 2c + +Say a walk on source set S has **depth d** if every nonzero S-mask is a sum of +at most d prefixes q_t. + +**Concatenation.** Let P and P′ be walks on disjoint source sets, each source +used c times, with depths d and d′, where d + d′ ≤ c. In PP′, the prefix at a +boundary inside P′ is (0, q′) because P returns to zero modulo c. A mask +(m, m′) is the sum of the prefixes for m in P and for m′ in P′. The +remaining readouts go to boundary 0, which has prefix zero. So PP′ has +depth d + d′, and by induction blocks with total depth at most c give a floor +walk. + +**Blocks of depth one.** For sources a and b, take + +```text +a b a^(c-1) b^(c-1) +``` + +Its prefixes include (1,0) after one step, (1,1) after two and (0,1) after +c + 1. The one-source block a^c has prefix 1 after one step. Pair the k sources +into ⌈k/2⌉ ≤ c blocks. Each mask then reads once at one boundary in every block +where it is nonzero, and at boundary 0 for the remaining readouts. + +The verifier builds this word for all 54 pairs (c, k) with 2 ≤ c ≤ 7 and +k ≤ 2c. It simulates each with generic coefficients and checks that every +operator is called exactly c times. At (c, k) = (3, 7), four blocks are needed +and the construction is rejected. + +## 3. Lemma C: depth-one blocks carry at most two sources + +In a walk that uses source j exactly c times, coordinate j of q_t is 0 before +its first event and after its last. It is 1 between its first and second +events, and lies in {2, …, c − 1} between its second and last. A prefix is +binary exactly when no coordinate is in that middle stage. Its support is +{j : first_j ≤ t < second_j}. That set changes only at the 2k first and second +events, so there are at most 2k distinct nonzero binary prefixes. Since +2^k − 1 > 2k for k ≥ 3, a depth-one walk has at most two sources. + +As a control, the verifier enumerates all 90, 1,680 and 34,650 three-source +walks for c = 2, 3 and 4. None has depth one. + +Under concatenation, a block of depth d therefore adds more than 2 sources per +unit depth only if it has more than 2d sources. The nine-source c = 4 walk +below has depth 4, so it is such a block. + +## 4. Characteristic four: 9 ≤ N(4) ≤ 21 + +[CERTIFICATE.json](CERTIFICATE.json) gives the walk + +```text +4 2 6 4 0 8 1 7 3 2 5 2 1 7 4 3 0 2 5 8 6 5 6 4 8 3 1 0 5 7 8 7 0 3 6 1 +``` + +Each of the nine sources occurs four times. The verifier regenerates, for each +of the 511 masks, the lexicographically first boundary multiset of size four +that sums to it. It then builds the literal 2,080-call word, simulates it with +generic coefficients, and runs it on random singular, noncommuting 2×2 +matrices over Z/4. + +**Deletion lemma.** This is #4232's lemma; its proof does not use c = 3. +Delete the c events of source j from a floor walk. Each old boundary maps to a +new boundary with the same counts on the other sources, so every mask with bit +j zero keeps its readouts. The attaining set is therefore an initial segment +{1, …, N(c)}. The verifier checks all nine deletions of the certified walk. + +**Counting.** Boundaries 0 and ck both have prefix zero, so the readouts of a +mask are a multiset of size c drawn from ck boundary indices. There are +C(ck + c − 1, c) such multisets. For c = 4, C(87, 4) = 2,225,895 ≥ 2,097,151 +at k = 21, but C(91, 4) = 2,672,670 < 4,194,303 at k = 22. With the deletion +lemma, every k ≥ 22 fails. At c = 3 the threshold is 14, as in #4232. The +verifier checks the table for c ≤ 9 and that failure persists up to k = 200. + +## 5. Search notes (local only, not proofs) + +The nine-source walk came from simulated annealing over restored 36-event +walks. These are search failures, not exclusions: + +- Eight annealing runs over 40-event walks did not reach all 1,023 masks at + k = 10. +- No depth-two five-source block at c = 4 was found; the best run covered 28 of + 31 masks. +- No depth-three seven-source block was found; the best run covered 125 of 127. + +Depth-two blocks on four sources and depth-three blocks on six exist at c = 4. +They reach only eight sources by concatenation. The search programs and logs +are not committed. + +## 6. Reproduction + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-depth-blocks/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-depth-blocks +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-depth-blocks --check-source-history +``` + +Expected marker: +`PASS_CONNECTOR_DEPTH_BLOCKS blocks_k<=2c c4_attained_k<=9 c4_counting_excludes_k>=22`. +The verifier uses only the standard library and takes about 3 s. It prints a +receipt hash bound to all six package files. Six mutation controls must be +rejected: a dropped call, a doubled readout, a relabelled source call, the +c = 4 word read in characteristic eight, the sorted run walk at k = 9, and the +block construction at (c, k) = (3, 7). + +## 7. Limitations + +The result covers only the unsigned, immutable-source, complete-call interface +of #4231. Theorem A is proved for every c; the word check runs for c ≤ 7. +Fixed call prices must include their full implementation. Input admission, +coefficient preparation, dispatch and physical costs are additional and +unknown. No consumer is instantiated. The exact value of N(4) and the growth +of N(c) remain open. Proof-kernel checks and independent human review are not +claimed. + +## Open next questions + +These are recorded with first steps in [TASK.json](TASK.json). + +1. What is N(4) exactly, within 9 ≤ N(4) ≤ 21? Every ten-source floor walk + restricts to a nine-source one, so an insertion search over nine-source + floor walks is a natural first step. +2. How does N(c) grow? Theorem A gives 2c and counting gives O(c log c). A + depth-d block with more than 2d sources, valid for every large c, would + improve the constant. +3. Does any concrete consumer use a characteristic-c batch of more than c + sources at a favourable complete invoice? + +## Credit + +Produced by Nick Petalas. The interface, the floor c(k + 2^k − 1) and the k ≤ c +run walk are #4231's. The prefix criterion, deletion lemma and counting +argument extend #4232's F3 versions. The connector interface and prefix-boundary +readout criterion come from Ross Richardson's +[#943](../universal-connector-boundary/README.md). Apache-2.0. diff --git a/research/connector-c5-certificate/vendor/drat-trim/LICENSE b/research/connector-c5-certificate/vendor/drat-trim/LICENSE new file mode 100644 index 0000000000..9859ca161d --- /dev/null +++ b/research/connector-c5-certificate/vendor/drat-trim/LICENSE @@ -0,0 +1,17 @@ +Copyright (c) 2014 Marijn Heule and Nathan Wetzler, The University of Texas at Austin. +Copyright (c) 2015-2016 Marijn Heule, The University of Texas at Austin. + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/research/connector-c5-certificate/vendor/drat-trim/drat-trim.c b/research/connector-c5-certificate/vendor/drat-trim/drat-trim.c new file mode 100644 index 0000000000..cf8a676ffc --- /dev/null +++ b/research/connector-c5-certificate/vendor/drat-trim/drat-trim.c @@ -0,0 +1,1501 @@ +/************************************************************************************[drat-trim.c] +Copyright (c) 2014 Marijn Heule and Nathan Wetzler, The University of Texas at Austin. +Copyright (c) 2015-2024 Marijn Heule, Carnegie Mellon University +Last edit: April 21, 2024 + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include +#include +#include +#include + +//#define PARTIALPROOF + +#define TIMEOUT 40000 +#define BIGINIT 1000000 +#define INIT 4 +#define END 0 +#define UNSAT 0 +#define SAT 1 +#define DERIVATION 2 +#define ID -1 +#define PIVOT -2 +#define MAXDEP -3 +#define EXTRA 4 // ID + PIVOT + MAXDEP + terminating 0 +#define INFOBITS 2 // could be 1 for SAT, must be 2 for QBF +#define DBIT 1 +#define ASSUMED 2 +#define MARK 3 +#define ERROR -1 +#define ACTIVE 1 + +#define FORWARD_SAT 10 +#define FORWARD_UNSAT 20 +#define BACKWARD_UNSAT 30 +#define SUCCESS 40 +#define FAILED 50 +#define FIXPOINT 60 +#define NOWARNING 70 +#define HARDWARNING 80 + +#define COMPRESS + +struct solver { FILE *inputFile, *proofFile, *lratFile, *traceFile, *activeFile; + int *DB, nVars, timeout, mask, delete, *falseStack, *falseA, *forced, binMode, optimize, binOutput, + *processed, *assigned, count, *used, *max, COREcount, RATmode, RATcount, nActive, *lratTable, + nLemmas, maxRAT, *preRAT, maxDependencies, nDependencies, bar, backforce, reduce, + *dependencies, maxVar, maxSize, mode, verb, unitSize, unitStackSize, prep, *current, nRemoved, warning, + delProof, *setMap, *setTruth, rupOnly; + char *coreStr, *lemmaStr; + struct timeval start_time; + long mem_used, time, nClauses, nStep, nOpt, nAlloc, *unitStack, *reason, lemmas, nResolve, *RATset, + nReads, nWrites, lratSize, lratAlloc, *lratLookup, **wlist, *optproof, *formula, *proof; }; + +static inline void assign (struct solver* S, int lit) { + S->falseA[-lit] = 1; *(S->assigned++) = -lit; } + +int compare (const void *a, const void *b) { + return (*(int*)a - *(int*)b); } + +int abscompare (const void *a, const void *b) { + return (abs(*(int*)a) - abs(*(int*)b)); } + +static inline void printClause (int* clause) { + printf ("[%i] ", clause[ID]); + while (*clause) printf ("%i ", *clause++); printf ("0\n"); } + +static inline void addWatchPtr (struct solver* S, int lit, long watch) { + if (S->used[lit] + 1 == S->max[lit]) { S->max[lit] *= 1.5; + S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]); + if (S->wlist[lit] == NULL) { printf("c MEMOUT: reallocation failed for watch list of %i\n", lit); exit (0); } } + S->wlist[lit][ S->used[lit]++ ] = watch | S->mask; + S->wlist[lit][ S->used[lit] ] = END; } + +static inline void addWatch (struct solver* S, int* clause, int index) { + addWatchPtr (S, clause[index], ((long) (((clause) - S->DB)) << 1)); } + +static inline void removeWatch (struct solver* S, int* clause, int index) { + int i, lit = clause[index]; + if ((S->used[lit] > INIT) && (S->max[lit] > 2 * S->used[lit])) { + S->max[lit] = (3 * S->used[lit]) >> 1; + S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]); + assert(S->wlist[lit] != NULL); } + long *watch = S->wlist[lit]; + for (i = 0; i < S->used[lit]; i++) { + int* _clause = S->DB + (*(watch++) >> 1); + if (_clause == clause) { + watch[-1] = S->wlist[lit][ --S->used[lit] ]; + S->wlist[lit][ S->used[lit] ] = END; return; } } } + +static inline void addUnit (struct solver* S, long index) { +// printf("c adding unit %i\n", S->DB[index]); + if (S->unitSize >= S->unitStackSize) { + S->unitStackSize = (S->unitStackSize * 3) >> 1; + S->unitStack = (long*) realloc (S->unitStack, sizeof(long) * S->unitStackSize); + if (S->unitStack == NULL) { + printf ("c failed to reallocate unit stack\n"); exit (0); } } + S->unitStack[S->unitSize++] = index; } + +static inline void removeUnit (struct solver* S, int lit) { + int i, found = 0; + for (i = 0; i < S->unitSize; i++) { + if (found) S->unitStack[i - 1] = S->unitStack[i]; + if (S->DB[ S->unitStack[i] ] == lit) found = 1; } + S->unitSize--; } + +static inline void unassignUnit (struct solver* S, int lit) { + if (S->verb) + printf ("\rc removing unit %i\n", lit); + while (S->falseA[-lit]) { + if (S->verb) + printf ("\rc removing unit %i (%i)\n", S->forced[-1], lit); + S->falseA[*(--S->forced)] = 0; + S->reason[abs(*S->forced)] = 0; } + S->processed = S->assigned = S->forced; } + +static inline void markWatch (struct solver* S, int* clause, int index, int offset) { + long* watch = S->wlist[ clause[ index ] ]; + for (;;) { + int *_clause = (S->DB + (*(watch++) >> 1) + (long) offset); + if (_clause == clause) { watch[ID] |= ACTIVE; return; } } } + +static inline void addDependency (struct solver* S, int dep, int forced) { + if (1 || S->traceFile || S->lratFile) { // temporary for MAXDEP + if (S->nDependencies == S->maxDependencies) { + S->maxDependencies = (S->maxDependencies * 3) >> 1; +// printf ("c dependencies increased to %i\n", S->maxDependencies); + S->dependencies = realloc (S->dependencies, sizeof (int) * S->maxDependencies); + if (S->dependencies == NULL) { printf ("c MEMOUT: dependencies reallocation failed\n"); exit (0); } } +// printf("c adding dep %i\n", (dep << 1) + forced); + S->dependencies[S->nDependencies++] = (dep << 1) + forced; } } + +static inline void markClause (struct solver* S, int* clause, int index) { + S->nResolve++; + addDependency (S, clause[index - 1] >> 1, (S->assigned > S->forced)); + + if ((clause[index + ID] & ACTIVE) == 0) { + S->nActive++; + clause[index + ID] |= ACTIVE; +//#ifdef PARTIALPROOF +// if ((clause + index) > (S->DB + S->firstLemma)) // don't delete original clauses +//#endif + if ((S->mode == BACKWARD_UNSAT) && clause[index + 1]) { + S->optproof[S->nOpt++] = (((long) (clause - S->DB) + index) << INFOBITS) + 1; } + if (clause[1 + index] == 0) return; + markWatch (S, clause, index, -index); + markWatch (S, clause, 1 + index, -index); } + while (*clause) S->falseA[*(clause++)] = MARK; } + +void analyze (struct solver* S, int* clause, int index) { // Mark all clauses involved in conflict + markClause (S, clause, index); + while (S->assigned > S->falseStack) { + int lit = *(--S->assigned); + if (S->falseA[lit] == MARK) { + if (S->reason[abs (lit)]) { + markClause (S, S->DB + S->reason[abs (lit)], -1); + if (S->assigned >= S->forced) + S->reason[abs (lit)] = 0; } } +#ifndef PARTIALPROOF + else if (S->falseA[lit] == ASSUMED && !S->RATmode && S->reduce && !S->lratFile) { // Remove unused literal + S->nRemoved++; + int *tmp = S->current; + while (*tmp != lit) tmp++; + while (*tmp) { tmp[0] = tmp[1]; tmp++; } + tmp[-1] = 0; } +#endif + if (S->assigned >= S->forced) S->reason[abs (lit)] = 0; + S->falseA[lit] = (S->assigned < S->forced); } + + S->processed = S->assigned = S->forced; } + +void noAnalyze (struct solver* S) { + while (S->assigned > S->falseStack) { + int lit = *(--S->assigned); + if (S->assigned >= S->forced) S->reason[abs (lit)] = 0; + S->falseA[lit] = (S->assigned < S->forced); } + + S->processed = S->assigned = S->forced; } + +int propagate (struct solver* S, int init, int mark) { // Performs unit propagation (init not used?) + int *start[2]; + int check = 0, mode = !S->prep; + int i, lit, _lit = 0; long *watch, *_watch; + start[0] = start[1] = S->processed; + flip_check:; + check ^= 1; + while (start[check] < S->assigned) { // While unprocessed false literals + lit = *(start[check]++); // Get first unprocessed literal + if (lit == _lit) watch = _watch; + else watch = S->wlist[ lit ]; // Obtain the first watch pointer + while (*watch != END) { // While there are watched clauses (watched by lit) + if ((*watch & mode) != check) { + watch++; continue; } + int *clause = S->DB + (*watch >> 1); // Get the clause from DB + if (S->falseA[ -clause[0] ] || + S->falseA[ -clause[1] ]) { + watch++; continue; } + if (clause[0] == lit) clause[0] = clause[1]; // Ensure that the other watched literal is in front + for (i = 2; clause[i]; ++i) // Scan the non-watched literals + if (S->falseA[ clause[i] ] == 0) { // When clause[j] is not false, it is either true or unset + clause[1] = clause[i]; clause[i] = lit; // Swap literals + addWatchPtr (S, clause[1], *watch); // Add the watch to the list of clause[1] + *watch = S->wlist[lit][ --S->used[lit] ]; // Remove pointer + S->wlist[lit][ S->used[lit] ] = END; + goto next_clause; } // Goto the next watched clause + clause[1] = lit; watch++; // Set lit at clause[1] and set next watch + if (!S->falseA[ clause[0] ]) { // If the other watched literal is falsified, + assign (S, clause[0]); // A unit clause is found, and the reason is set + S->reason[abs (clause[0])] = ((long) ((clause)-S->DB)) + 1; + if (!check) { + start[0]--; _lit = lit; _watch = watch; + goto flip_check; } } + else if (!mark) { noAnalyze (S); return UNSAT; } + else { analyze (S, clause, 0); return UNSAT; } // Found a root level conflict -> UNSAT + next_clause: ; } } // Set position for next clause + if (check) goto flip_check; + S->processed = S->assigned; + return SAT; } // Finally, no conflict was found + + +// Propagate top level units +static inline int propagateUnits (struct solver* S, int init) { + int i; +// printf("c propagateUnits %i\n", S->unitSize); + while (S->forced > S->falseStack) { + S->falseA[*(--S->forced)] = 0; + S->reason[abs (*S->forced)] = 0; } + S->forced = S->assigned = S->processed = S->falseStack; + for (i = 0; i < S->unitSize; i++) { + int lit = S->DB[ S->unitStack[i] ]; + S->reason[abs (lit)] = S->unitStack[i] + 1; + assign (S, lit); } + + if (propagate (S, init, 1) == UNSAT) { return UNSAT; } + S->forced = S->processed; + return SAT; } + +// Put falsified literals at the end and returns the size under the current +// assignment: negative size means satisfied, size = 0 means falsified +int sortSize (struct solver *S, int *lemma) { + unsigned int size = 0, last = 0, sat = 1; + while (lemma[last]) { + int lit = lemma[last++]; + if (S->falseA[lit] == 0) { + if (S->falseA[-lit]) sat = -1; + lemma[last-1] = lemma[ size ]; + lemma[size++] = lit; } } + return sat * size; } + +// print the core clauses to coreFile in DIMACS format +void printCore (struct solver *S) { + int i, j; + for (i = 0; i < S->nClauses; i++) { + int *clause = S->DB + (S->formula[i] >> INFOBITS); + if (clause[ID] & ACTIVE) S->COREcount++; } + printf ("\rc %i of %li clauses in core \n", S->COREcount, S->nClauses); + + if (S->coreStr) { + FILE *coreFile = fopen (S->coreStr, "w"); + fprintf (coreFile, "p cnf %i %i\n", S->nVars, S->COREcount); + for (i = 0; i < S->nClauses; i++) { + int *clause = S->DB + (S->formula[i] >> INFOBITS); + if (clause[ID] & ACTIVE) { + while (*clause) fprintf (coreFile, "%i ", *clause++); + fprintf (coreFile, "0\n"); } } + fclose (coreFile); } } + +void write_lit (struct solver *S, FILE *output, int lit) { // change to long? + unsigned int l = abs (lit) << 1; + if (lit < 0) l++; + + do { + if (l <= 127) { fputc ((char) l, output); } + else { fputc ((char) (128 + (l & 127)), output); } + S->nWrites++; + l = l >> 7; } + while (l); } + +void printLRATline (struct solver *S, int time) { + int *line = S->lratTable + S->lratLookup[time]; + if (S->binOutput) { + fputc ('a', S->lratFile); S->nWrites++; + while (*line) write_lit (S, S->lratFile, *line++); + write_lit (S, S->lratFile, *line++); + while (*line) write_lit (S, S->lratFile, *line++); + write_lit (S, S->lratFile, *line++); } + else { + while (*line) fprintf (S->lratFile, "%i ", *line++); + fprintf (S->lratFile, "%i ", *line++); + while (*line) fprintf (S->lratFile, "%i ", *line++); + fprintf (S->lratFile, "%i\n", *line++); } } + +// print the core lemmas to lemmaFile in DRAT format +void printProof (struct solver *S) { + int step; + printf ("\rc %i of %i lemmas in core using %lu resolution steps\n", S->nActive - S->COREcount + 1, S->nLemmas + 1, S->nResolve); + printf ("\rc %d RAT lemmas in core; %i redundant literals in core lemmas\n", S->RATcount, S->nRemoved); + + // NB: not yet working with forward checking + if (S->mode == FORWARD_UNSAT) { + printf ("\rc optimized proofs are not supported for forward checking\n"); + return; } + + // replace S->proof by S->optproof + if (S->mode == BACKWARD_UNSAT) { + if (S->nOpt > S->nAlloc) { + S->nAlloc = S->nOpt; + S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); + if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + S->nStep = 0; + S->nLemmas = 0; + for (step = S->nOpt - 1; step >= 0; step--) { + long ad = S->optproof[step]; + int *lemmas = S->DB + (ad >> INFOBITS); + if ((ad & 1) == 0) S->nLemmas++; +// if (lemmas[ID] & ACTIVE) lemmas[ID] ^= ACTIVE; // only useful for checking multiple times? + S->proof[S->nStep++] = S->optproof[step]; } } // why not reuse ad? + + if (S->lemmaStr) { + FILE *lemmaFile = fopen (S->lemmaStr, "w"); + for (step = 0; step < S->nStep; step++) { + long ad = S->proof[step]; + int *lemmas = S->DB + (ad >> INFOBITS); + if (!lemmas[1] && (ad & 1)) continue; // don't delete unit clauses + if (S->binOutput) { + S->nWrites++; + if (ad & 1) fputc ('d', lemmaFile); + else fputc ('a', lemmaFile); } + else if (ad & 1) fprintf (lemmaFile, "d "); + int reslit = lemmas[PIVOT]; + while (*lemmas) { + int lit = *lemmas++; + if (lit == reslit) { + if (S->binOutput) write_lit (S, lemmaFile, lit); + else fprintf (lemmaFile, "%i ", lit); } } + lemmas = S->DB + (ad >> INFOBITS); + while (*lemmas) { + int lit = *lemmas++; + if (lit != reslit) { + if (S->binOutput) write_lit (S, lemmaFile, lit); + else fprintf (lemmaFile, "%i ", lit); } } + if (S->binOutput) write_lit (S, lemmaFile, 0); + else fprintf (lemmaFile, "0\n"); } + if (S->binOutput) { fputc ('a', lemmaFile); write_lit (S, lemmaFile, 0); } + else fprintf (lemmaFile, "0\n"); + fclose (lemmaFile); } + + if (S->lratFile) { + int lastAdded = S->nClauses; + int flag = 0; + for (step = 0; step < S->nStep; step++) { + long ad = S->proof[step]; + int *lemmas = S->DB + (ad >> INFOBITS); + if ((ad & 1) == 0) { + if (lastAdded == 0) { + if (S->binOutput) { + write_lit (S, S->lratFile, 0); } + else { + fprintf (S->lratFile, "0\n"); } } + lastAdded = lemmas[ID] >> 1; + printLRATline (S, lastAdded); } + else if (lastAdded == S->nClauses) continue; + else if (!lemmas[1] && (ad & 1)) continue; // don't delete unit clauses + else if (ad & 1) { + if (lastAdded != 0) { + if (S->binOutput) { + fputc ('d', S->lratFile); S->nWrites++; } + else { + fprintf (S->lratFile, "%i d ", lastAdded); } } + lastAdded = 0; + if (S->binOutput) { + write_lit (S, S->lratFile, lemmas[ID] >> 1); } + else { + fprintf (S->lratFile, "%i ", lemmas[ID] >> 1); } } } + if (lastAdded != S->nClauses) { + if (S->binOutput) { + write_lit (S, S->lratFile, 0); } + else { + fprintf(S->lratFile, "0\n"); } } + + printLRATline (S, S->count); + + fclose (S->lratFile); + if (S->nWrites) + printf ("c wrote optimized proof in LRAT format of %li bytes\n", S->nWrites); } } + +void printNoCore (struct solver *S) { + if (S->lratFile) { + if (S->binOutput) { + fputc ('d', S->lratFile); S->nWrites++; } + else { + fprintf (S->lratFile, "%ld d ", S->nClauses); } + int i; + for (i = 0; i < S->nClauses; i++) { + int *clause = S->DB + (S->formula[i] >> INFOBITS); + if ((clause[ID] & ACTIVE) == 0) { + if (S->binOutput) { + write_lit (S, S->lratFile, clause[ID] >> 1); } + else { + fprintf (S->lratFile, "%i ", clause[ID] >> 1); } } } + if (S->binOutput) { + write_lit (S, S->lratFile, 0); } + else { + fprintf (S->lratFile, "0\n"); } } } + +// print the dependency graph to traceFile in TraceCheck+ format +// this procedure adds the active clauses at the end of the trace +void printTrace (struct solver *S) { + if (S->traceFile) { int i; + for (i = 0; i < S->nClauses; i++) { + int *clause = S->DB + (S->formula[i] >> INFOBITS); + if (clause[ID] & ACTIVE) { + fprintf (S->traceFile, "%i ", i + 1); + while (*clause) fprintf (S->traceFile, "%i ", *clause++); + fprintf (S->traceFile, "0 0\n"); } } + fclose (S->traceFile); } } + +void printActive (struct solver *S) { + int i, j; + if (S->activeFile) { + for (i = -S->maxVar; i <= S->maxVar; i++) + if (i != 0) + for (j = 0; j < S->used[i]; j++) { + int *clause = S->DB + (S->wlist[i][j] >> 1); + if (*clause == i) { + while (*clause) + fprintf (S->activeFile, "%i ", *clause++); + fprintf (S->activeFile, "0\n"); } } } } + +void postprocess (struct solver *S) { + printNoCore (S); // print before proof optimization + printActive (S); + printCore (S); + printTrace (S); // closes traceFile + printProof (S); } // closes lratFile + +void lratAdd (struct solver *S, int elem) { + if (S->lratSize == S->lratAlloc) { + S->lratAlloc = S->lratAlloc * 3 >> 1; + S->lratTable = (int *) realloc (S->lratTable, sizeof (int) * S->lratAlloc); + if (S->lratTable == NULL) { + printf ("c MEMOUT: failed to reallocate lrat table\n"); exit (0); } } + S->lratTable[S->lratSize++] = elem; } + +void printDependenciesFile (struct solver *S, int* clause, int RATflag, int mode) { + FILE *file = NULL; + if (mode == 0) file = S->traceFile; + if (mode == 1) file = S->lratFile; + + if (file) { + int i, j, k; + int tmp = S->lratSize; + + if (clause != NULL) { + S->lratLookup[clause[ID] >> 1] = S->lratSize; } + else { S->lratLookup[S->count] = S->lratSize; } + + if (clause != NULL) { + int size = 0; + int *sortClause; + + sortClause = (int *) malloc (sizeof(int) * S->maxSize); + assert (sortClause != NULL); + lratAdd (S, S->time >> 1); // NB: long to ing + int reslit = clause[PIVOT]; + while (*clause) { + if (*clause == reslit) + lratAdd (S, reslit); + sortClause[size++] = *clause++; } + qsort (sortClause, size, sizeof (int), abscompare); + for (i = 0; i < size; i++) { + int lit = sortClause[i]; + if (lit != reslit) + lratAdd (S, lit); } + free (sortClause); } + else { lratAdd (S, S->count); } + lratAdd (S, 0); + + int isRUP = 1; + for (i = 0; i < S->nDependencies; i++) + if (S->dependencies[i] < 0) { isRUP = 0; break; } + + if (isRUP) { + for (i = S->nDependencies - 1; i >= 0; i--) + lratAdd (S, S->dependencies[i] >> 1); + lratAdd (S, 0); + goto printLine; } + + // first print the preRAT units in order of becoming unit + int size = 0; + for (i = 0; i < S->nDependencies; i++) { + if (S->dependencies[i] > 0) continue; + for (j = i - 1; j >= 0 && S->dependencies[j] > 0; j--) { + int flag = 0; + int cls = S->dependencies[j]; + if (cls & 1) continue; + for (k = 0; k < size; k++) + if (S->preRAT[k] == cls) flag = 1; + if (!flag) { + S->preRAT[size++] = cls; + lratAdd (S, cls >> 1); } } } + + // print dependencies in order of becoming unit + for (i = S->nDependencies - 1; i >= 0; i--) { + int cls = S->dependencies[i]; + if ((mode == 0) && (cls < 0)) continue; + if (mode == 0) { + int flag = 0; + for (j = 0; j < size; j++) + if (S->preRAT[j] == cls) flag = 1; + if (!flag) { + S->preRAT[size++] = cls; + lratAdd (S, cls >> 1); } } + if ((mode == 1) && (cls & 1)) + lratAdd (S, cls >> 1); } + lratAdd (S, 0); + + printLine:; + if (mode == 0) { + for (i = tmp; i < S->lratSize; i++) + fprintf (file, "%d ", S->lratTable[i]); + S->lratSize = tmp; + fprintf (file, "\n"); } } } + +void printDependencies (struct solver *S, int* clause, int RATflag) { + if (clause != NULL) { + int i; + clause[MAXDEP] = 0; + for (i = 0; i < S->nDependencies; i++) { + if (S->dependencies[i] > clause[MAXDEP]) + clause[MAXDEP] = S->dependencies[i]; } + assert (clause[MAXDEP] < clause[ID]); } + + printDependenciesFile (S, clause, RATflag, 0); + printDependenciesFile (S, clause, RATflag, 1); } + +int checkRAT (struct solver *S, int pivot, int mark) { + int i, j, nRAT = 0; + + // Loop over all literals to calculate resolution candidates + for (i = -S->maxVar; i <= S->maxVar; i++) { + if (i == 0) continue; + // Loop over all watched clauses for literal + for (j = 0; j < S->used[i]; j++) { + int* watched = S->DB + (S->wlist[i][j] >> 1); + int id = watched[ID] >> 1; + int active = watched[ID] & ACTIVE; + if (*watched == i) { // If watched literal is in first position + while (*watched) + if (*watched++ == -pivot) { + if ((S->mode == BACKWARD_UNSAT) && !active) { +// printf ("\rc RAT check ignores unmarked clause : "); printClause (S->DB + (S->wlist[i][j] >> 1)); + continue; } + if (nRAT == S->maxRAT) { + S->maxRAT = (S->maxRAT * 3) >> 1; + S->RATset = realloc (S->RATset, sizeof (long) * S->maxRAT); + assert (S->RATset != NULL); } + S->RATset[nRAT++] = S->wlist[i][j] >> 1; + break; } } } } + + // S->prep = 1; + // Check all clauses in RATset for RUP + int flag = 1; + qsort (S->RATset, nRAT, sizeof (long), compare); + S->nDependencies = 0; + for (i = nRAT - 1; i >= 0; i--) { + int* RATcls = (int*) (S->DB + S->RATset[i]); + int id = RATcls[ID] >> 1; + int blocked = 0; + long int reason = 0; + if (S->verb) { + printf ("\rc RAT clause: "); printClause (RATcls); } + + while (*RATcls) { + int lit = *RATcls++; + if (lit != -pivot && S->falseA[-lit]) + if (!blocked || reason > S->reason[abs (lit)]) + blocked = lit, reason = S->reason[abs (lit)]; } + + if (blocked && reason) { + analyze (S, S->DB + reason, -1); + S->reason[abs (blocked)] = 0; } + + if (!blocked) { + RATcls = (int*) (S->DB + S->RATset[i]); + while (*RATcls) { + int lit = *RATcls++; + if (lit != -pivot && !S->falseA[lit]) { + assign (S, -lit); S->reason[abs (lit)] = 0; } } + if (propagate (S, 0, mark) == SAT) { flag = 0; break; } } + addDependency (S, -id, 1); } + + if (flag == 0) { + while (S->forced < S->assigned) { + S->falseA[*(--S->assigned)] = 0; + S->reason[abs (*S->assigned)] = 0; } + if (S->verb) printf ("\rc RAT check on pivot %i failed\n", pivot); + return FAILED; } + + return SUCCESS; } + +int redundancyCheck (struct solver *S, int *clause, int size, int mark) { + int i, indegree; + int falsePivot = S->falseA[clause[PIVOT]]; + if (S->verb) { printf ("\rc checking lemma (%i, %i) ", size, clause[PIVOT]); printClause (clause); } + + if (S->mode != FORWARD_UNSAT) { + if ((clause[ID] & ACTIVE) == 0) return SUCCESS; } // redundant? +// clause[PIVOT] ^= ACTIVE; } + + if (size < 0) { + S->DB[ S->reason[abs (*clause)] - 2] |= 1; + return SUCCESS; } + + indegree = S->nResolve; + + S->RATmode = 0; + S->nDependencies = 0; + for (i = 0; i < size; ++i) { + if (S->falseA[-clause[i]]) { // should only occur in forward mode + if (S->warning != NOWARNING) { + printf ("\rc WARNING: found a tautological clause in proof: "); printClause (clause); } + if (S->warning == HARDWARNING) exit (HARDWARNING); + while (S->forced < S->assigned) { + S->falseA[*(--S->assigned)] = 0; + S->reason[abs (*S->assigned)] = 0; } + return SUCCESS; } + S->falseA[clause[i]] = ASSUMED; + *(S->assigned++) = clause[i]; + S->reason[abs (clause[i])] = 0; } + + S->current = clause; + if (propagate (S, 0, mark) == UNSAT) { + indegree = S->nResolve - indegree; + if (indegree <= 2 && S->prep == 0) { + S->prep = 1; if (S->verb) printf ("\rc [%li] preprocessing checking mode on\n", S->time); } + if (indegree > 2 && S->prep == 1) { + S->prep = 0; if (S->verb) printf ("\rc [%li] preprocessing checking mode off\n", S->time); } + if (S->verb) printf ("\rc lemma has RUP\n"); + printDependencies (S, clause, 0); + return SUCCESS; } + + // Failed RUP check. Now test RAT. + // printf ("RUP check failed. Starting RAT check.\n"); + if (S->rupOnly) { + printf ("\rc RUP check failed\n"); + return FAILED; } + int reslit = clause[PIVOT]; + if (S->verb) + printf ("\rc RUP checked failed; starting RAT check on pivot %d.\n", reslit); + + if (falsePivot) return FAILED; + + int* savedForced = S->forced; + + S->RATmode = 1; + S->forced = S->assigned; + + int failed = 0; + if (checkRAT (S, reslit, mark) == FAILED) { + failed = 1; + if (S->warning != NOWARNING) { + printf ("\rc WARNING: RAT check on proof pivot failed : "); printClause (clause); } + if (S->warning == HARDWARNING) exit (HARDWARNING); + for (i = 0; i < size; i++) { + if (clause[i] == reslit) continue; + if (checkRAT (S, clause[i], mark) == SUCCESS) { + clause[PIVOT] = clause[i]; + failed = 0; break; } } } + + if (failed == 0) + printDependencies (S, clause, 1); + + S->processed = S->forced = savedForced; + while (S->forced < S->assigned) { + S->falseA[*(--S->assigned)] = 0; + S->reason[abs (*S->assigned)] = 0; } + + if (failed) { + printf ("c RAT check failed on all possible pivots\n"); + return FAILED; } + + + if (mark) S->RATcount++; + if (S->verb) printf ("\rc lemma has RAT on %i\n", clause[PIVOT]); + return SUCCESS; } + +int init (struct solver *S) { + S->forced = S->falseStack; // Points inside *falseStack at first decision (unforced literal) + S->processed = S->falseStack; // Points inside *falseStack at first unprocessed literal + S->assigned = S->falseStack; // Points inside *falseStack at last unprocessed literal + + // initialize watch pointers on the original clauses + S->RATmode = 0; + S->nRemoved = 0; + S->nOpt = 0; + S->nResolve = 0; + S->RATcount = 0; + S->nActive = 0; + S->COREcount = 0; + S->unitSize = 0; + + int i; + for (i = 1; i <= S->maxVar; ++i) { + S->reason [i] = 0; + S->falseStack[i] = 0; + S->falseA[i] = S->falseA[-i] = 0; + S->used [i] = S->used [-i] = 0; + S->wlist [i][0] = S->wlist [-i][0] = END; } + + for (i = 0; i < S->nClauses; i++) { + int *clause = S->DB + (S->formula[i] >> INFOBITS); + if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE; + if (clause[0] == 0) { + printf ("\rc formula contains empty clause\n"); + if (S->coreStr) { + FILE *coreFile = fopen (S->coreStr, "w"); + fprintf (coreFile, "p cnf 0 1\n 0\n"); + fclose (coreFile); } + if (S->lemmaStr) { + FILE *lemmaFile = fopen (S->lemmaStr, "w"); + fprintf (lemmaFile, "0\n"); + fclose (lemmaFile); } + return UNSAT; } + if (clause[1]) { addWatch (S, clause, 0); addWatch (S, clause, 1); } + else if (S->falseA[clause[0]]) { + printf ("\rc found complementary unit clauses: %i\n", clause[0]); + if (S->coreStr) { + FILE *coreFile = fopen (S->coreStr, "w"); + fprintf (coreFile, "p cnf %i 2\n%i 0\n%i 0\n", abs (clause[0]), clause[0], -clause[0]); + fclose (coreFile); } + if (S->lemmaStr) { + FILE *lemmaFile = fopen (S->lemmaStr, "w"); + fprintf (lemmaFile, "0\n"); + fclose (lemmaFile); } + if (S->lratFile) { + int j; + for (j = 0; j < i; j++) { + int *_clause = S->DB + (S->formula[j] >> INFOBITS); + if ((_clause[0] == -clause[0]) && !_clause[1]) break; } + fprintf (S->lratFile, "%li 0 %i %i 0\n", S->nClauses + 1, j + 1, i + 1); } + return UNSAT; } + else if (!S->falseA[ -clause[0] ]) { + addUnit (S, (long) (clause - S->DB)); + assign (S, clause[0]); } } + + S->nDependencies = 0; + S->time = S->count; // Alternative time init + if (propagateUnits (S, 1) == UNSAT) { + printf ("\rc UNSAT via unit propagation on the input instance\n"); + printDependencies (S, NULL, 0); + postprocess (S); return UNSAT; } + return SAT; } + +int verify (struct solver *S, int begin, int end) { + int top_flag = 1; + if (init (S) == UNSAT) return UNSAT; + + if (S->mode == FORWARD_UNSAT) { + if (begin == end) + printf ("\rc start forward verification\n"); } + + int step; + int adds = 0; + int active = S->nClauses; + for (step = 0; step < S->nStep; step++) { + if (step >= begin && step < end) continue; + long ad = S->proof[step]; long d = ad & 1; + int *lemmas = S->DB + (ad >> INFOBITS); + + S->time = lemmas[ID]; + if (d) { active--; } + else { active++; adds++; } + if (S->mode == FORWARD_SAT && S->verb) printf ("\rc %i active clauses\n", active); + + if (!lemmas[1]) { // found a unit + int lit = lemmas[0]; + if (S->verb) + printf ("\rc found unit in proof %i [%li]\n", lit, S->time); + if (d) { + if (S->mode == FORWARD_SAT) { + removeUnit (S, lit); propagateUnits (S, 0); } + else { // no need to remove units while checking UNSAT + if (S->verb) { printf("c removing proof step: d "); printClause(lemmas); } + S->proof[step] = 0; continue; } } + else { +// printf ("c unit %i\n", lit); +// if (S->falseA[-lit]) S->reason[abs(lit)] = (lemmas - S->DB) + 1; + if (S->mode == BACKWARD_UNSAT && S->falseA[-lit]) { S->proof[step] = 0; continue; } + else { addUnit (S, (long) (lemmas - S->DB)); } } } + + if (d && lemmas[1]) { // if delete and not unit + if ((S->reason[abs (lemmas[0])] - 1) == (lemmas - S->DB)) { // what is this check? + if (S->mode != FORWARD_SAT) { // ignore pseudo unit clause deletion + if (S->warning != NOWARNING) { + if (S->verb) { printf ("\rc WARNING: ignoring deletion instruction %li: ", (lemmas - S->DB)); printClause (lemmas); } } + if (S->warning == HARDWARNING) exit (HARDWARNING); + if (S->verb) { printf ("c ignoring deletion instruction %li: ", (lemmas - S->DB)); printClause (lemmas); } +// if (S->mode == BACKWARD_UNSAT) { // ignore pseudo unit clause deletion + S->proof[step] = 0; } + else { // if (S->mode == FORWARD_SAT) { // also for FORWARD_UNSAT? + removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1); + propagateUnits (S, 0); } } + else { + removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1); } + if (S->mode == FORWARD_UNSAT ) continue; // Ignore deletion of top-level units + if (S->mode == BACKWARD_UNSAT) continue; } + + int size = sortSize (S, lemmas); // after removal of watches + + if (d && S->mode == FORWARD_SAT) { + if (size == -1) propagateUnits (S, 0); // necessary? + if (redundancyCheck (S, lemmas, size, 1) == FAILED) { + printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); + return SAT; } + continue; } + + if (d == 0 && S->mode == FORWARD_UNSAT) { + if (step > end) { + if (size < 0) continue; // Fix of bus error: 10 + if (redundancyCheck (S, lemmas, size, 1) == FAILED) { + printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); + return SAT; } + + size = sortSize (S, lemmas); + S->nDependencies = 0; } } + + if (lemmas[1]) + addWatch (S, lemmas, 0), addWatch (S, lemmas, 1); + + if (size == 0) { printf ("\rc conflict claimed, but not detected\n"); return SAT; } // change to FAILED? + if (size == 1) { + if (S->verb) printf ("\rc found unit %i\n", lemmas[0]); + assign (S, lemmas[0]); S->reason[abs (lemmas[0])] = ((long) ((lemmas)-S->DB)) + 1; + if (propagate (S, 1, 1) == UNSAT) goto start_verification; + S->forced = S->processed; } } + + if (S->mode == FORWARD_SAT && active == 0) { + postprocess (S); return UNSAT; } + + if (S->mode == FORWARD_UNSAT) { + if (begin == end) { + postprocess (S); + printf ("\rc VERIFIED derivation: all lemmas preserve satisfiability\n"); + if (S->warning != NOWARNING) { + printf ("\rc WARNING: no empty clause detected, this is not a refutation\n"); } + return DERIVATION; } + return SAT; } + + if (S->mode == BACKWARD_UNSAT) { + if (S->backforce) { + int s; + for (s = 0; s < step; s++) { + long ad = S->proof[s]; + int *clause = S->DB + (ad >> INFOBITS); + if (sortSize(S, clause) >= 0) { + if ( (ad & 1) && (clause[ID] & ACTIVE)) clause[ID] ^= ACTIVE; + if (!(ad & 1)) clause[ID] |= ACTIVE; } } } + if (!S->backforce) { + printf ("\rc ERROR: no conflict\n"); + return SAT; + } } + + start_verification:; + if (S->mode == FORWARD_UNSAT) { + printDependencies (S, NULL, 0); + postprocess (S); return UNSAT; } + + if (!S->backforce) + printDependencies (S, NULL, 0); + + if (S->mode == FORWARD_SAT) { + printf ("\rc ERROR: found empty clause during SAT check\n"); exit (0); } + printf ("\rc detected empty clause; start verification via backward checking\n"); + + S->forced = S->processed; + assert (S->mode == BACKWARD_UNSAT); // only reachable in BACKWARD_UNSAT mode + + S->nOpt = 0; + + int checked = 0, skipped = 0; + + double max = (double) adds; + + struct timeval backward_time; + gettimeofday (&backward_time, NULL); + for (; step >= 0; step--) { + struct timeval current_time; + gettimeofday (¤t_time, NULL); + int seconds = (int) (current_time.tv_sec - S->start_time.tv_sec); + if ((seconds > S->timeout) && (S->optimize == 0)) printf ("s TIMEOUT\n"), exit (0); + + if (S->bar) + if ((adds % 1000) == 0) { + int f; + long runtime = (current_time.tv_sec - backward_time.tv_sec ) * 1000000 + + (current_time.tv_usec - backward_time.tv_usec); + double time = (double) (runtime / 1000000.0); + double fraction = (adds * 1.0) / max; + printf("\rc %.2f%% [", 100.0 * (1.0 - fraction)); + for (f = 1; f <= 20; f++) { + if ((1.0 - fraction) * 20.0 < 1.0 * f) printf(" "); + else printf("="); } + printf("] time remaining: %.2f seconds ", time / (1.0 - fraction) - time); + if (step == 0) printf("\n"); + fflush (stdout); } + + long ad = S->proof[step]; long d = ad & 1; + int *clause = S->DB + (ad >> INFOBITS); + + + if (ad == 0) continue; // Skip lemma that has been removed from proof + if ( d == 0) { + adds--; + if (clause[1]) { + removeWatch (S, clause, 0), removeWatch (S, clause, 1); + if (S->reason[abs (clause[0])] == (clause + 1 - S->DB)) { // use this check also for units? + unassignUnit (S, clause[0]); } } + else unassignUnit (S, clause[0]); } + + int size = sortSize (S, clause); + + if (d) { + if (S->verb) { printf ("\rc adding clause (%i) ", size); printClause (clause); } + addWatch (S, clause, 0), addWatch (S, clause, 1); continue; } + + S->time = clause[ID]; + if ((S->time & ACTIVE) == 0) { + skipped++; +// if ((skipped % 100) == 0) printf("c skipped %i, checked %i\n", skipped, checked); + continue; } // If not marked, continue + + assert (size >= 1); + int *_clause = clause + size; + while (*_clause++) { S->nRemoved++; } + clause[size] = 0; + + if (S->verb) { + printf ("\rc validating clause (%i, %i): ", clause[PIVOT], size); printClause (clause); } + + if (redundancyCheck (S, clause, size, 1) == FAILED) { + printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); + return SAT; } + checked++; + S->optproof[S->nOpt++] = ad; } + + postprocess (S); + return UNSAT; } + +long matchClause (struct solver* S, long *clauselist, int listsize, int* input, int size) { + int i, j; + for (i = 0; i < listsize; ++i) { + int *clause = S->DB + clauselist[i]; + for (j = 0; j <= size; j++) + if (clause[j] != input[j]) goto match_next; + + long result = clauselist[i]; + clauselist[i] = clauselist[--listsize]; + return result; + match_next:; } + return 0; } + +unsigned int getHash (int* input) { + unsigned int sum = 0, prod = 1, xor = 0; + while (*input) { + prod *= *input; sum += *input; xor ^= *input; input++; } + return (1023 * sum + prod ^ (31 * xor)) % BIGINIT; } + +int read_lit (struct solver *S, int *lit) { + int l = 0, lc, shift = 0; + do { + lc = getc_unlocked (S->proofFile); + S->nReads++; + if ((shift == 0) && (lc == EOF)) return EOF; + l |= (lc & 127) << shift; + shift += 7; } + while (lc > 127); + if (l % 2) *lit = (l >> 1) * -1; + else *lit = (l >> 1); + return 1; } + +void deactivate (struct solver *S) { + S->nActive = 0; + int step; + for (step = 0; step < S->nStep; step++) { + if ((S->proof[step] & 1) == 0) { + int *clause = S->DB + (S->proof[step] >> INFOBITS); + if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE; } } +} + +void shuffleProof (struct solver *S, int iteration) { + int i, step, _step; + + double base = 100; + for (i = 1; i < iteration; i++) + base *= 1.1; + + // randomly remove clause deletion steps + for (_step = 0, step = 0; step < S->nStep; step++) { + if (S->proof[step] & 1) { + int length = 0; + int *clause = S->DB + (S->proof[step] >> INFOBITS); + while (*clause) { length++; clause++; } + if ((rand() % 1000) < (base * iteration / length)) continue; } + S->proof[_step++] = S->proof[step]; } + S->nStep = _step; + + for (step = S->nStep - 1; step > 0; step--) { + long a = S->proof[step ]; + if (a & DBIT) continue; + long b = S->proof[step-1]; + if (b & DBIT) { + S->proof[step ] = b; + S->proof[step-1] = a; } + else { + int *c = S->DB + (a >> INFOBITS); + int *d = S->DB + (b >> INFOBITS); + int coinflip = 0; +// int coinflip = rand () / (RAND_MAX >> 1); + if (c[MAXDEP] < d[MAXDEP] || (coinflip && (c[MAXDEP] < d[ID]))) { + int tmp = d[ID]; + d[ID] = c[ID]; + c[ID] = tmp; + S->proof[step ] = b; + S->proof[step-1] = a; } } } + + for (step = 0; step < S->nStep; step++) { + long ad = S->proof[step]; + if (ad & 1) continue; + int *clause = S->DB + (ad >> INFOBITS); + int i, length = 0; + while (*clause) { length++; clause++; } + clause = S->DB + (ad >> INFOBITS); + for (i = 0; i < length - 1; i++) { + int j = i + rand() / (RAND_MAX / (length - i) + 1); + int t = clause[i]; clause[i] = clause[j]; clause[j] = t; } } } + +int parse (struct solver* S) { + int tmp, active = 0, retvalue = SAT; + int del = 0, fileLine = 0; + int *buffer, bufferAlloc; + + S->nVars = 0; + S->nClauses = 0; + do { tmp = fscanf (S->inputFile, " cnf %i %li \n", &S->nVars, &S->nClauses); // Read the first line + if (tmp > 0 && tmp != EOF) break; tmp = fscanf (S->inputFile, "%*s\n"); } // In case a commment line was found + while (tmp != 2 && tmp != EOF); // Skip it and read next line + int nZeros = S->nClauses; + + if (!S->nVars && !S->nClauses) { + printf ("\rc ERROR: did not find p cnf line in input file\n"); exit (0); } + + printf ("\rc parsing input formula with %i variables and %li clauses\n", S->nVars, S->nClauses); + + bufferAlloc = INIT; + buffer = (int*) malloc (sizeof (int) * bufferAlloc); + + S->count = 1; + S->nStep = 0; + S->mem_used = 0; // The number of integers allocated in the DB + + long size; + long DBsize = S->mem_used + BIGINIT; + S->DB = (int*) malloc (DBsize * sizeof (int)); + if (S->DB == NULL) { free (buffer); return ERROR; } + + S->maxVar = 0; + S->maxSize = 0; + S->nLemmas = 0; + S->nAlloc = BIGINIT; + S->formula = (long *) malloc (sizeof (long) * S->nClauses); + S->proof = (long *) malloc (sizeof (long) * S->nAlloc); + long **hashTable = (long**) malloc (sizeof (long*) * BIGINIT); + int *hashUsed = (int * ) malloc (sizeof (int ) * BIGINIT); + int *hashMax = (int * ) malloc (sizeof (int ) * BIGINIT); + + int i; + for (i = 0; i < BIGINIT; i++) { + hashUsed [i] = 0; + hashMax [i] = INIT; + hashTable[i] = (long*) malloc (sizeof (long) * hashMax[i]); } + + int fileSwitchFlag = 0; + long finalClause = 0; + size = 0; + while (1) { + int lit = 0; tmp = 0; + fileSwitchFlag = nZeros <= 0; + + if (size == 0) { + if (fileSwitchFlag) { // read for proof + if (S->binMode == 1) { + int res = getc_unlocked (S->proofFile); + if (res == EOF) break; + else if (res == 97) del = 0; + else if (res == 100) del = 1; + else { + if (S->warning != NOWARNING) { + printf ("\rc WARNING: wrong binary prefix, stop reading proof\n"); break; } + if (S->warning == HARDWARNING) exit (HARDWARNING); } + S->nReads++; } + else { + tmp = fscanf (S->proofFile, " d %i ", &lit); + if (tmp == EOF) break; + del = tmp > 0; } } } + + if (!lit) { + if (!fileSwitchFlag) tmp = fscanf (S->inputFile, " %i ", &lit); // Read a literal. + else { + if (S->binMode == 1) { + tmp = read_lit (S, &lit); } + else { + tmp = fscanf (S->proofFile, " %i ", &lit); } } + if (tmp == EOF && !fileSwitchFlag) { + if (S->warning != NOWARNING) { + printf ("\rc WARNING: early EOF of the input formula\n"); + printf ("\rc WARNING: %i clauses less than expected\n", nZeros); } + if (S->warning == HARDWARNING) exit (HARDWARNING); + fileLine = 0; + fileSwitchFlag = 1; } } + + if (!tmp && !S->binMode) { + char ignore[1<<16]; + if (!fileSwitchFlag) { if (fgets (ignore, sizeof (ignore), S->inputFile) == NULL) printf ("c\n"); } + else if (fgets (ignore, sizeof (ignore), S->proofFile) == NULL) printf ("c\n"); + if (ignore[0] != 'c') continue; + for (i = 0; i < sizeof ignore; i++) { if (ignore[i] == '\n') break; } + if (i == sizeof ignore) { + printf ("c ERROR: comment longer than %zu characters: %s\n", sizeof ignore, ignore); + exit (HARDWARNING); } + if (S->verb) printf ("\rc WARNING: parsing mismatch assuming a comment\n"); + continue; } + + if (abs (lit) > S->maxVar) S->maxVar = abs (lit); + if (tmp == EOF && fileSwitchFlag) break; + if (abs (lit) > S->nVars && !fileSwitchFlag) { + printf ("\rc illegal literal %i due to max var %i\n", lit, S->nVars); exit (0); } + if (!lit) { + fileLine++; + if (size > S->maxSize) S->maxSize = size; + int pivot = buffer[0]; + buffer[size] = 0; + qsort (buffer, size, sizeof (int), compare); + int j = 0; + for (i = 0; i < size; ++i) { + if (buffer[i] == buffer[i+1]) { + if (S->warning != NOWARNING) { + printf ("\rc WARNING: detected and deleted duplicate literal %i at position %i of proof line %i\n", buffer[i+1], i+1, fileLine); } + if (S->warning == HARDWARNING) exit (HARDWARNING); } + else { buffer[j++] = buffer[i]; } } + buffer[j] = 0; size = j; + + if (size == 0 && !fileSwitchFlag) retvalue = UNSAT; + if (del && S->mode == BACKWARD_UNSAT && size <= 1) { + if (S->warning != NOWARNING) { + printf ("\rc WARNING: backward mode ignores deletion of (pseudo) unit clause "); + printClause (buffer); } + if (S->warning == HARDWARNING) exit (HARDWARNING); + del = 0; size = 0; continue; } + int rem = buffer[0]; + buffer[size] = 0; + unsigned int hash = getHash (buffer); + if (del) { + if (S->delete) { + long match = 0; + match = matchClause (S, hashTable[hash], hashUsed[hash], buffer, size); + if (match == 0) { + if (S->warning != NOWARNING) { + printf ("\rc WARNING: deleted clause on proof line %i does not occur: ", fileLine); printClause (buffer); } + if (S->warning == HARDWARNING) exit (HARDWARNING); + goto end_delete; } + if (S->mode == FORWARD_SAT) S->DB[ match - 2 ] = rem; + hashUsed[hash]--; + active--; + if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1; + S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); +// printf ("c proof allocation increased to %li\n", S->nAlloc); + if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + S->proof[S->nStep++] = (match << INFOBITS) + 1; } + end_delete:; + if (del) { del = 0; size = 0; continue; } } + + if (S->mem_used + size + EXTRA >= DBsize) { DBsize = (DBsize * 3) >> 1; + S->DB = (int *) realloc (S->DB, DBsize * sizeof (int)); +// printf("c database increased to %li\n", DBsize); + if (S->DB == NULL) { printf("c MEMOUT: reallocation of clause database failed\n"); exit (0); } } + int *clause = &S->DB[S->mem_used + EXTRA - 1]; + if (size != 0) clause[PIVOT] = pivot; + clause[ID] = 2 * S->count; S->count++; + finalClause = S->mem_used + EXTRA - 1; + if (S->mode == FORWARD_SAT) if (nZeros > 0) clause[ID] |= ACTIVE; + + for (i = 0; i < size; ++i) { clause[ i ] = buffer[ i ]; } clause[ i ] = 0; + S->mem_used += size + EXTRA; + + hash = getHash (clause); + if (hashUsed[hash] == hashMax[hash]) { hashMax[hash] = (hashMax[hash] * 3) >> 1; + hashTable[hash] = (long *) realloc (hashTable[hash], sizeof (long*) * hashMax[hash]); + if (hashTable[hash] == NULL) { printf("c MEMOUT reallocation of hash table %i failed\n", hash); exit (0); } } + hashTable[ hash ][ hashUsed[hash]++ ] = (long) (clause - S->DB); + + active++; + if (nZeros > 0) { // if still parsing the formula + S->formula[S->nClauses - nZeros] = (((long) (clause - S->DB)) << INFOBITS); } + else { + if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1; + S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); +// printf ("c proof allocation increased to %li\n", S->nAlloc); + if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + S->proof[S->nStep++] = (((long) (clause - S->DB)) << INFOBITS); } + + if (nZeros <= 0) S->nLemmas++; + + if (!nZeros) S->lemmas = (long) (clause - S->DB); // S->lemmas is no longer pointer + size = 0; del = 0; --nZeros; } // Reset buffer + else { + buffer[size++] = lit; // Add literal to buffer + if (size == bufferAlloc) { bufferAlloc = (bufferAlloc * 3) >> 1; + buffer = (int*) realloc (buffer, sizeof (int) * bufferAlloc); + if (buffer == NULL) { + printf ("c MEMOUT: failed to reallocate buffer\n"); exit (0); } } } } + + if (S->mode == FORWARD_SAT && active) { + if (S->warning != NOWARNING) + printf ("\rc WARNING: %i clauses active if proof succeeds\n", active); + if (S->warning == HARDWARNING) exit (HARDWARNING); + for (i = 0; i < BIGINIT; i++) { + int j; + for (j = 0; j < hashUsed[i]; j++) { + printf ("\rc "); + int *clause = S->DB + hashTable [i][j]; + printClause (clause); + if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1; + S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); +// printf ("c proof allocation increased to %li\n", S->nAlloc); + if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + S->proof[S->nStep++] = (((long) (clause - S->DB)) << INFOBITS) + 1; } } } + + S->DB = (int *) realloc (S->DB, S->mem_used * sizeof (int)); + if (S->mem_used && S->DB == NULL) { printf("c MEMOUT: reallocation of DB failed\n"); exit (0); } + + for (i = 0; i < BIGINIT; i++) free (hashTable[i]); + free (hashTable); + free (hashUsed); + free (hashMax); + free (buffer); + + int *clause = &S->DB[finalClause]; + if (clause) clause[ID] |= ACTIVE; // temporary + + printf ("\rc finished parsing"); + if (S->nReads) printf (", read %li bytes from proof file", S->nReads); + printf ("\n"); + + int n = S->maxVar; + S->falseStack = (int *) malloc (( n + 1) * sizeof (int )); // Stack of falsified literals -- this pointer is never changed + S->reason = (long *) malloc (( n + 1) * sizeof (long)); // Array of clauses + S->used = (int *) malloc ((2 * n + 1) * sizeof (int )); S->used += n; // Labels for variables, non-zero means false + S->max = (int *) malloc ((2 * n + 1) * sizeof (int )); S->max += n; // Labels for variables, non-zero means false + S->falseA = (int *) malloc ((2 * n + 1) * sizeof (int )); S->falseA += n; // Labels for variables, non-zero means false + S->setMap = (int *) malloc ((2 * n + 1) * sizeof (int )); S->setMap += n; // Labels for variables, non-zero means false + S->setTruth = (int *) malloc ((2 * n + 1) * sizeof (int )); S->setTruth += n; // Labels for variables, non-zero means false + + S->optproof = (long *) malloc (sizeof(long) * (2 * S->nLemmas + S->nClauses)); + + S->maxRAT = INIT; + S->RATset = (long*) malloc (sizeof (long) * S->maxRAT); + for (i = 0; i < S->maxRAT; i++) S->RATset[i] = 0; // is this required? + + S->preRAT = (int*) malloc (sizeof (int) * n); + + S->lratAlloc = INIT; + S->lratSize = 0; + S->lratTable = (int *) malloc (sizeof(int ) * S->lratAlloc); + S->lratLookup = (long *) malloc (sizeof(long) * (S->count + 1)); + + S->maxDependencies = INIT; + S->dependencies = (int*) malloc (sizeof (int) * S->maxDependencies); + for (i = 0; i < S->maxDependencies; i++) S->dependencies[i] = 0; // is this required? + + S->wlist = (long**) malloc (sizeof (long*) * (2*n+1)); S->wlist += n; + + for (i = 1; i <= n; ++i) { S->max [ i] = S->max [-i] = INIT; + S->setMap [ i] = S->setMap [-i] = 0; + S->setTruth[ i] = S->setTruth[-i] = 0; + S->wlist [ i] = (long*) malloc (sizeof (long) * S->max[ i]); + S->wlist [-i] = (long*) malloc (sizeof (long) * S->max[-i]); } + + S->unitStackSize = INIT; + S->unitStack = (long *) malloc (sizeof (long) * S->unitStackSize); + + return retvalue; } + +void freeMemory (struct solver *S) { + free (S->DB); + free (S->falseStack); + free (S->reason); + free (S->proof); + free (S->formula); + int i; + for (i = 1; i <= S->maxVar; ++i) { free (S->wlist[i]); free (S->wlist[-i]); } + free (S->used - S->maxVar); + free (S->max - S->maxVar); + free (S->falseA - S->maxVar); + free (S->wlist - S->maxVar); + free (S->RATset); + free (S->dependencies); + return; } + +int onlyDelete (struct solver* S, int begin, int end) { + int step; + for (step = begin; step < end; step++) + if ((S->proof[step] & 1) == 0) return 0; + return 1; } + +void printHelp ( ) { + printf ("usage: drat-trim [INPUT] [] [