어려운 문제가 발생하면 하나의 표준 접근 방식은 SAT 인스턴스로 표현하고 SAT 솔버를 실행하는 것입니다. 또 다른 표준 접근법은이를 제약 조건 만족 문제로 표현하고 CSP 솔버를 사용해보십시오. 이 두 가지는 어떤 종류의 문제가 자연스럽게 입력 형식으로 표현 될 수 있는지에 대해 모호하게 유사하다고 생각합니다.
주어진 문제에 대해 어떤 방법으로 좋은 결과를 얻을 수 있는지 인식하는 방법에 대한 지침이나 경험 규칙이 있습니까? CSP 솔버보다 SAT 솔버가 더 잘 처리 할 수있는 문제에 대해 어떤 사람이 제공 할 수있는 지침이 있습니까?
(분명히 두 가지 방법으로 해결할 수있는 몇 가지 쉬운 문제가 있습니다. 두 가지 방법으로 유용하게 해결할 수없는 몇 가지 어려운 문제도 있습니다. 두 가지 방법 모두 따로합시다. 지침이 가장 도움이되는 경우는 SAT 솔버가 CSP 솔버보다 성능이 우수하거나 CSP 솔버가 SAT 솔버보다 성능이 우수한 위치 SAT 솔버가 CSP 솔버보다 더 적합 할 가능성이 있거나 CSP 솔버가 더 적합 할 수있는 경우를 어떻게 알 수 있습니까? SAT 솔버-먼저 어떤 방법을 시도해야합니까?)
답변
나는 이것이 매우 좋은 질문이라고 생각합니다. SMT 솔버를 언제 사용해야합니까? 문제를 모델링하고 실제로 CSP / SAT / SMT 솔버를 실행하고 찾기 전에 결정하기가 어려울 수 있습니다. 다른 솔버조차도 동일한 인스턴스에서 매우 다르게 수행되는 것으로 잘 알려져 있습니다! 저의 직감은 잠재적으로 문제를 모델링하는 많은 방법이 있다는 사실에서 비롯됩니다. 또한 어떤 유형의 제약 조건이 사용되는지에 따라 검색 및 추론을 수행하는 많은 방법이 있습니다 (문제 형식이 다른 유형을 허용하는 경우).
8×8
9+9+9=27
32×32
스도쿠 퍼즐, SAT 솔버는 CSP 솔버보다 빠릅니다.
서로 다른 형식주의는 도메인 별 정보를 캡처하고 더 잘 다른 방식으로 활용합니다. 이에 대한 자세한 내용 은 여기에서 답변과 의견을 참조하십시오 .