Giới hạn của lý luận trong số học định lượng trong SMT là gì?

Question

Tôi đã thử một vài giải quyết SMT (CVC3, CVC4 và Z3) trên điểm chuẩn dường như tầm thường như sau:

(set-logic LIA) 
(set-info :smt-lib-version 2.0) 
(assert (forall ((x Int)) (forall ((y Int)) (= y x)))) 
(check-sat) 
(exit) 

Các giải quyết tất cả trở lại chưa biết. Tôi hiểu rằng đây là một đoạn không thể giải quyết được (cũng không tuyến tính) nhưng tôi đã mong đợi sẽ có một số phỏng đoán tức thời đơn giản có thể giải quyết nó. Tôi cũng đã thử thêm một số xác nhận bổ sung với các hằng số nhưng nó không giúp ích gì.

Có cách nào để tấn công những vấn đề này và giới hạn của lý luận trong số học định lượng trong SMT?

Answer 1

Ví dụ của bạn thuộc danh mục Số học tuyến tính (LIA).

LIA tức là Presburger Arithmetic thừa nhận việc loại bỏ định lượng (qe) mặc dù độ phức tạp của quy trình qe rất cao.

Tôi không chắc chắn rằng loại bỏ CVC3 và CVC4 hỗ trợ lượng hóa cho LIA, nhưng trong Z3 bạn có thể làm

(set-logic LIA) 
(set-info :smt-lib-version 2.0) 
(assert (forall ((x Int)) (forall ((y Int)) (= y x)))) 
(check-sat-using (then qe smt)) 

Từ Rise4Fun execution, tôi đã có unsat kết quả.

Ở đây chiến thuật qe là bước tiền xử lý trước khi áp dụng chiến thuật kết thúc smt.

Answer 2

Pad chính xác, bộ xử lý trước qe có thể khá tốn kém. Hơn nữa, nó không hiệu quả trong các công thức đến từ các công cụ xác minh phần mềm như VCC, Poirot, Dafny, VeriFast, Why3 và ESCJava2. Nó không hiệu quả vì các công thức do các ứng dụng này tạo ra cũng chứa các hàm không được giải thích, mảng, v.v.

Như câu trả lời của Pad cho thấy, Z3 là tập hợp các công cụ. Nó cung cấp các API và các lệnh cho phép người dùng lựa chọn động cơ nào (hoặc kết hợp các công cụ) sẽ được sử dụng để giải quyết vấn đề. Khi người dùng chỉ nói (check-sat) là cố gắng đoán công cụ tốt nhất để giải quyết công thức nhập liệu là gì. Việc đoán dựa trên cấu trúc của công thức nhập liệu và chú thích do người dùng cung cấp (ví dụ: lệnh set-logic). Chúng tôi liên tục mở rộng bộ mảnh vỡ được tự động phát hiện và bộ công cụ chúng tôi cung cấp.

Điều đó đang được nói, thật lúng túng khi Z3 bỏ lỡ một đoạn như LIA và không tự động áp dụng thủ tục qe cho nó. Đối với công thức LIA, qe thường là tùy chọn tốt nhất. Các giải pháp thay thế dựa trên kết hợp E hoặc MBQI không hiệu quả vì chúng có nghĩa là cho các mảnh hoàn toàn khác nhau.

Tôi chỉ committed code phát hiện LIA (ngay cả khi không sử dụng set-logic). Thay đổi đã có sẵn trong chi nhánh unstable (đang hoạt động). Nó sẽ có vào ngày mai trong các bản dựng hàng đêm và trong bản phát hành chính thức tiếp theo.