최대 만족도 문제

계산 복잡성 이론에서 최대 만족도 문제(MAX-SAT)는 결합 정상 형태의 주어진 부울 공식의 최대 개수를 결정하는 문제로서, 공식의 변수에 진실 값을 할당함으로써 이루어질 수 있다.모든 조항을 진실되게 만드는 진실과제가 존재하는지 여부를 묻는 부울 만족도 문제의 일반화다.

예

결막정상형식

${\displaystyle (x_{0}\lor x_{1}\land (x_{0}\lor \lot x_{1}\land (\lot x_{0}\lor x_{1})\land (\lot x_{0}\lor \lot x_{1}}}}$

만족스럽지 않다: 어떤 진실 값이 그것의 두 변수에 할당되든, 적어도 네 개의 조항 중 하나는 거짓이 될 것이다.그러나 4개 조항 중 3개 조항이 진실되게 만드는 방식으로 진실 가치를 부여할 수 있다. 실제로 모든 진실 배정은 이렇게 할 것이다.따라서 이 공식이 MAX-SAT 문제의 한 예로서 주어진다면 문제의 해결책은 숫자 3이다.

경도

MAX-SAT 문제는 NP-완전인 부울 만족도 문제의 해결로 쉽게 이어지기 때문에 NP-SAT 문제는 NP-hard이다.

또한 최적의 해결책의 보장 근사율 내에서 다수의 절들을 만족시키는 대략적인 문제의 해결책을 찾기가 어렵다.보다 정확히 말하면, 문제는 APX-완전성이므로 P = NP가 아닌 한 다항 시간 근사치를 인정하지 않는다.^[1][2][3]

가중치 MAX-SAT

보다 일반적으로는 MAX-SAT의 가중치 버전을 다음과 같이 정의할 수 있다: 각 절에 음이 아닌 가중치가 할당된 결합 정상 형태 공식에 주어진 경우, 만족된 절의 결합 가중치를 최대화하는 변수에 대한 진실 값을 찾는다.MAX-SAT 문제는 가중 MAX-SAT의 한 예로서 모든 가중치가 1이다.^[4][5][6]

근사 알고리즘

1/2 근사치

확률 1/2로 각 변수를 참으로 랜덤하게 할당하면 예상 근사치가 발생한다.더 정확히 말하자면, 각 조항이 최소한k변수(1 - 2^−k) 근사치를 산출한다.^[7]이 알고리즘은 조건부 확률의 방법을 사용하여 절충할 수 있다.^[8]

(1-1/e)-대략

MAX-SAT는 또한 정수 선형 프로그램(ILP)을 사용하여 표현할 수 있다.접합 정규 폼 공식 수정F변수와 함께x₁,x₂, ...,x_n, 그리고 letC의 조항을 나타내다F각 절에 대하여.c에C, letS⁺_c 그리고S⁻_c 부정되지 않는 변수 집합을 나타냄c, 그리고 부정된 것.c각각,변수들y_x ILP는 공식의 변수와 일치한다.F, 반면에 변수들z_c 조항에 해당된다.ILP는 다음과 같다.

극대화하다	${\displaystyle \sum _{c\in C}w_{c}\cdot z_{c}}$		(만족 조항의 가중치 부여)
의 대상이 되다	${\displaystyle z_{c}\leq \sum _{x\in S_{c}^{+y_{x}+\sum _{x\in S_{c}^{-}}:{-}(1-y_{x})}}}}$	$모든{\displaystyle }$ c${\displaystyle }$for ${\displaystyle C}$ ${\displaystyle c\in C}$에 대해	(진정한 비부정 변수 또는 거짓 부정 변수인 경우 진실한 변수임)
	${\displaystyle z_{c}\in \{0,1\}}$	$모든{\displaystyle }$ c${\displaystyle }$for ${\displaystyle C}$ ${\displaystyle c\in C}$에 대해$.$	(모든 조항이 충족되거나 충족되지 않음)
	${\displaystyle y_{x}\in \{0,1\}}$	모든 $x{\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle F}$ ${\displaystyle x\in F}$에 대해$.$	(모든 변수는 참 또는 거짓)

위의 프로그램은 다음과 같은 선형 프로그램으로 완화할 수 있다.L:

극대화하다	${\displaystyle \sum _{c\in C}w_{c}\cdot z_{c}}$		(만족 조항의 가중치 부여)
의 대상이 되다	${\displaystyle z_{c}\leq \sum _{x\in S_{c}^{+y_{x}+\sum _{x\in S_{c}^{-}}:{-}(1-y_{x})}}}}$	$모든{\displaystyle }$ c${\displaystyle }$for ${\displaystyle C}$ ${\displaystyle c\in C}$에 대해	(진정한 비부정 변수 또는 거짓 부정 변수인 경우 진실한 변수임)
	${\displaystyle 0\leq z_{c}\leq 1}$	$모든{\displaystyle }$ c${\displaystyle }$for ${\displaystyle C}$ ${\displaystyle c\in C}$에 대해$.$
	${\displaystyle 0\leq y_{x}\leq 1}$	모든 $x{\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle F}$ ${\displaystyle x\in F}$에 대해$.$

이완을 사용하는 다음 알고리즘은 예상(1-1/e)-대략이다.^[9]

