Giải quyết SAT với hơn 2^32 điều khoản

Question

Tôi đang cố gắng giải quyết một công thức CN CNF sử dụng số SAT solver. Công thức (ở định dạng DIMACS) có 4,697,898,048 = 2^32 + 402,930,752 khoản, và tất cả những người giải quyết SAT tôi có thể tìm được gặp rắc rối với nó:

• (P)lingeling báo cáo rằng có "quá nhiều điều khoản" (tức là nhiều mệnh đề so với dòng tiêu đề quy định cụ thể, nhưng đây không phải là trường hợp)
• CryptoMiniSat4 & picosat tuyên bố để đọc dòng tiêu đề như nói 402.930.752 khoản mà là 2^32 quá ít
• Glucose dường như để phân tích 98.916.961 khoản và sau đó reports to have solved the formula as UNSAT sử dụng đơn giản, nhưng t của anh ta là không đúng (một phân đoạn ban đầu của công thức này ngắn rất có thể là SAT).

Có ai biết về một người giải quyết SAT có thể xử lý các file này lớn? Hoặc là có một cái gì đó giống như một công cụ chuyển đổi trình biên dịch có thể bỏ qua loại hành vi này? Tôi tin rằng tất cả các giải pháp được biên soạn cho 64bit linux. (Tôi hơi noob khi nói đến việc xử lý những con số lớn này, xin lỗi.)

Answer 1

Tôi là nhà phát triển của CryptoMiniSat. Trong hầu hết các trường hợp CNF là rất lớn, vấn đề không phải là giải quyết SAT nhưng việc dịch bản gốc của vấn đề thành CNF đã không được thực hiện một cách cẩn thận đủ. Tôi cho rằng bạn đã không viết CNF đó bằng tay - bạn có một vấn đề mà bạn đã dịch sang CNF bằng cách sử dụng một công cụ tự động.

Hành động dịch một vấn đề sang CNF được gọi là mã hóa và nó có một tài liệu lớn trong học viện. Đó là một chủ đề toàn bộ cho chính nó, hoặc một cách thích hợp hơn, toàn bộ chủ đề cho chính họ. Vui lòng xem các tài liệu nghiên cứu về lập trình ràng buộc (CP), ràng buộc giả boolean (PB), kỹ thuật dịch ANF-to-CNF (xem hội thảo/hội thảo crypo) và mã hóa mạch điện tử (tìm kiếm mã hóa AIG, Tseitin và các biến thể của nó) tại các tài liệu tham khảo). Đây là những chủ đề lớn nhưng có nhiều chủ đề khác. Nhìn vào những điều này sẽ làm giảm CNF của bạn ít nhất 3 đơn đặt hàng của cường độ, có lẽ nhiều hơn nữa.