샤프-SAT

이 글은 검증을 위해 인용구가 추가로 필요하다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "Sharp-SAT" – 뉴스 · 신문 · 책 · 학자 · JSTOR (1919년 6월) (이 템플릿 메시지 제거 방법과 시기 학습)

컴퓨터 과학에서 샤프 만족도 문제(Sharp-SAT 또는 #SAT라고도 함)는 발레안트가 1979년에 도입한 주어진 부울포뮬라를 만족시키는 해석의 수를 세는 문제다.^[1]즉, 주어진 부울 공식의 변수를 TRUE 또는 FALSE 값으로 일관성 있게 대체하여 공식이 TRUE로 평가될 수 있는 방법에는 얼마나 많은 방법이 있는지 묻는다.예를 들어, ${\displaystyle \mathrm{∆}}$ ${\displaystyle b}$ ${\displaystyle a\lor \neg b}$ $공식$은 변수의 세 가지 고유한$$부울 값 할당, 즉 ${\displaystyle }$({\$displaystyle$ $a$$}$ $$= TRUE, b ${\displaystyle b}$ $$= FALSE)$$$$으로 충족된다$$.
(${\displaystyle }$ ${\displaystyle a}$ $$= $TRUE{\displaystyle }$, b ${\displaystyle b}$ $$= TRUE) ${\displaystyle \mathrm{\vee }}$ ${\displaystyle b}$ ${\displaystyle a\lor \neg$b}$$ = TRUE가 $있다{\displaystyle }$.

#SAT는 부울식 해법이 존재하는지 묻는 부울만족도 문제(SAT)와는 다르다.대신, #SAT는 부울 공식에 대한 모든 해결책을 열거하도록 요청한다.#SAT는 부울 공식에 대한 총 솔루션 개수가 알려지면 일정한 시간에 SAT를 결정할 수 있다는 점에서 SAT보다 어렵다.그러나, 부울 공식에 해결책이 있다는 것을 아는 것은 기하급수적으로 많은 가능성이 있기 때문에, 모든 해결책을 세는 데 도움이 되지 않기 때문에, 그 반대는 사실이 아니다.

#SAT는 계산 문제 클래스의 잘 알려진 예로서, #P-complete(sharp p complete로 읽음)로 알려져 있다.즉, 복잡도 클래스 #P의 모든 문제 인스턴스를 #SAT 문제의 인스턴스로 줄일 수 있다.이는 알려진 공식 없이 Enumerative Compinatorics, Statistical Physics, Network Reliability, 인공지능(AI)에서 많은 어려운 계산 문제가 발생하기 때문에 중요한 결과물이다.만약 문제가 어려운 것으로 보인다면, 그것은 멋져 보이는 공식의 부족에 대한 복잡한 이론적 설명을 제공한다.^[2]

#P-완전성

#SAT는 #P 완성.이것을 증명하기 위해서, #SAT는 분명히 #P에 있다는 것을 첫째로 주목하라.

다음으로, 우리는 #SAT가 #P-hard라는 것을 증명한다.어떤 문제라도 #P에서 #A를 취하라.우리는 A가 비결정론적 튜링 머신 M을 사용하여 해결될 수 있다는 것을 알고 있다.한편, 쿡-레빈 정리증거를 통해 우리는 M을 부울 공식 F로 줄일 수 있다는 것을 알고 있다.이제 F의 각 유효한 할당은 M의 고유한 허용 가능한 경로에 해당하며, 그 반대의 경우도 마찬가지다.단, M이 취하는 각각의 허용 가능한 경로는 A에 대한 해결책을 나타낸다.즉, F의 유효한 할당과 A에 대한 해결책 사이에는 편견이 있다.그래서, 쿡-레빈 정리증명에 사용된 감소는 패러디한 것이다.이는 #SAT가 #P-hard임을 암시한다.

난치특례

만족도가 추적 가능한 특별한 경우뿐만 아니라 만족도가 난치(NP-완전)인 경우 해결 방법을 계산하는 것은 난치(#P-완전)여기에는 다음이 포함된다.

3위 SAT

이것은 3SAT의 카운팅 버전이다.SAT의 어떤 공식도 만족스러운 과제 수를 보존하는 3-CNF의 공식으로 다시 쓸 수 있다는 것을 보여줄 수 있다.따라서 #SAT와 #3SAT는 등가수를 세고 #3SAT 역시 #P-완전성을 세고 있다.

2위 SAT

2SAT(2CNF 공식에 솔루션이 있는지 여부 결정)가 다항식임에도 솔루션 개수를 세는 것은 #P-완전이다.^[3]

#호른-SAT

마찬가지로 Horn 만족도가 다항식임에도 불구하고 솔루션 수를 세는 것은 #P-완전이다.이 결과는 SAT와 같은 문제가 #P-완전이라는 일반적인 이분법적 특성화에서 비롯된다.^[4]

플라나르 #3SAT

이것은 Planar 3SAT의 계산 버전이다.리히텐슈타인이^[5] 준 3SAT에서 Planar 3SAT로의 경도 감소는 파렴치하다.이것은 Planar #3SAT가 #P-완전하다는 것을 암시한다.

평면 모노톤 직선 #3SAT

이것은 Planar Monotone Corpilinar 3SAT의 계산 버전이다.^[6]de Berg & Khosravi가^[6] 준 NP-hardity 감소는 parsimonous이다.따라서 이 문제도 #P-완전하다.

추적 가능한 특수 사례

모델 카운팅은 (주문된) BDD와 d-DNNF에 대해 추적 가능(다항식 시간 내에 해결 가능)하다.

참조