Wann ist SAT vs. Constraint Satisfaction anzuwenden?

Wenn ich ein schweres Problem habe, besteht ein Standardansatz darin, es als SAT-Instanz auszudrücken und einen SAT-Solver darauf auszuführen. Ein weiterer Standardansatz besteht darin, es als Problem der Einschränkungszufriedenheit auszudrücken und einen CSP-Löser zu verwenden. Die beiden fühlen sich irgendwie vage ähnlich, was Arten von Problemen angeht, die sich natürlich in ihrem Eingabeformat ausdrücken lassen.

Gibt es Richtlinien oder Faustregeln, um für ein bestimmtes Problem zu erkennen, welche Vorgehensweise mit größerer Wahrscheinlichkeit zu guten Ergebnissen führt? Gibt es eine Anleitung, die jemand anbieten kann, um welche Probleme es sich bei SAT-Lösern besser handelt als bei CSP-Lösern oder umgekehrt?

(Offensichtlich gibt es einige einfache Probleme, die mit beiden Ansätzen gelöst werden können. Es gibt auch einige schwierige Probleme, die mit beiden Ansätzen nicht sinnvoll gelöst werden können. Lassen Sie uns diese beiseite legen. Der Fall, in dem die Anleitung am hilfreichsten ist, sind Probleme mit beiden SAT Solver erzielen eine bessere Leistung als CSP-Solver oder CSP-Solver erzielen eine bessere Leistung als SAT-Solver. Woran erkenne ich, dass ein SAT-Solver wahrscheinlich besser passt als ein CSP-Solver oder ein CSP-Solver besser passt als ein SAT-Löser - dh welcher Ansatz zuerst zu versuchen?)

Ich denke das ist eine sehr gute Frage. Sie könnten auch fragen, wann Sie einen SMT-Solver verwenden sollen. Ich habe das Gefühl, dass es schwierig sein könnte, es zu bestimmen, bevor das Problem modelliert und die CSP / SAT / SMT-Löser ausgeführt und herausgefunden werden. Es ist allgemein bekannt, dass sogar verschiedene Löser in denselben Instanzen sehr unterschiedlich arbeiten! Meine Intuition kommt auch von der Tatsache, dass es möglicherweise viele Möglichkeiten gibt, ein Problem zu modellieren. Darüber hinaus gibt es viele Möglichkeiten zum Suchen und Schliessen, je nachdem, welche Art von Einschränkungen verwendet wird (wenn der fragliche Formalismus verschiedene Arten zulässt).

$8 \times 8$$9+9+9=27$$32 \times 32$ Sudoku-Rätsel, SAT-Löser wären schneller als CSP-Löser.

Verschiedene Formalismen sind in der Lage, domänenspezifische Informationen zu erfassen und besser und auf unterschiedliche Weise zu nutzen. Weitere Informationen finden Sie in der Antwort und den Kommentaren hier .