SAT 학습 자료 (부울 만족 성 문제)

SAT (부울 충족 성 문제) 해결 자에서 읽을 수있는 좋은 문서는 무엇입니까? Google을 통해 좋은 자료를 찾을 수 없었습니다. 내가 찾은 문서는 조감도, 너무 진보되거나 손상된 PDF 파일 중 하나였습니다 ...SAT 학습 자료 (부울 만족 성 문제)

실용적인 SAT 해결사의 알고리즘에 대해 알아 보려면 어떤 논문/문서를 권하고 있습니까?

출처

2010-03-27 Jules

"SAT 질문 풀기"의 의미에 대해 자세히 설명해 주시겠습니까? SAT 문제는 응시자가 창의적인 문제 해결 기술을 필요로하도록 특별히 고안되었습니다. 컴퓨터에는이 기능이 없습니다. –

코리 (Cory)는 SAT (미국에서 널리 사용되는 대학 입학 시험 중 한 세트)에 대한 질문이 아니라 불리언 논리 (http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 참조)에서 만족도 문제를 의미합니다. –

예, 죄송합니다. Doug McClean이 맞습니다. 제 질문은 부울 만족 해결 자에 관한 것입니다. – Jules

Davis-Putnam-Logemann-Loveland page on Wikipedia에는 좋은 개요가 있습니다.

미니 종이 인 "An Extensible SAT-solver"을 따라갈 수 있어야합니다.

minisat에서 사용되는 충돌 중심 학습 알고리즘을 이해하려면 "GRASP - A New Search Algorithm for Satisfiability"도 읽어야합니다.

나는 이러한 자원을 사용하여 Python으로 SAT 솔버를 매우 쉽게 작성할 수있었습니다. 내 sat.py 코드를 사용할 수 있습니다 (현재 LGPL 2.1). 그러나 최근에는 버그가있을 수 있습니다. 미니 디자인에서 몇 가지 최적화가 부족합니다. 원시 속도를 원하면 minisat 코드를 사용하십시오.

업데이트 : 또한 유형을 쉽게 볼 수있는 OCaml 버전 sat.ml을 만들었습니다.

출처

2010-03-28 10:46:03

감사합니다. PDF 리더는 minisat 웹 사이트에서 파일을 열 수 없으므로이 파일들을 포기했습니다. 하지만 당신이 제안한 이후로 나는 당신이 * 열 수 있다고 가정합니다. 그리고 실제로 Google의 온라인 pdf 뷰어를 열어 볼 때 그들은 일을합니다! 감사. 파이썬 SAT 솔버의 코드를 사용할 수 있습니까? – Jules

좋은 아이디어 - 내 코드에 대한 링크를 추가했습니다. PDF는 나를 위해 잘 열렸습니다 (Evince : http://projects.gnome.org/evince/). –

좋은 책은 : Uwe Schöning; Jacobo Torán - 만족도 문제

출처

2015-06-24 17:37:04 noctua

SAT 학습 자료 (부울 만족 성 문제)

답변

관련 문제