diff --git a/research/e8-rank8-rigidity-small-deletions/LICENSE b/research/e8-rank8-rigidity-small-deletions/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/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/e8-rank8-rigidity-small-deletions/MANIFEST.sha256 b/research/e8-rank8-rigidity-small-deletions/MANIFEST.sha256 new file mode 100644 index 0000000000..57a044d410 --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/MANIFEST.sha256 @@ -0,0 +1,64 @@ +1a26d6839a349750e9a65f820a0cb925fc45127ef6c954e7091a46b286bc2892 checks/core.py +fa2a4ea5d20353acc39722b0364020b5845ce413a1bce7fa99a869ce6509ce16 checks/cube.cpp +b86994a83f8e0641eda25229d4e003bc3a72a18c400adc346c6c17e6f60a7629 checks/cubes_check.py +71ab2a9dc5a294ad8fba4ccb8c45aaa8a439596d314a2a046ac9b62266872a18 checks/DRAT-TRIM-LICENSE +d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee checks/drat-trim.c +b1a0339383cc4ae6957caec6a9feffb9fb344679cceeff8eca49996ff21bcf4d checks/e8lib.py +8f23b1bc7e40095339e92b430659071c0e45ed486aa7d4075a41399865c1d77b checks/export.py +e8b8ca1e63ca3390cbbc5cd9fd063a50345a206158f31d6445901b289e252ca3 checks/grp.py +a6fae8f8b2e00eb9562463c49caf4b861f5dd3072bf791d6625d8ebdd5b733ed checks/hf.cpp +d2c8b3fb1f0a04db654a61c3df67ee0f2e0231de21cb180c74321159052090e4 checks/hf40.cpp +012739ff3dc3421c187ca089b361c0b1d49f808908a5a7efdb0603c20f08ca71 checks/manifest_check.py +e6dd17c474b51cfda8c5e6d2e944d44db3662fd6d70d7aaaf72d040040bf4784 checks/mktid.py +feed7163c80bb3c64d8bbc7083cadc116f5bfd81b0d47d93ecefa1a12e0d8286 checks/prep.py +6852eaf02bb8f3a3f180abc0de22467f50d6f9acc5cb2b8299aab787684e8252 checks/regen.py +773e840271dca361eb0b2575d9afb5b24a36db8300a05a3587c436b1edc00d0f checks/s.c +a812f7bbfc7653f7d517849881811e5a6aac48cc64bfaa83173a52cd8b0fbbfc data/cnf_sha256.txt +bda9dfb4ab72ea63f1071c8f2964afb4a2df83e84ecd13edc5e80366875de8c3 data/core0_frames.json +508ca5cab2212d7ff997364cb121ae1b0457f94b216a243ba844212014e3da29 data/core1_frames.json +12640d4873c202590b3600a1325d70af032c5ccedcc06456c2407bfe968e5a26 data/core2_frames.json +7af3ac1326d41460dc2aa59cc6f1187e3d52d5fb1eb97a8a761ba7f8ea801a7d data/core3_frames.json +56c6c3042b849a7f6b0da6a5d2c2ee3cc5a527336e02a0a67a805dcd2a3dbd8b data/core4_frames.json +462999ebbf3502f0b950dfabc0709da42cf6c1491f67bcedf2f854291f5d5ef7 data/core5_frames.json +8088785c40f83190519c09635f68c63b80c0c789d0349ac059b2a94bb29e4702 data/core6_frames.json +093d49f7d76bfaec37d31f15b099b24ff291812954ff29b9233583510f67d2b3 data/core7_frames.json +c9afeafc2203bc863a68c19fceced25397cfd60869342654293b3ec32c3d23d6 data/core8_frames.json +88174d84ef99299b37da99689ac023922f2d6d63d5c7d92edb52033a2105ecc1 data/core9_frames.json +f4b3e093be3533de02e0e3ed2f474b6b4e08854392e615792e81ecdbac4bfd29 data/cores_v.json +117ab52b74ebb201f71003d06738cba6a4c96829bd052d35a9ff15faf00f9cfb data/cubes4.txt +e3d3ac27b8511040740da2dbbd72580eff771a9f2915c2ae6c4c9bb688fecc92 data/proofs/core0.drat.xz +b986869dcca5da0b64a59ff5f695bd138ba7ee1292e0123ffa146331fa43525a data/proofs/core1.drat.xz +ea736b0d6f91aa46b9631b01081e841ae1de6b42c81844f0a5ca795b2f4d2a63 data/proofs/core2.drat.xz +56e901e4c829239cae90104113db0491c3bd8986c5de31f86d320c0ba4d22791 data/proofs/core3.drat.xz +a807408f46cbb685b39ab98d9e0fbdbc5774147cfc975ea761758138d9feccde data/proofs/core4.drat.xz +691206367deed932cca62431c206eeaa62b56a7ed9d62ea256c2df229d0a976d data/proofs/core5.drat.xz +c151dee8e1e002c97e927024aacbb4be04324a537adaa05c9cfa818ef8dcad9f data/proofs/core6.drat.xz +bf51c43e8a06fd2333a175c0781a4fcff8da8889e4a929f7c633014e40a2adf8 data/proofs/core7.drat.xz +0b1d1c42e98ded52f91a00babe0fb74f6acaede4ab1d3c94a7a85dc4eb5a61fc data/proofs/core8.drat.xz +88d203b1b40dd4aed4e33b441a3718569f4ac00b15ec7b2d069a319820f76ef8 data/proofs/core9.drat.xz +5a6fc980e16e68fd86a52c202953192e1703baef6a916c872b4c1d5b4ce6bd46 evidence/cubev8.out +63a136ad6e62b07cc6ec2a60761f67ea14fc60cb0e01065f353a7c98c6c0ae1c evidence/R1-RIG3/fr_40.out +e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 evidence/R1-RIG3/fr_c0.out +b55d4d4cf96443bcb55954b0df1c87434cbea211209adfb85aad9ea6e53e3756 evidence/R1-RIG3/fr_full.out +b43f9d97734ee3852ff55e1073913c28f68f77b57bcddce63b4a4fcaf5005eb0 evidence/R1-RIG3/frn.out +6c28137830e305c7202afd2c0b926dd2157b3b7a495ca202638b85cfd1c7ee50 evidence/R1-RIG3/h8_o0_j0.out +a23330a62c87b1875fe6423df3dad66064187162a754453b5b19f3a8bb45d18f evidence/R1-RIG3/h8_o0_j1.out +8b60123605700339115a31246744a9f37a3c362fa6d23a98578907a20f3b261c evidence/R1-RIG3/h8_o0_j2.out +a32d62b664f0af8e732a7bafa0b7dd8a3b50c132c9b1172ba0916416c7930a09 evidence/R1-RIG3/h8_o0.out +cf8e7e87ea8a4e751712661d9ef62c5432351574d0d7df47cf351c7de22bbb77 evidence/R1-RIG3/h8_o1.out +a443bdb32ab83bca03c167016628012165a55551b28f93ef623a8b8d246e8ad2 evidence/R1-RIG3/h8_o2.out +cc2a8cecac4ffb67397829e1b9e0bb4dd1a22b7740ae28951988ca0f5f4c6f7b evidence/R1-RIG3/h8_o3.out +5e33d391cbdf352cf2dd1596258f66f7807f5f3ae50f7d49ef4356877e3b9fbc evidence/R1-RIG3/h8_o4.out +8e9d97cc45c3a4825bc05b58b680c78410354d3ed1e8bbfd0ee477839343f699 evidence/R1-RIG3/h9_0.out +12604f4097a3194704f7c1691342d8f982c6fafba2fa778fb6f8b8abc8a8decf evidence/R1-RIG3/h9_1.out +aafb2d2043c7eba6c4f50fbb1c5097e4041d89d10d049d7d51c68e28409998e0 evidence/R1-RIG3/h9_3.out +f17cd5a1149186088901478cf1a7feb98b8c44f8fba5cdc289c8ced1e858ac5e evidence/R1-RIG3/h9_4.out +488fb541f9853ae6e95b6af758d9aef1ed2e440faa6962c6168612ce70c61db9 evidence/R1-RIG3/h9_6.out +fe91d98af147f26f294e7b40cb782042a98fe604a984ebf486227844f8a12c63 evidence/R1-RIG3/h9_7.out +ee2b9886287749f8e5663e0a5fc890f05fc438464374649c1d37d5b15f4dbbaa evidence/verify_default.log +c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE +1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec NOTICE.md +ec890e1604f840e20ef88dc904399a770e75e502a2a357bc63f5991f76a4e0bb PROOF_MAP.md +1a4c698a5976f3faff9a0406296343210b45483c48189d37921c23129032bf67 README.md +4ddc9fac6812009f664a46c80b8fd573c9f2bcc4ac391cca9531ca94cd432e63 requirements.txt +4cc21114f55d317dd2dc3236910d4e9c074b95fecbddc75363caa27275b44310 verify.sh diff --git a/research/e8-rank8-rigidity-small-deletions/NOTICE.md b/research/e8-rank8-rigidity-small-deletions/NOTICE.md new file mode 100644 index 0000000000..c6f3494c2c --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/NOTICE.md @@ -0,0 +1,3 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). diff --git a/research/e8-rank8-rigidity-small-deletions/PROOF_MAP.md b/research/e8-rank8-rigidity-small-deletions/PROOF_MAP.md new file mode 100644 index 0000000000..ea883351fa --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/PROOF_MAP.md @@ -0,0 +1,23 @@ +# Claim to check map + +Every claim is a line here; "step" refers to `verify.sh`. PROVEN = argument in README; CHECKED = recomputed; CONDITIONAL = cited, not rerun. + +| # | claim | status | where | +|---|---|---|---| +| A1 | The zero-pattern model (variables `z(u,s)`, tetrad rules, Gram-frame rules) is a necessary-conditions abstraction of "rank <= 8, forced zeros, other entries free" | CONDITIONAL (from #2864): generator `checks/core.py` is the rule set of `research/e8-rank9-extra-zeros/` (Theorem RK, `checks/rkz.py`, rule proofs in `evidence/ZPIN*_THEORY_snapshot.md`) restricted to a line subset; #2864's README proves Theorem RK from its two CNFs (rk7, rk8), not the restriction use, and we do not re-prove rule soundness | `checks/core.py` | +| A2 | Rank is monotone under restriction to `U <= L'`, so a refutation on `U` refutes every `L' containing U` | PROVEN (trivial) | README | +| A3 | `W(E8)` is transitive on ordered non-orthogonal line pairs (orbit of (0,2) has 6720 = all such pairs) | CHECKED | step 2 (`grp.py`) | +| A4 | `W(E6)` (generated by reflections in E6 roots orthogonal to lines 0, 2) has order 51840, fixes 0 and 2, so maps cores to cores | CHECKED | step 2 | +| B1 | Ten cores (`data/cores_v.json`, 27..38 lines) have UNSAT zero-pattern models with goal `z(0,2)`; CNFs regenerate to pinned sha256 (`data/cnf_sha256.txt`) from `data/core*_frames.json` | CHECKED | step 4 (`regen.py`) | +| B2 | Shipped DRAT proofs (`data/proofs/*.xz`, kissat 4 `--factor=false --preprocessfactor=false`) verify with drat-trim | CHECKED | step 4 | +| C1 | `data/cubes4.txt` (1402 lines) is a complete set of `W(E6)` orbit representatives of 4-subsets of the 118 lines (pairwise inequivalent and equal in number to the Burnside count) | CHECKED | step 3 (`cubes_check.py`) | +| C2 | HIT: no `D`, `|D| <= 8`, avoiding lines 0, 2, meets every `W(E6)`-image of every core (implementation 1: `cube.cpp`, DFS with top-r coverage bound over the 1402 cubes, `D` padded to size 8) | CHECKED (exhaustive, no proof object) | step 5 | +| C3 | HIT, independent implementation (`s.c`, orbit-ordered DFS, disjoint-packing bound, written independently) | CHECKED: orbits 1..4 in default; orbit 0 (3 chunks) with `FULL=1`; original logs `evidence/R1-RIG3/h8_*.out` | steps 7, 8 | +| C4 | Control: the same HIT search finds a hitting `D` of size 12, so the size-8 negative is not vacuous | CHECKED | step 5 (`cube ... 12 4 stop` control) | +| C5 | Consequence of A2-C3: for every `D`, `|D| <= 8`, Step 1 (no extra zero on `E8 \ D`) holds | PROVEN from A1-A4, B1, B2, C1, C2 | README | +| D1 | FRAMES (hf.cpp): no `D`, `|D| <= 8`, has two lines in one tetrad of every one of the 2025 frames (roots: both `W(E8)` orbits of line pairs: non-orth (0,2) and orth (0,x)) | CHECKED (exhaustive) | step 6 | +| D2 | FRAMES independent implementation (`s.c fr`): case C (D pairwise orthogonal) and case N (D contains 0, 2 and an orbit representative) | CHECKED: case C and N orbits 3, 4 default; N orbits 0..2 with `FULL=1` (original single run `evidence/R1-RIG3/fr_full.out`, 1377 CPU-s) | steps 7, 8 | +| D3 | Control: with the first 40 frames a bad `D` exists (verified in the original card in Python) | CHECKED in both implementations | steps 6, 7 | +| E1 | Step 2 (iff pattern implies Gram): the frame calculus of #2819/#1212 Theorem P runs on a frame inside `L'` with every tetrad meeting `D` in <= 1 line | CONDITIONAL (#2819 / #2864 Step 2, `pcompK.py`); the existence of such a frame for all `|D| <= 8` is D1/D2 | README | +| F | Conclusion: Lemma RIGD hypothesis (1) holds for every `|D| <= 8` | PROVEN from C5, D1/D2, E1 (hypotheses (2), (3) were proved in the R1 theory text of #2864) | README | +| G | R1 for arbitrarily many extra zeros | NOT CLAIMED (open) | README | diff --git a/research/e8-rank8-rigidity-small-deletions/README.md b/research/e8-rank8-rigidity-small-deletions/README.md new file mode 100644 index 0000000000..e9ccc91a52 --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/README.md @@ -0,0 +1,20 @@ +# Rank-8 rigidity of the E8 pattern after deleting at most 8 lines (closes hypothesis (1) of Lemma RIGD for |D| <= 8; no kappa claim) + +> **Scope.** Pure matrix classification on the E8 unit (120 lines). **No kappa claim**, no window, no supplier, no decoder cost. R1 for an **arbitrary** number of extra zeros is **not** claimed and stays open (see "Not claimed"). +> Labels: **PROVEN** (written argument), **CHECKED** (recomputed by `verify.sh`; SAT steps are kissat UNSAT with a DRAT proof accepted by the standard `drat-trim`; the exhaustive searches are plain C/C++ DFS, no proof object, but two independent implementations), **CONDITIONAL** (inherited, cited). +> **Credit.** The problem (R1/R2/R3, universal rigidity R2 for the complement of a small set, normal forms) is philippeVV's (Discussion #1587). Rank-8 rigidity with the full iff pattern is #1212. The zero-pattern SAT model and the frame calculus are those of the merged package `research/e8-rank9-extra-zeros/` (#2864, Theorem RK) and `research/e8-rank9-realisations/` (#2819). + +## Result +Setting (as #2864 Theorem RK): `D` a set of at most 8 lines of E8, `L' = E8 \ D`; `N` a matrix over a field of characteristic 0 indexed by `L'`, rank <= 8, `N_tt != 0`, `N_ts = 0` for `t` orthogonal to `s`, all other entries free (extra zeros allowed). **Then `N` has no extra zero and `N = D1 G D2` with `D1, D2` invertible** (a root realisation). #2864 proves this for `D` a clique; here `D` is **arbitrary** with `|D| <= 8`. This is hypothesis (1) of Lemma RIGD (the rank-8 rigidity hypothesis) for all `|D| <= 8`. + +## Proof structure (details and the claim-to-check map: `PROOF_MAP.md`) +* **Step 1 (no extra zero).** Rank is monotone under restriction. If a local core `U` (a set of lines containing the pair `(u0, s0)` and some E8 frames inside `U`) has an UNSAT zero-pattern model with goal `N_{u0 s0} = 0`, then no `N` on any `L' containing U` has that zero. `W(E8)` is transitive on ordered non-orthogonal pairs (orbit 6720), so `(u0, s0) = (0, 2)`; the stabiliser `W(E6)` (order 51840) maps cores to cores. Ten cores (27 to 38 lines) have UNSAT models (DRAT checked). Step 1 holds for `D` iff `D` (not containing 0, 2) misses at least one `W(E6)`-image of some core; exhaustive search: **no `D` with `|D| <= 8` meets all images** (two implementations). +* **Step 2 (iff pattern implies Gram).** With no extra zero `N` has the iff pattern; the frame calculus of #2819 (Theorem P, #1212's argument) needs one frame `F` inside `L'` in which each of the 14 tetrads holds at most one line of `D`. Exhaustive search: **no `D` with `|D| <= 8` meets two lines of a tetrad in every one of the 2025 frames** (two implementations; the search is run for the two `W(E8)` orbits of line pairs as roots). + +## Not claimed +* R1 for an arbitrary number of extra zeros (the P/A/Sigma/S steps without the per-line budget): **open**. This package only supplies the rigidity input for `|D| <= 8`; it does not remove the per-row / per-column budget of #2864 Theorem Z3'. +* Larger `D` (`|D| = 9`: the same searches were run as a probe only: HIT with 9 found none in the sampled orbits (logs `evidence/R1-RIG3/h9_*.out`), not part of `verify.sh` and not claimed). +* Inherited: the zero-pattern model's equivalence to Theorem RK is **assumed from #2864** (see `PROOF_MAP.md`, A1): #2864 ships the model generator and one-line rule proofs (`evidence/ZPIN*_THEORY_snapshot.md`) but its README does not state this exact core-restriction use; the CNF generator here (`checks/core.py`) is the same rule set specialised to a core, and its soundness is not re-proved here. + +## Verification +`bash verify.sh` (about 15 CPU-minutes by default; needs numpy, `cc`, `c++`, `xz`; drat-trim is built from the shipped `checks/drat-trim.c`, MIT, copyright in the file and `checks/DRAT-TRIM-LICENSE`). `FULL=1` adds the complete independent HIT and FRAMES searches (about 1.3 CPU-hours each, chunked, every chunk under 20 minutes). diff --git a/research/e8-rank8-rigidity-small-deletions/checks/DRAT-TRIM-LICENSE b/research/e8-rank8-rigidity-small-deletions/checks/DRAT-TRIM-LICENSE new file mode 100644 index 0000000000..9859ca161d --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/checks/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/e8-rank8-rigidity-small-deletions/checks/core.py b/research/e8-rank8-rigidity-small-deletions/checks/core.py new file mode 100644 index 0000000000..02ecc109af --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/checks/core.py @@ -0,0 +1,74 @@ +# Core search for Step 1: for a line set U (containing u0,s0) and frames inside U, is "N_{u0 s0}=0" refutable (zero-pattern model)? +import sys, random, subprocess, os, pickle +import os; sys.path.insert(0,os.path.dirname(os.path.abspath(__file__))) +from e8lib import E,N,G,O,frames +def build(L, FRs, FRall, goal, path): + L=sorted(L); var={}; cl=[] + def v(k): + if k not in var: var[k]=len(var)+1 + return var[k] + def Z(u,s): return v(('z',u,s)) + def T(u,f,s): + key=('t',u,f,s) + if key not in var: + t=v(key); a=[Z(p,q) for (p,q) in ((u,f),(f,s)) if p!=q] + for x in a: cl.append([-t,-x]) + cl.append([t]+a) + return var[key] + for F in FRs: + Fs=set(F) + for u in L: + if u in Fs: continue + Tu=[f for f in F if G[u][f]!=0] + for s in L: + if s in Fs: continue + I=[f for f in Tu if G[s][f]!=0] + ts=[T(u,f,s) for f in I] + if u==s: cl.append(ts); continue + if G[u][s]==0: + for i,t in enumerate(ts): cl.append([-t]+[x for j,x in enumerate(ts) if j!=i]) + else: + z=Z(u,s); cl.append([z]+ts) + for i,t in enumerate(ts): cl.append([-z,-t]+[x for j,x in enumerate(ts) if j!=i]) + for F in FRall: + Fs=set(F) + for w in L: + if w in Fs: continue + Tw=[f for f in F if G[w][f]!=0] + cl.append([-Z(w,f) for f in Tw]); cl.append([-Z(f,w) for f in Tw]) + cl.append([Z(*goal)]) + with open(path,'w') as fh: + fh.write('p cnf %d %d\n'%(len(var),len(cl))) + for c in cl: fh.write(' '.join(map(str,c))+' 0\n') + return {k:i for k,i in var.items() if k[0]=='z'} +def kissat(path, tl=1200, proof=None): + cmd=['kissat','--factor=false','--preprocessfactor=false','-q',path]+([proof] if proof else []) + r=subprocess.run(cmd,capture_output=True,text=True,timeout=tl) + return r.returncode, r.stdout +def cegar(L, goal, nfr=20, maxit=40, tag='c', seed=1, proof=None, tl=1200, verbose=True): + """returns (status, frames used). status 'UNSAT' (refuted) or 'SAT'""" + Ls=set(L); FR=frames(L); rnd=random.Random(seed) + FRs=FR if nfr>=len(FR) else rnd.sample(FR,nfr) + for it in range(maxit): + m=build(L,FRs,FR,goal,tag+'.cnf') + rc,out=kissat(tag+'.cnf',tl,proof) + if verbose: print(' it',it,'frames',len(FRs),'of',len(FR),'rc',rc,flush=True) + if rc==20: return 'UNSAT',FRs,FR + if rc!=10: return 'TIMEOUT',FRs,FR + val=set() + for line in out.splitlines(): + if line.startswith('v '): val|={int(x) for x in line[2:].split() if int(x)>0} + Zs=[(k[1],k[2]) for k,i in m.items() if i in val] + S=set(u for u,s in Zs)|set(s for u,s in Zs) + have=set(FRs) + sc=sorted([F for F in FR if F not in have],key=lambda F:-len(S&set(F))) + if not sc: return 'SAT',FRs,FR + FRs=FRs+sc[:10] + return 'MAXIT',FRs,FR +if __name__=='__main__': + u0=0; s0=[s for s in range(N) if G[0][s]!=0 and s!=0][0] + L=list(range(N)); print('goal',u0,s0) + st,FRs,FR=cegar(L,(u0,s0),tag='r1rig_full') + print(st,len(FRs)); U=set([u0,s0]); + for F in FRs: U|=set(F) + print('union size',len(U)) diff --git a/research/e8-rank8-rigidity-small-deletions/checks/cube.cpp b/research/e8-rank8-rigidity-small-deletions/checks/cube.cpp new file mode 100644 index 0000000000..803a778392 --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/checks/cube.cpp @@ -0,0 +1,41 @@ +#include +#include +#include +#include +#include +using namespace std; +typedef unsigned __int128 u128; +static int K; static long long nodes; +static inline bool has(u128 s,int e){return (s>>e)&1;} +static bool dfs(const vector&U, u128 excl, int r, vector&sol){ + nodes++; + if(U.empty()) return true; + if(r==0) return false; + int cnt[128]={0}; + for(u128 s: U){ u128 av=s&~excl; if(!av) return false; uint64_t lo=(uint64_t)av, hi=(uint64_t)(av>>64); + while(lo){int b=__builtin_ctzll(lo); cnt[b]++; lo&=lo-1;} while(hi){int b=__builtin_ctzll(hi); cnt[64+b]++; hi&=hi-1;} } + // top-r bound + int tmp[128]; int m=0; for(int e=0;e<128;e++) if(cnt[e]) tmp[m++]=cnt[e]; + sort(tmp,tmp+m,[](int a,int b){return a>b;}); + long long sum=0; for(int i=0;icnt[be])) be=e; + u128 b=((u128)1)< U2; U2.reserve(U.size()); + for(u128 s:U) if(!(s&b)) U2.push_back(s); + if(dfs(U2,excl,r-1,sol)){ sol.push_back(be); return true; } + return dfs(U,excl|b,r,sol); +} +int main(int argc,char**argv){ + K=atoi(argv[3]); FILE*f=fopen(argv[1],"rb"); vector fam; uint64_t a,b; while(fread(&a,8,1,f)==1&&fread(&b,8,1,f)==1) fam.push_back(((u128)b<<64)|a); fclose(f); + FILE*c=fopen(argv[2],"r"); int cs=atoi(argv[4]); // cube size + u128 base=((u128)1<<0)|((u128)1<<2); long long tot=0; int nc=0, found=0; + vector cube(cs); + while(true){ bool ok=true; u128 cm=0; for(int i=0;i U; for(u128 s:fam) if(!(s&cm)) U.push_back(s); + vector sol; nodes=0; bool r=dfs(U,base|cm,K-cs,sol); tot+=nodes; nc++; if(nc%50==0){fprintf(stderr,"cube %d nodes %lld\n",nc,tot);} + if(r){ found++; if(argc>5){ printf("FOUND cube"); for(int x:cube)printf(" %d",x); printf(" +"); for(int x:sol)printf(" %d",x); printf("\n"); return 0;} printf("FOUND cube"); for(int x:cube)printf(" %d",x); printf(" +"); for(int x:sol)printf(" %d",x); printf("\n"); fflush(stdout); } + } + fprintf(stderr,"cubes %d found %d total nodes %lld\n",nc,found,tot); + printf("DONE cubes %d found %d\n",nc,found); +} diff --git a/research/e8-rank8-rigidity-small-deletions/checks/cubes_check.py b/research/e8-rank8-rigidity-small-deletions/checks/cubes_check.py new file mode 100644 index 0000000000..0ed445257b --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/checks/cubes_check.py @@ -0,0 +1,26 @@ +# W(E6) = Stab of ordered pair (0,2) acting on 118 lines (W6.pkl from grp.py). Checks that data/cubes4.txt (GAP orbit reps of +# 4-subsets, 1-based) are pairwise inequivalent AND their number equals the Burnside orbit count => complete set of orbit reps. +import pickle,sys +import numpy as np +from math import comb +W=pickle.load(open('W6.pkl','rb')); A=np.array([list(p) for p in W],dtype=np.int64); print('group order',len(A)) +pts=[x for x in range(120) if x not in(0,2)] +assert len(pts)==118 +tot=0 +for p in A: + seen=[0]*120; cyc={} + for x in pts: + if seen[x]: continue + n=0;y=x + while not seen[y]: seen[y]=1;y=p[y];n+=1 + cyc[n]=cyc.get(n,0)+1 + c1,c2,c3,c4=[cyc.get(k,0) for k in(1,2,3,4)] + tot+=comb(c1,4)+comb(c1,2)*c2+comb(c2,2)+c1*c3+c4 +assert tot%len(A)==0; nb=tot//len(A); print('Burnside orbits of 4-subsets',nb) +reps=[tuple(int(x) for x in l.split()) for l in open(sys.argv[1]) if l.strip()] +keys=set() +for r in reps: + im=np.sort(A[:,list(r)],axis=1); k=(im[:,0]*120**3+im[:,1]*120**2+im[:,2]*120+im[:,3]).min(); keys.add(int(k)) +print('reps',len(reps),'distinct orbits',len(keys)) +assert len(reps)==len(keys)==nb and all(0 not in r and 2 not in r for r in reps) +print('PASS cubes4.txt is a complete set of W(E6)-orbit reps of 4-subsets (%d)'%nb) diff --git a/research/e8-rank8-rigidity-small-deletions/checks/drat-trim.c b/research/e8-rank8-rigidity-small-deletions/checks/drat-trim.c new file mode 100644 index 0000000000..cf8a676ffc --- /dev/null +++ b/research/e8-rank8-rigidity-small-deletions/checks/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] [] [