SAT는 무엇이며 어떤 장점이 있습니까?

Question

최근에 SAT를 사용하여 퍼즐을 푸는 방법에 대한 Reddit 기사를 보았습니다 [1]. 이것은이 "SAT"에 대한 호기심을 불러 일으켰습니다. 위키 백과 기사를 읽었지만 좀 더 평범한 용어로 설명해달라고 부탁하고 싶습니다.

SAT 란 무엇이며 어떤 이점이 있습니까? 트리 구조를 횡단하는 데 사용할 수 있습니까? 텍스트 구문 분석을 위해? 줄 바꿈 [2]? 빈 포장 [3]? 일종의 최적화 기술인가요?

관련 메모에서 NP 대 P는 집합 합계의 어떤 숫자를 0으로 선택하는 것과 일부 숫자의 합이 0인지 확인하는 것에 관한 것이라고 읽었습니다. SAT는 이와 관련이 있습니까?

[1] http://www.reddit.com/r/ programming / comments / pxpzd / solving_hexiom_really_fast_with_a_sat_solver /

[2] http://en.wikipedia.org/wiki/Line_wrap

[3] http://en.wikipedia.org/wiki/Bin_packing_problem

Answer 1

SAT는 NP-Complete이기 때문에 매우 중요합니다. 이것이 의미하는 바를 이해하려면 Complexity 클래스에 대한 명확한 개념이 필요합니다. 다음은 간단한 요약입니다.

• P는 다항식 시간 (즉, 빠름)으로 풀 수있는 모든 문제의 클래스입니다.

• NP는 다항식 시간에 솔루션을 검증 할 수있는 모든 문제의 클래스입니다. 즉, 주어진 솔루션을 찾아내는 것이 빠르지 만 하나를 찾는 것이 일반적으로 느립니다 (대부분의 경우 지수 시간). 물론 문제가 NP의 P 부분에 있지 않는 한 (아래에서 지적했듯이 P는 쉽게 확인할 수 있으므로 NP의 일부입니다).

  그런 다음 NP-Complete 문제 세트가 있습니다. 이 세트에는 매우 일반적인 모든 문제가 포함되어 있으므로 NP의 다른 문제 대신 이러한 문제를 해결할 수 있습니다 (이를 다른 문제로 문제 줄이기라고 함). 즉, 한 도메인의 문제를 다른 NP-Complete 문제로 변환하고 답을 도출하고 답을 다시 변환 할 수 있습니다.

  그러나 문제가 NP-Complete라는 것이 증명 될 수 있지만 다른 주어진 문제에 대한 변환은 명확하지 않습니다.

  SAT는 NP-Complete이기 때문에 매우 좋습니다. 즉, NP의 다른 문제 대신 해결할 수 있으며 감소도 그렇게 어렵지 않습니다. TSP는 또 다른 NP-Complete 문제이지만 변환은 대개 훨씬 더 어렵습니다.

  예, SAT는 언급 한 모든 문제에 사용할 수 있습니다. 그러나 종종 이것은 실행 가능하지 않습니다. 가능한 곳은 언급 한 퍼즐과 같은 다른 빠른 알고리즘이 알려져 있지 않을 때입니다. 이 경우 퍼즐에 대한 알고리즘을 개발할 필요는 없지만 고도로 최적화 된 SAT-Solvers를 사용할 수 있으며 퍼즐에 대해 합리적이고 빠른 알고리즘을 얻을 수 있습니다.

  예를 들어 트리 구조를 탐색하는 것은 매우 간단하여 SAT에서 또는 SAT 로의 모든 변환은 단순히 탐색을 직접 작성하는 것보다 훨씬 더 복잡 할 것입니다.

Answer 2

긴 이야기를 간단히하기 위해 SAT 솔버는 부울 공식을 제공하는 것으로, 공식이 참인 다른 변수에 대한 값을 찾을 수 있는지 여부를 알려줍니다.

예

a, b 및 c가 부울 변수라고 가정하고, 이러한 변수에 (¬a ∨ b) ∧ (¬b ∨ c) 수식을 만드는 값을 할당 할 수 있는지 알고 싶습니다. 이 공식을 SAT 솔버로 보내면 true가 반환됩니다. SAT 솔버는 종종 유효한 할당을 제공합니다. 이 경우이 할당은 a: false, b:false, c:false 일 수 있습니다.

어떻게 사용할 수 있나요?

트리를 가로 지르거나 텍스트를 구문 분석하거나 줄을 끊는 데 사용하지 않습니다. 그러나 트리를 순회 할 때이를 사용하여 트리의 일부 제약 조건이 충족되는지 확인할 수 있습니다. 일부 전문 CSP 솔버가 이러한 종류의 문제에 대해 더 잘 수행 할 수 있지만 확실히 빈 패킹에 사용할 수 있습니다.

SAT 솔버는 특히 패키지 관리자와 같은 소프트웨어에서 요즘 훨씬 더 보편화되고 있습니다. Eclipse는 SAT4j를 내장하여 플러그인 간의 종속성을 관리합니다. SAT의 다른 응용 프로그램에는 일반적으로 모델 검사, 계획 응용 프로그램, 구성자, 스케줄링 등이 포함됩니다.