Tôi tin rằng những điều này được thực hiện thường xuyên trong constraint logic programming. Đáng tiếc là tôi không đủ kinh nghiệm để cung cấp chi tiết chính xác hơn, nhưng đó phải là điểm khởi đầu tốt.
Nguyên tắc chung rất đơn giản: biến không liên kết có thể có bất kỳ giá trị nào; khi bạn kiểm tra nó so với sự bất bình đẳng, tập hợp các giá trị có thể bị hạn chế bởi một hoặc nhiều khoảng thời gian. Khi/nếu những khoảng thời gian đó hội tụ với một điểm duy nhất, biến đó sẽ bị ràng buộc với giá trị đó. Nếu, OTOH, bất kỳ sự bất bình đẳng nào được coi là không thể giải quyết được cho mọi giá trị trong khoảng thời gian, lỗi logic [lập trình] xảy ra.
Xem thêm this, để biết ví dụ về cách thực hiện điều này trong thực tế sử dụng swi-prolog. Hy vọng rằng bạn sẽ tìm thấy các liên kết hoặc tham chiếu đến các thuật toán cơ bản, vì vậy bạn có thể tái tạo chúng trong nền tảng lựa chọn của bạn (thậm chí có thể tìm các thư viện sẵn sàng).
Cập nhật: Tôi đã cố tạo lại ví dụ của bạn bằng swi-prolog và clpfd, nhưng không nhận được kết quả mà tôi mong đợi, chỉ những kết quả gần đúng. Dưới đây là mã của tôi:
?- [library(clpfd)].
simplify(A,B,C,D) :-
A #= 1 ,
(B #= 1 ; B #\= 0) ,
(C#>= 35 ; D #\= 5) ,
(C#>= 38 ; D #= 6).
Và kết quả của tôi, trên backtracking (ngắt dòng chèn vào cho dễ đọc):
10 ?- simplify(A,B,C,D).
A = 1,
B = 1,
C in 38..sup ;
A = 1,
B = 1,
D = 6,
C in 35..sup ;
A = 1,
B = 1,
C in 38..sup,
D in inf..4\/6..sup ;
A = 1,
B = 1,
D = 6 ;
A = 1,
B in inf.. -1\/1..sup,
C in 38..sup ;
A = 1,
D = 6,
B in inf.. -1\/1..sup,
C in 35..sup ;
A = 1,
B in inf.. -1\/1..sup,
C in 38..sup,
D in inf..4\/6..sup ;
A = 1,
D = 6,
B in inf.. -1\/1..sup.
11 ?-
Vì vậy, chương trình mang lại 8 kết quả, trong số những người 2 bạn đã quan tâm trên (5th và thứ 8):
A = 1,
B in inf.. -1\/1..sup,
C in 38..sup ;
A = 1,
D = 6,
B in inf.. -1\/1..sup.
Các khác là không cần thiết, và có thể có thể được loại bỏ sử dụng đơn giản, các quy tắc logic automatable:
1st or 5th ==> 5th [B == 1 or B != 0 --> B != 0]
2nd or 4th ==> 4th [C >= 35 or True --> True ]
3rd or 1st ==> 1st ==> 5th [D != 5 or True --> True ]
4th or 8th ==> 8th [B == 1 or B != 0 --> B != 0]
6th or 8th ==> 8th [C >= 35 or True --> True ]
7th or 3rd ==> 3rd ==> 5th [B == 1 or B != 0 --> B != 0]
Tôi biết đó là một chặng đường dài phía sau là một giải pháp chung, nhưng như tôi đã nói, hy vọng đó là một sự khởi đầu ...
T.B. Tôi đã sử dụng "thông thường" VÀ và HOẶC (, và ;) vì những thứ của clpfd (#/\ và #\/) đã cho kết quả rất lạ mà tôi không thể hiểu bản thân ... có thể ai đó có kinh nghiệm hơn có thể truyền một số ánh sáng lên đó ...
Có giới hạn cho việc giảm bao nhiêu có thể được thực hiện trong thời gian đa thức. Ví dụ: nếu bạn luôn có thể giảm bất kỳ biểu thức biểu mẫu bình thường liên kết nào thành dạng đơn giản nhất của nó, bạn sẽ giải quyết được vấn đề 3SAT mở. – mbeckish
@mbeckish: Điều đó nghe có vẻ đáng sợ với tôi. Trên thực tế, tôi không biết về những điều này cho đến khi bạn folks hướng tôi đi đúng hướng. Tôi đã suy nghĩ không chỉ 3SAT, mà còn là vấn đề nSAT. Bây giờ, tất cả đều không thể. –
Đừng ngại giải quyết các vấn đề NP-hard. Đối với hầu hết trong số họ, phần cứng sẽ nằm trong một khu vực tương đối nhỏ của không gian vấn đề, trong giai đoạn chuyển tiếp giữa các vấn đề dễ xảy ra và dễ xảy ra. Nếu giải quyết vấn đề NP-hard luôn luôn là không thể, tôi sẽ không thể làm được. Nó phụ thuộc nhiều vào cách bạn mong đợi thuật toán của bạn để mở rộng quy mô. – twinterer