Kiedy stosować SAT vs Constraint Satisfaction?

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?)

heuristics sat-solvers constraint-programming

— DW
źródło

Pamiętaj, że problem nie może być zbyt trudny, jeśli chcesz zredukować do SAT.

— Raphael

Albo dlaczego skupić się tylko na SAT / CSP, a co z SMT?

— Juho

Korzystanie z narzędzia do rozwiązywania ograniczeń ma tę zaletę, że można łatwo wypróbować niektóre optymalizacje (np. Techniki łamania symetrii) w instancjach, które nie są zbyt trudne (i sprawdzić skuteczność takich optymalizacji). Ponadto wiele z nich może wyprowadzać standardowy plik CNF jako wynik pośredni.

— Vor

Świetna uwaga, @Juho! Warto również rozważyć SMT - jeśli masz jakieś przemyślenia, możesz porównać wszystkie trzy (SAT, CSP, SMT).

— DW

Miałem to samo pytanie, dziękuję za pytanie.

— xxx ---

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).

$8 \times 8$ $9+9+9=27$ $32 \times 32$ Sudoku, solwery SAT byłyby szybsze niż solwery CSP.

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 .

— Juho
źródło