GATE D32

Khả-thực-hiện ngầm và nhân CEGAR biểu tượng: PARTIAL

partialEvidence I2Kiểm: doubleClaim công khai: Không2026-07-20

Điều gì thay đổi

D32 kiểm đường chưa-bị-bác còn lại, biểu diễn bài toán khả-thực-hiện toàn cục ngầm và tinh chỉnh bằng predicate chính xác thay vì liệt kê bất kỳ tích trạng thái cục bộ nào. Khảo sát định nghĩa một vòng trừu-tượng-tinh-chỉnh mà các predicate của nó, admissibility cục bộ, square lift hệ số cao nhất, bất đẳng thức dương và Newton, và square splitting, mỗi cái được chứng minh giữ mọi tuple governed, và trên miền hữu hạn đầy đủ vòng khớp liệt kê brute-force, gồm một trường hợp mà square splitting là tinh chỉnh chịu lực. Pha 1 triển khai một nhân biểu tượng thật với hai backend chính xác độc lập, một decision diagram thu gọn canonical và một engine miền-hữu-hạn độc lập. Lớp admissibility cục bộ nén thật: diagram dùng số node tuyến tính theo số prime trong khi biểu diễn tích đầy đủ, với materialization Cartesian bằng không. Ràng buộc ghép không nén trong các backend đã triển khai, vì cấu trúc của nó materialize một liệt kê bình-phương-bị-chặn hoặc tích, nên chi phí chuyển sang tiền xử lý. Kết quả tách-cục-bộ là một định lý được chứng minh; lớp ghép là obstruction đặc-thù-biểu-diễn, không phải phổ quát. LRC(13) vẫn mở.

Bằng chứng

kiểm 1Vòng trừu-tượng-tinh-chỉnh được chứng minh sound và chính xác trên miền hữu hạn đầy đủ; mỗi tinh chỉnh giữ mọi tuple governed; pilot khả-thực-hiện 34-trạng-thái được thiết lập bởi song ánh chứng minh, không bởi đếm bằng nhau; một trường hợp empty hai-vòng được chứng nhận trên miền của nó

kiểm 2Nhân biểu tượng: admissibility cục bộ nén về số node tuyến tính theo số prime trong khi biểu diễn tích đầy đủ với materialization Cartesian bằng không; cấu trúc ràng buộc ghép materialize một liệt kê bị chặn, chuyển chi phí sang tiền xử lý

kiểm 3D32-PARTIAL: một nén tách-cục-bộ PASS-THEORY được chứng minh, với obstruction lớp-ghép đặc-thù-biểu-diễn. V1 10/10, một backend thứ hai độc lập, corruption 560/560. Không PASS-implicit-seeding, không chiến dịch. Không BASE-SURVIVOR, không GLOBAL-WITNESS. LRC(13) MỞ

Kiểm chứng: double · I2 · 6 artifact (report, verifier, bộ tấn công, manifest SHA-256)

← Tất cả gate