nie jestem w tej kwestii zbytnim specem, ale solvery/testery często "sprowadza się" do iteracyjnego:
- wzięcia kolejnego wyrażenia podanego jako warunek/ograniczenie
- upraszczania pozostalych zdan/wyrażen wobec wiedzy w nim zawartej
- proby uzupełniania faktów na podstawie zmienionej bazy faktow i ograniczen (np. a<b i b<e, wiec fakt pochodny to a<e)
- ew. proby znalezienia przykladu lub kontr-przykladu na danym etapie
de facto, kazdy z tych kroczkow stanowi niezly problem sam w sobie, silnie zalezny od charakteru i typu zdan..
IMHO, na poczatek zainteresuj się programami/jezykami takimi jak Prolog czy Z3 - razem z nimi bardzo czesto przychodza artykuly, a nawet ksiażki, opisujące jak za tego typu problemu zabrać. Prolog moze wygladac prosto, ale pokaze, jak manioulujac postacia wyrazen logicznych mozesz w "szybki" sposob oceniac czy ze soba nie kolidują.
Niestety, w zaleznosci od DOKŁADNEGO opisu problemu, Twoj sposob rozwiazywania drastycznie się zmienia. Np. majac problem - to:
A) zestaw zdań logiki Boole'a z małą liczba zmiennych - mozesz "pojechac" bruteforce'm i sprawdzic wszytkie kombinacje przypisan true-false do zmiennych
B) dużą liczbą zmiennych - masz bardzo duzy NP-trudny problem, idz do publikacji zwiazanych z "checking for logic/boolean satisfiability", bo wyników nieoptymalizowanego algorytmu sprawdzacza mozesz banalnie po prostu nie dożyć
C) zestaw ograniczen a < b, c >= d itp, gdzie a/b/c/d to liczby i zmienne lub proste wyrazenia liniowe - problem rozwiazuje sie budujac i obcinajac "wielokaty wypukle", w impementacji sprowadza sie to do 1 tabelki i kilku petel
D) zestaw ograniczen a < b, c >= d itp, gdzie a/b/c/d to wyrazenia matematyczne "dowolnej" postaci - masz spory problem, poniewaz analiza funkcji nie jest prosta - po to sa kombajny w stylu mathcad czy mathematica. Jezeli znasz pewne "gwarantowane" cechy wyrazen (monotoniczne? wielomianowe? itp...), mozna to wykorzystac do znaczengo przyspieszenia/uproszczenia wstepnego zagadnienia ale i tak nie jest latwo, a dochodzi jeszcez do tego problem, czy Twoj checker ma byc "matematyczny" cyz "programistyczny".. tzn. czy ma operowac na liczbach rzeczywistych, czy "dziurawych" n-bitowych skonczonych reprezentacjach.. po przeanalizowaniu funkcji wspolnie lub osobno, stajesz przed problemem podobnym do (C), ale masz juz niekoniecznie wypukłe wielokąty, co jest bardziej trudne/czasochlonne
E) czy odpowiedz ma byc absolutna, czy z okreslonym % prawdopodobienstwa błędu? - jesli to drugie, mozesz monte-carlo'wac, co niby upraszcza, ale wprowadza Cie w problem pokrycia przestrzeni i "dobrego rozkladu" strzałów..
F) ..
...
mam nadzieje ze rozumiesz rozdzwięk pomiędzy klasami problemow które się pojawiają.. rodzaj logiki która rządzi zdaniami które dostarczasz, ma niemniejszy wpływ na konstrukcję rozwiązania niż takie "detale" jak wyżej. jezeli chcesz, aby ktos sensownie cokolwiek Ci powiedział, musisz scisle okreslic, co masz do analizy, podrzucic wszystkie ograniczenia ulatwiajace/utrudniajace jakie znasz w ramach "rzeczy do analizy", oraz jakiego wyniku masz w odpowiedzi dostarczyc.
sformułowania "zdanie logiczne", "zmienna losowa", "opis wnioskowania", czy "każda możliwość wczytywanej zmiennej" to znacząco za mało, aby w ogóle zgadnąć przed jakiej klasy problemem się stawiasz, chocby dlatego, że do "zdan logicznych" na upartego zaliczysz także "F jest jednoargumentowe => calka z F(x) ma być większa od e^x", a w kontekscie pisania solvera dla pakietu takich zdan erm.. "życzę powodzenia" i szczesliwego zakonczenia habilitacji/profesury :)