I believe that such things are done regularly in logical programming constraints . Unfortunately, I'm not experienced enough to provide more accurate data, but this should be a good starting point.
The general principle is simple: an unbound variable can have any value; since you test it for inequalities, the set of possible values โโis limited to one or more intervals. When / if these intervals converge to a single point, this variable is tied to this value. If, OTOH, any of these inequalities is considered unsolvable for each value in the intervals, a logic [programming] error occurs.
See also this , for example, how it is done in practice using swi-prolog. We hope you find links or links to the main algorithms so that you can play them on your platform of choice (perhaps even when searching for ready-made libraries).
Update: I tried to reproduce your example using swi-prolog and clpfd, but did not get the expected results, only close ones. Here is my code:
?- [library(clpfd)]. simplify(A,B,C,D) :- A
And my results, with backtracking (line breaks inserted for readability):
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 ?-
So, the program gave 8 results, among those you were interested in (5th and 8th):
A = 1, B in inf.. -1\/1..sup, C in 38..sup ; A = 1, D = 6, B in inf.. -1\/1..sup.
Others were redundant and could possibly be eliminated using simple, automated logic rules:
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]
I know this is a long way to go for a common solution, but as I said, I hope this is the beginning ...
PS I used "regular" AND and OR ( ,
and ;
) because clpfd ( #/\
and #\/
) gave a very strange result that I couldnโt understand myself ... maybe someone more experienced might throw a little light on it ...