워크SAT
WalkSAT컴퓨터 공학에서 GSAT와 워크에서SAT는 부울 만족도 문제를 해결하기 위한 로컬 검색 알고리즘이다.null
두 알고리즘은 모두 부울 논리에서의 공식에 대해 작용하며, 또는 결합 정상 형태로 변환된다.공식의 각 변수에 랜덤 값을 할당하는 것으로 시작한다.과제가 모든 조항을 충족하면 알고리즘이 종료되어 할당을 반환한다.그렇지 않으면 변수가 뒤집히고 이후 모든 조항이 충족될 때까지 위의 내용을 반복한다.WalkSAT와 GSAT는 플립할 변수를 선택하는 데 사용되는 방법이 다르다.null
GSAT는 새로운 과제에서 불만족 조항 수를 최소화하거나 어느 정도 확률로 변수를 무작위로 선택하는 변경을 한다.null
WalkSAT는 우선 현재 과제에서 만족하지 못하는 조항을 선택한 다음 해당 조항 내에서 변수를 생략한다.그 조항은 불만족스러운 조항 중에서 무작위로 선정된다.변수 중 하나를 무작위로 선택할 확률과 함께 이전에 가장 적게 충족된 조항이 만족되지 않게 되는 변수를 선택한다.무작위로 고를 때, 워크SAT는 현재 잘못된 할당을 고치는 조항의 변수 개수 중 하나 이상을 보장받는다.WalkSAT는 예측 최적 변수를 선택할 때 GSAT보다 낮은 계산을 해야 하는데, 이는 가능성이 더 적기 때문이다.null
알고리즘은 너무 오랫동안 해결책이 발견되지 않은 경우, 불만족 조항 수의 국소적 미니마에서 벗어나는 방법으로 새로운 무작위 할당으로 재시작할 수 있다.null
다양한 버전의 GSAT 및 워크SAT가 존재한다.워크SAT는 자동화된 계획 문제에서 전환하여 발생하는 만족도 문제를 해결하는 데 특히 유용한 것으로 입증되었다.계획 문제를 부울 만족도 문제로 전환하는 계획을 위한 접근방식을 satplan이라고 한다.null
MaxWalkSAT는 가중 만족도 문제를 해결하기 위해 고안된 WalkSAT의 변형으로, 각 조항이 가중치와 연관되어 있으며, 목표는 해당 할당에 의해 충족되는 조항의 총 가중치를 최대화하는 과제(전체 공식을 충족하거나 충족하지 않을 수 있는 과제)를 찾는 것이다.null
참조
- 헨리 코츠와 B.셀만(1996년).한계에 도전하는 것: 계획, 명제적 논리, 확률적 탐색.제13차 전국 인공지능 회의(AAAI'96)의 절차에서, 1194–1201페이지.
- Papadimitriou, Christos H. (1991), "On selecting a satisfying truth assignment", Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, pp. 163–169, doi:10.1109/SFCS.1991.185365, ISBN 978-0-8186-2445-2.
- Schöning, U. (1999), "A probabilistic algorithm for k-SAT and constraint satisfaction problems", Proceedings of 40th Annual Symposium on Foundations of Computer Science, pp. 410–414, CiteSeerX 10.1.1.132.6306, doi:10.1109/SFFCS.1999.814612, ISBN 978-0-7695-0409-4.
- B. Selman과 Henry Kautz (1993년).GSAT에 대한 도메인 독립형 확장: 대규모 구조적 만족도 문제 해결.제13차 국제인공지능 공동회의(IJCAI'93호)에 290-295페이지가 실려 있다.
- 바트 셀만, 헨리 카우츠, 브람 코헨."만족도 검사를 위한 현지 검색 전략"최종 버전은 Clike, Coloring 및 만족도에 표시됨:1993년 10월 11일-13일 제2회 DIMACS 이행 도전.데이비드 S. 존슨과 마이클 A. 속임수, 에드.이산수학과 이론 컴퓨터 과학의 DIMACS 시리즈, 26권, AMS, 1996.
- B. Selman, H. Levesque, D.미첼(1992년).어려운 만족도 문제를 해결하기 위한 새로운 방법.제10차 인공지능 전국회의(AAAI'92)의 '프로세스'에서는 440~446페이지에 이른다.