1. 선형 프로그램 해결L그리고 해결책을 얻는다.O
2. 변수 설정x확률적으로 진실하다y_x 어디에y_x 에 주어진 값이다.O.

또한 이 알고리즘은 조건부 확률의 방법을 사용하여 절충될 수 있다.

3/4 근사치

1/2 근사치 알고리즘은 절이 클 때 더 잘한다(1-1/).e)-조항이 작을 때 근사치가 더 잘 된다.다음과 같이 조합할 수 있다.

1. 1/2 근사치 알고리즘을 실행하여 진실 할당을 얻으십시오.X.
2. (분산)(1-1/e) 근사치를 실행하여 진실 할당을 얻으십시오.Y.
3. 다음 중 하나를 출력하십시오.X또는Y만족 조항의 가중치를 최대화한다.

이는 결정론적 요인(3/4)-대략이다.^[10]

예

공식에 관하여

$${\displaystyle F=\underbrace {(x\lor y)} _{\text{weight }\land \underbrace {(x\lor \lot y)} _{\텍스트{not x\lor z)} _{\textwepsilon}}}}$$

여기서 > ${\displaystyle \epsilon >0$ (1-1/)e)- 근사치는 확률 1/2로 각 변수를 True로 설정하므로 1/2 근사치와 동일하게 동작한다.의 할당을 가정하여xderandomization 동안 먼저 선택되며, derandomized 알고리즘은 총 $중량{\displaystyle \mathrm{}}$ 3${\displaystyle }$+ $[\displaystyle 3+\epsilon }$을(를) 가진 솔루션을 선택하는 반면$,$ 최적 솔루션은 $중량{\displaystyle \mathrm{}}$ 4${\displaystyle }$+ $[\displaystyle$ 4$+\epsilon }$을(를)로 한다$.$^[11]

해결사

MAX-SAT를 위한 정확한 해결사들이 최근 몇 년 동안 많이 개발되었고, 그 중 많은 해결사들이 부울만족도 문제와 관련 문제들에 대한 잘 알려진 콘퍼런스인 SAT 콘퍼런스에 발표되었다.2006년 SAT Conference는 사이비 부울 만족도 문제와 정량화된 부울 공식 문제에 대해 과거에 그랬던 것처럼 MAX-SAT를 위한 실제 해결사의 성능을 비교하는 첫 번째 MAX-SAT 평가를 개최하였다.NP-강성 때문에 대형 MAX-SAT 인스턴스는 일반적으로 정확하게 해결할 수 없으며, 종종 근사 알고리즘과 경험적^[12] 접근에 의존해야 한다.

지난 Max-SAT 평가에는 다음과 같은 몇 가지 해결사가 제출되었다.

• 분기 및 바운드 기반:클론, MaxSatz (Satz 기반), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
• 만족도 기반: SAT4J, QMaxSat.
• 불만족 기반: msuncore, WPM1, PM2.

특례

MAX-SAT는 Boolean 만족도 문제의 최적화 확장 중 하나로, 주어진 Boolean 공식의 변수를 TRUE로 평가할 수 있는 방식으로 할당할 수 있는지 여부를 결정하는 문제다. 2-만족도에서와 같이 조항이 최대 2 리터까지 제한되면 MAX-2SAT 문제가 발생한다.만약 그들이 3-만족도에서와 같이 조항당 최대 3리터로 제한된다면, 우리는 MAX-3SAT 문제를 얻게 된다.

관련 문제

부울 공식의 결합 정상 형태 만족도와 관련된 많은 문제들이 있다.

• 의사결정 문제:
  • 2SAT
  • 3SAT
• 최적화 문제, 충족되는 절의 수를 최대화하는 것이 목표인 경우:
  • MAX-SAT 및 대응 가중 버전 가중 MAX-SAT
  • MAX-kSAT, 각 조항이 정확히 존재하는 곳k변수:
    • MAX-2SAT
    • MAX-3SAT
    • 맥섹삿
  • 부분 최대 만족도 문제(PMAX-SAT)는 주어진 절의 하위 집합을 할당함으로써 충족될 수 있는 절의 최대 수를 요구한다.나머지 조항은 반드시 충족되어야 한다.
  • 일련의 SAT 문제가 주어진 소프트 만족도 문제(soft-SAT)는 어떤 과제에 의해서도 충족될 수 있는 문제의 최대 수를 요구한다.^[13]
  • 최소 만족도 문제.
• MAX-SAT 문제는 제약 만족도 문제의 변수가 실수 집합에 속하는 경우까지 확대될 수 있다.문제는 제약조건의 q-완화 교차점이 비어 있지 않은 가장 작은 q를 찾는 것이다.^[14]

참고 항목

• 부울 만족도 문제
• 제약 만족도
• 만족도 모듈로 이론

외부 링크

• http://www.satisfiability.org/
• https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
• http://www.maxsat.udl.cat
• 숨겨진 최적 솔루션을 사용한 가중치 최대 2-SAT 벤치마크
• MAX-SAT 근사치에 대한 강의 노트

참조

• Vazirani, Vijay V. (2001), Approximation Algorithms (PDF), Springer-Verlag, ISBN 978-3-540-65367-7