Jeśli mam trudny problem, jednym ze standardowych sposobów jest wyrażenie go jako instancji SAT i próby uruchomienia na nim solvera SAT. Innym standardowym podejściem jest wyrażenie go jako problemu satysfakcji z ograniczeń i próba użycia solvera CSP. Obaj czują się nieco niejasno pod względem tego, jakie problemy można naturalnie wyrazić w ich formacie wejściowym.
Czy istnieją jakieś praktyczne wskazówki dotyczące rozpoznawania danego problemu, które podejście może przynieść dobre wyniki? Czy istnieją jakieś wskazówki dotyczące tego, jakie rodzaje problemów można lepiej rozwiązać w rozwiązaniach SAT niż w rozwiązaniach CSP lub odwrotnie?
(Oczywiście, istnieje kilka łatwych problemów, które można rozwiązać za pomocą obu podejść. Są też pewne trudne problemy, których nie można skutecznie rozwiązać za pomocą obu podejść. Odłóżmy je na bok. Przypadek, w którym wskazówki są najbardziej pomocne, to problemy, w których SAT solwery działają lepiej niż solwery CSP lub tam, gdzie solwery CSP działają lepiej niż solwery SAT Jak rozpoznać, kiedy solver SAT może lepiej pasować niż solver CSP lub kiedy solver CSP prawdopodobnie będzie lepiej pasował niż solver SAT - czyli jakie podejście spróbować najpierw?)
Odpowiedzi:
Myślę, że to bardzo dobre pytanie. Możesz również zapytać: kiedy używać solvera SMT? Mam wrażenie, że ustalenie problemu przed modelowaniem problemu i uruchomieniem solverów CSP / SAT / SMT może być trudne. Powszechnie wiadomo, że nawet różne solwery działają bardzo różnie w tych samych instancjach! Moja intuicja wynika również z faktu, że istnieje potencjalnie wiele sposobów modelowania problemu. Ponadto istnieje wiele sposobów wyszukiwania i wnioskowania, w zależności od rodzaju zastosowanych ograniczeń (jeśli dany formalizm dopuszcza różne typy).
Różne formalizmy są w stanie uchwycić informacje specyficzne dla domeny i wykorzystać je lepiej i na różne sposoby. Aby uzyskać więcej informacji na ten temat, zobacz odpowiedź i komentarze tutaj .
źródło