Chính xác những gì các số lượng là SMT hoàn thành?

Question

Tôi đã xem xét các giải pháp SMT khác nhau, chủ yếu là Z3, CVC4 và VeriT. Tất cả đều có những mô tả mơ hồ về khả năng của họ để giải quyết các vấn đề SMT với số lượng. Tài liệu của họ chủ yếu dựa trên ví dụ (Z3), hoặc bao gồm các tài liệu học thuật, mô tả các thay đổi có thể có hoặc có thể không thực sự được thực hiện.

Tôi biết rằng có rất nhiều mảnh vỡ decidable logic đầu tiên đặt hàng, chẳng hạn như:

• quantifiers hữu hạn-giáp
• monadic bậc nhất Logic

Những gì tôi muốn biết là, mà (nếu có) các lớp học của FOL là những người giải quyết SMT khác nhau đảm bảo được hoàn thành? Làm thế nào tôi có thể biết được liệu vấn đề tôi đang xem có nằm trong những mảnh vỡ mà họ hoàn thành không?

Answer 1

Có hai loại công thức được định lượng mà CVC4 hoàn tất.

(1) Công thức được định lượng với các miền hữu hạn.

CVC4 là mô hình hữu hạn hoàn thành trên các định lượng trên các loại chưa giải thích, có nghĩa là nếu có một mô hình mà tất cả các loại không giải thích được hiểu là hữu hạn thì CVC4 cuối cùng sẽ tìm thấy nó. Để biết chi tiết, bạn có thể nhìn thấy bài viết này:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
đó tóm tắt các báo cáo hội thảo ở đây:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Chú ý rằng những kỹ thuật này kết hợp với bất kỳ lý thuyết được hỗ trợ bởi CVC4. Miễn là lý thuyết này là đáng tin cậy và việc định lượng không liên quan đến các loại được giải thích (vô hạn), thì sự đảm bảo về mô hình hữu hạn-đầy đủ vẫn còn.

Cách tiếp cận cũng được hoàn thành cho các đoạn nhất định, chẳng hạn như đoạn Bernays-Schoenfinkel-Ramsey (EPR), có nghĩa là đối với bất kỳ vấn đề nào không thỏa mãn trong đoạn này, CVC4 cuối cùng sẽ trả lời "unsat".

Nếu bạn quan tâm đến tính năng này, CVC4 sẽ không theo mặc định sử dụng tìm kiếm mô hình hữu hạn trên một vấn đề đầu vào. Tùy chọn dòng lệnh "--finite-model-find" sẽ bật các kỹ thuật này.

(2) Công thức định lượng trong một số lý thuyết phát ra loại bỏ định lượng.

Ví dụ: CVC4 được hoàn thành cho số học tuyến tính được định lượng (thuần). Để biết chi tiết bạn có thể nhìn thấy bài viết này:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
mà xây dựng dựa trên một giấy hội nghị trước đó:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf

Đây là tinh thần tương tự cách tiếp cận khác, ví dụ trong Z3:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf

Answer 2

Tại nguy cơ vô ích không trả lời câu hỏi, có những lý do tại sao tài liệu này khó tìm.

Liên kết giữa khả năng quyết định và "thực sự có thể giải quyết vấn đề cụ thể của tôi trong một khoảng thời gian tôi sẵn sàng chờ" không phải là điều mạnh mẽ. Ví dụ thường xuyên, tập hợp các điểm chuẩn và kết quả thử nghiệm là một chỉ báo tốt hơn (và do đó được trình bày).

Ngoài ra, hầu hết người giải quyết đều thực hiện một số thao tác viết lại và xử lý sự cố trước khi cố giải quyết. Vì vậy, cách cổ điển, cách diễn đạt các đoạn decideable không phải lúc nào cũng áp dụng được vì các vấn đề khác có thể được viết lại thành các phần có thể phân tách được (hy vọng không phải là cách khác nhưng tôi không thể hứa là nó sẽ không bao giờ xảy ra!).

Cuối cùng, nhiều người giải quyết sử dụng các quy trình bán quyết định heuristic hoạt động tốt nhưng khó mô tả trong một cái gì đó trang trọng hơn mã. Vì vậy, có những thứ có thể không xuất hiện trong bất kỳ mảnh vỡ được biết đến nào, nhưng có thể tìm thấy câu trả lời nào.