2 SAT의 솔루션 수 찾기

Question

알고리즘은 2 개의 적합성 문제에 대해 하나 이상의 솔루션이 존재하는지 여부를 알기를 원합니다. 이는 1000 개의 리터럴이 만족할 만하다고 가정합니다. 설명 해주십시오. Wikipedia 따르면

Answer 1

:.

Feder의 (1994)이 효율적으로 모든 용액을 나열하는 알고리즘 설명 주어진 2 satisfiability 인스턴스 과 관련된 여러 문제점을 해결하기위한 [14] 알고리즘은 또한 모든 솔루션을 나열 할 수있는 것보다 더 빠르게 솔루션의 수를 카운트하는 공지 [15] 이다 가능한 만큼 크게 다를 솔루션 쌍을 찾는. [16]

특히

Dahllöf, Vilhelm; 존슨, 피터; "2SAT 및 3SAT 공식에 대한 모델 계산" Wahlström, 매그너스 (2005), 이론 컴퓨터 과학 (332) (1-3) : 265-291, 도이 : 10.1016/j.tcs.2004.10.037; 총무, Martin; 정보 및 관리, 알고리즘 측면 Kasiviswanathan, 시바 프라 사드 (2007), "2-SAT 솔루션과 응용 프로그램과 색소를 계산하기위한 알고리즘은"컴퓨터 과학, 4508 년 노트 강의, 출판사 (Springer-Verlag), PP. 47 -57, doi : 10.1007/978-3-540-72870-2.

원하는 것으로 보입니다.

---

다음은이 주제에 대한 졸업 증서입니다. 꽤 길기 때문에 다음과 같이 따라야합니다. http://people.inf.ethz.ch/arazen/publications/2sat.pdf

그리고 다른 하나는 의사 코드 : http://www.engineeringletters.com/issues_v15/issue_2/EL_15_2_12.pdf을 포함합니다.

하지만이 문제는 중요하지 않은 수학적 문제이므로이 경우 수학으로 생활해야합니다.

Answer 2

나는이 문구와 문제의 제목에 대해 다소 혼란 스럽다.

"둘 이상의 솔루션이 있는지 여부를 확인하는"것이 실제로 필요한 유일한 솔루션 인 경우 모든 솔루션을 나열하는 것이 과잉입니다. 첫 번째 해결책을 찾고 "A AND NOT B"라고 말하면서 SAT 해결자가 그 해결책에서 벗어나는 '차단 조항'을 추가하십시오.

언급 된 예에서 그러한 제약 조건은 "NOT (A AND NOT B)"입니다. CNF에 가져 가서 행복하게 :-)

Answer 3

OP는 하나 이상의 해결 방법이 있는지 알고 싶어합니다. 첫 번째 2SAT가 훨씬 쉽습니다. 직접 레이블이 지정된 그래프를 만듭니다. 각 노드는 리터럴 (변수 또는 부정)에 해당하며, a 또는 b 형식의 모든 절은 (a가 아닌) b와 (b)가 아닌 a. a에서 a (a가 아님)에 대한 경로가없는 경우에만 만족스러운 할당이 있습니다.실제로 Aspvall, Plass 및 Tarjan (참조 용 http://en.wikipedia.org/wiki/Strongly_connected_component 참조)로 인해 이것을 판별하는 선형 시간 알고리즘이 있습니다. 그래프가이 테스트를 통과하면 그래프에서 소스 노드를 선택하고 모든 의미 (모든 경로)를 찾아 솔루션을 얻습니다. 그들 중 일부는 다른 노드를 사라지게 만들 것입니다 (노드가 a 인 경우 리터럴을 true로 만드는 것에 해당하므로 노드 (a가 아님)가 제거됩니다. 원본 노드가 없어 질 때까지이 작업을 계속하십시오. 다른 솔루션이있는 경우 방금 발견 한 솔루션에 리터럴 중 하나가 있어야하며 부정됩니다. 그러니 차례대로 시도해보십시오. 이것은 2 차 알고리즘을 제공합니다. 나는 거기에 아마 더 좋은 것이 있다고 생각할 것입니다.

Answer 4

2-SAT 솔루션의 계산은 다항식 솔루션보다 훨씬 어려울 수 있으므로 어려운 문제입니다 (NP 완료 일 수도 있음). 그래서 다항식 시간에 우리는 모든 해를 열거 할 수 없습니다. 혼자서 빠른 알고리즘을 찾을 수 없으므로 지금 네트워크를보고 있습니다. 그러나 알고리즘이 빠르면 다항식 시간에 RSA를 깨뜨릴 수 있습니다.