C-D25-COMPOUNDING

Compounding clause D25 VALIDATED-BOUNDED (đo pilot): các clause thời-gian-hữu-tỉ COMPOUND trên nhánh reachable. Đo trên pilot: khoảng 32 thời gian hữu tỉ greedy giảm mẫu 4000 nhánh reachable xuống một nhúm, ở khoảng 0.95 sống sót mỗi clause. Từ tỉ lệ đó, khoảng 555 clause sẽ dự phóng đưa không gian residue reachable 2^84 xuống dưới cap 2^42. Con số ~555 đó là DỰ PHÓNG THĂM DÒ, KHÔNG phải bound chứng nhận: nó chưa tính các biến residue mới mỗi denominator mới đưa vào, tương quan giữa các clause, cỡ SAT / decision-diagram, chi phí proof-certificate, hay việc giữ một bộ chung xuyên mọi modulus. Nên compounding là lợi ích chất lượng thật so với D24, nhưng phát biểu cỡ-chiến-dịch chưa chứng minh

Nói dễ hiểu

Thêm nhiều đồng hồ riêng rõ ràng nhân pruning lên, và một đếm thô gợi ý vài trăm cái có thể thu nhỏ tìm kiếm dưới giới hạn. Đếm đó là ước lượng thăm dò, không phải chứng minh, vì nó bỏ qua vài chi phí thật.

Phát biểu chính xác

Compounding clause D25 VALIDATED-BOUNDED (đo pilot): các clause thời-gian-hữu-tỉ COMPOUND trên nhánh reachable. Đo trên pilot: khoảng 32 thời gian hữu tỉ greedy giảm mẫu 4000 nhánh reachable xuống một nhúm, ở khoảng 0.95 sống sót mỗi clause. Từ tỉ lệ đó, khoảng 555 clause sẽ dự phóng đưa không gian residue reachable 2^84 xuống dưới cap 2^42. Con số ~555 đó là DỰ PHÓNG THĂM DÒ, KHÔNG phải bound chứng nhận: nó chưa tính các biến residue mới mỗi denominator mới đưa vào, tương quan giữa các clause, cỡ SAT / decision-diagram, chi phí proof-certificate, hay việc giữ một bộ chung xuyên mọi modulus. Nên compounding là lợi ích chất lượng thật so với D24, nhưng phát biểu cỡ-chiến-dịch chưa chứng minh