Chắc chắn có cách để sử dụng trình giải SAT mà bạn đã mô tả để tìm tất cả các giải pháp của bài toán SAT, mặc dù nó có thể không phải là cách hiệu quả nhất.
Chỉ cần sử dụng bộ giải để tìm giải pháp cho vấn đề ban đầu của bạn, thêm mệnh đề không làm gì ngoại trừ loại trừ giải pháp bạn vừa tìm thấy, sử dụng bộ giải để tìm giải pháp cho vấn đề mới, v.v. Tiếp tục cho đến khi bạn gặp sự cố không thỏa mãn.
Ví dụ: giả sử bạn muốn thỏa mãn (X or Y) and (X or Z). Có năm các giải pháp:
Bốn với X đúng, Y và Z tùy ý.
Một với X sai, Y và Z đúng.
Vì vậy, bạn chạy trình giải quyết của mình và giả sử nó cung cấp cho bạn giải pháp (X, Y, Z) = (T, F, F). Bạn có thể loại trừ giải pháp này --- và chỉ giải pháp này --- với các hạn chế
not (X and (not Y) and (not Z))
hạn chế này có thể được viết lại như mệnh đề
(not X) or Y or Z
Vì vậy, bây giờ bạn có thể chạy giải của bạn trên vấn đề mới
(X or Y) and (X or Z) and ((not X) or Y or Z)
v.v.
Như tôi đã nói, đây là cách để làm những gì bạn muốn, nhưng nó có lẽ không phải là cách hiệu quả nhất. Khi người giải quyết SAT của bạn đang tìm kiếm một giải pháp, nó học rất nhiều về vấn đề, nhưng nó không trả lại tất cả thông tin đó cho bạn --- nó chỉ cung cấp cho bạn giải pháp mà nó tìm thấy. Khi bạn chạy trình giải quyết một lần nữa, nó phải tìm hiểu lại tất cả các thông tin đã bị vứt đi.
thể người downvoted xin giải thích lý do tại sao? Sau khi đọc mục nhập blog này (http://blog.stackoverflow.com/2011/07/its-ok-to-ask-and-answer-your-own-questions/), tôi nghĩ những gì tôi đã làm ở đây là "không chỉ đơn thuần là OK, "nhưng" được khuyến khích một cách rõ ràng. " – Vectornaut
Hoàn toàn ổn. Câu trả lời hay, btw. –