SAT 해결사

SAT solver

컴퓨터 과학과 형식적 방법에서 SAT 해결사는 부울 만족도 문제를 해결하는 것을 목표로 하는 컴퓨터 프로그램입니다.(x 또는 y) 및 (x 또는 not y)와 같은 부울 변수 위에 공식을 입력하면 SAT 해결사는 공식이 만족스러운지 여부를 출력합니다. 이는 공식을 참으로 만드는 x와 y의 가능한 값이 존재하거나 x와 y의 값이 존재하지 않는다는 것을 의미합니다.이 경우 x가 참일 때 공식이 만족스러우므로, 해결사는 "만족"을 반환해야 합니다.1960년대 SAT를 위한 알고리즘이 도입된 이후, 현대의 SAT 해결사들은 효율적으로 작동하기 위해 수많은 휴리스틱과 프로그램 최적화를 수반하는 복잡한 소프트웨어 아티팩트로 성장했습니다.

쿡-레빈 정리로 알려진 결과, 부울 만족도는 일반적으로 NP-완전 문제입니다.따라서 기하급수적인 최악의 경우 복잡도를 갖는 알고리즘만 알려져 있습니다.그럼에도 불구하고, 2000년대에 SAT를 위한 효율적이고 확장 가능한 알고리즘이 개발되었으며, 이는 수 만 개의 변수와 수백만 개의 제약 조건을 포함하는 문제 인스턴스를 자동으로 해결하는 기능의 획기적인 발전에 기여했습니다.[1]

SAT 해결사는 종종 공식을 접속 표준 형태로 변환하는 것으로 시작합니다.이들은 종종 DPLL 알고리즘과 같은 핵심 알고리즘을 기반으로 하지만 많은 확장과 기능을 통합합니다.대부분의 SAT 해결사는 제한 시간을 포함하고 있으므로 "Unknown"과 같은 출력을 가진 해결책을 찾지 못하더라도 합리적인 시간 내에 종료됩니다.종종 SAT 해결사는 단순히 답만 제공하는 것이 아니라 공식이 만족스럽지 못한 경우 공식이 만족스러운 경우 또는 만족스럽지 않은 절의 최소 집합인 경우 예제 할당(x, y 등의 값)을 포함한 추가 정보를 제공할 수 있습니다.

최신 SAT 솔루션은 소프트웨어 검증, 프로그램 분석, 제약 조건 해결, 인공지능, 전자 설계 자동화 및 운영 연구 등의 분야에서 상당한 영향을 미쳤습니다.강력한 해결사는 자유 및 오픈 소스 소프트웨어로 쉽게 사용할 수 있으며 제약 로직 프로그래밍의 제약 조건으로 SAT 해결사를 노출하는 것과 같은 일부 프로그래밍 언어에 내장되어 있습니다.

개요

주요 기사:부울 만족도 문제

부울 공식은 부울(제안형) 변수 x, y, z, ... 및 부울 연산 AND, OR, NOT를 사용하여 작성할 수 있는 모든 식입니다.예를들면,

(x 및 y) 또는 (x 및 (z 아님)

할당은 각 변수에 대해 TRUE 또는 FALSE를 선택하는 것으로 구성됩니다.임의의 할당 v에 대해 부울 공식을 평가하고 true 또는 false로 평가할 수 있습니다.공식이 참으로 평가되는 과제(만족 과제라고 함)가 존재하는 경우 공식은 만족할 수 있습니다.

부울 만족도 문제는 부울 공식을 입력할 때 공식이 만족스러운지 아닌지를 결정하는 결정 문제입니다.이 문제는 NP-완전입니다.

DPLL 솔버

주요 기사 : DPLL 알고리즘

DPLL SAT 해결사는 만족스러운 과제를 찾는 가변 과제의 (지수적으로 크기가 큰) 공간을 탐색하기 위해 체계적인 역추적 검색 절차를 사용합니다.기본적인 검색 절차는 1960년대 초에 두 개의 중요한 논문에서 제안되었으며(아래 참고문헌 참조), 현재 일반적으로 Davis라고 불립니다.퍼트넘-로게만-러브랜드 알고리즘("DPLL" 또는 "DLL").[2][3]실용적인 SAT 해결에 대한 많은 현대적인 접근법은 DPLL 알고리즘에서 도출되며 동일한 구조를 공유합니다.산업용 응용프로그램에 나타나는 인스턴스나 임의로 생성된 인스턴스와 같은 특정 클래스의 SAT 문제의 효율성만 개선하는 경우가 많습니다.[4]이론적으로 DPLL 알고리듬 계열에 대해 지수 하한이 입증되었습니다.[citation needed]

DPLL 계열에 속하지 않는 알고리즘에는 확률적 로컬 검색 알고리즘이 포함됩니다.한 가지 예로 워크SAT이 있습니다.확률적 방법은 만족스러운 해석을 찾으려고 노력하지만 DPLL과 같은 완전한 알고리즘과는 달리 SAT 인스턴스가 만족스럽지 않다는 것을 추론할 수 없습니다.[4]

반면, Paturi, Pudlak, Saks 및 Zane에 의한 PPSZ 알고리즘과 같은 무작위화된 알고리즘은 일부 휴리스틱(heristics)에 따라 변수를 임의의 순서로 설정합니다(예: 경계 폭 분해능).휴리스틱이 올바른 설정을 찾을 수 없는 경우 변수는 무작위로 할당됩니다.PPSZ 알고리즘에는 3-SAT에 대한 런타임이[clarify] 있습니다.이것은 Hansen, Kaplan, Zamir 및 Zwick이 3-SAT에 대한 런타임으로 해당 알고리듬의 수정을 발표하기 전까지 이 문제에 대해 가장 잘 알려진 런타임이었습니다.후자는 현재 k의 모든 값에서 k-SAT에 대해 가장 빠르게 알려진 알고리즘입니다.많은 만족스러운 할당이 있는 설정에서 Schöning에 의한 무작위화된 알고리즘은 더 나은 경계를 갖습니다.[5][6][7]

CDCL 해결사

주요 기사 : 갈등주도형 절 학습

2000년대에 개발된 현대 SAT 해결사는 "충돌 주도형"과 "전망형" 두 가지 맛이 있습니다.두 접근 방식 모두 DPLL에서 내려갑니다.[4]갈등 중심 조항 학습(CDCL)과 같은 갈등 중심 해결사는 효율적인 갈등 분석, 조항 학습, 백점프, 단위 전파의 "두 개의 감시 문자" 형태, 적응 분기 및 무작위 재시작으로 기본 DPLL 검색 알고리듬을 강화합니다.기본적인 체계적 검색에 대한 이러한 "추가 사항"은 EDA(전자 설계 자동화)에서 발생하는 대규모 SAT 인스턴스를 처리하는 데 필수적인 것으로 경험적으로 입증되었습니다.[8]잘 알려진 구현으로는 채프(Chaff[9])와 그랩(GRAPH)이 있습니다.[10] 미리 보는 해결사는 특히 (단위 절 전파를 넘어) 감소와 휴리스틱을 강화했습니다.또한 일반적으로 하드 인스턴스에서는 갈등 주도형 해결사보다 강력합니다(갈등 주도형 해결사는 내부에 쉬운 인스턴스가 있는 대규모 인스턴스에서는 훨씬 더 나을 수 있습니다).

2005년 SAT 대회에서 상대적으로 성공적이었던 갈등 주도형 MiniSAT의 코드 라인은 약 600개에 불과합니다.현대적인 병렬 SAT 해결사는 ManySAT입니다.[11]중요한 종류의 문제에 대해 초선형 속도 향상을 달성할 수 있습니다.미래를 내다보는 해결사의 예로는 2007년 SAT 대회에서 입상한 march_dl이 있습니다.OR-Tools의 일부인 Google의 CP-SAT 해결사는 2018년, 2019년, 2020년, 2021년 미니진크 제약 프로그래밍 대회에서 금메달을 획득했습니다.

SAT의 특정 유형의 대규모 랜덤 만족 인스턴스는 설문 조사 전파(SP)를 통해 해결할 수 있습니다.[citation needed]특히 하드웨어 설계 및 검증 애플리케이션에서, 주어진 명제 공식의 만족도 및 기타 논리적 속성은 이진 의사 결정 다이어그램(BDD)으로서 공식의 표현에 기초하여 때때로 결정됩니다.

다양한 SAT 솔루션을 제공하는 사람들은 다양한 인스턴스가 쉽거나 어렵다는 것을 알게 될 것이고, 어떤 사람들은 만족스럽지 못하다는 것을 증명하는 데 탁월하고 다른 사람들은 해결책을 찾는 데 뛰어납니다.이 모든 행동은 SAT 풀이 대회에서 볼 수 있습니다.[12]

기타 테크닉

병렬 SAT 풀이

병렬 SAT 해결사는 포트폴리오, 분할 정복 및 병렬 로컬 검색 알고리즘의 세 가지 범주로 제공됩니다.병렬 포트폴리오를 사용하면 다양한 SAT 솔루션을 동시에 실행할 수 있습니다.각각은 SAT 인스턴스의 복사본을 해결하는 반면 분할 및 정복 알고리즘은 프로세서 간의 문제를 분리합니다.로컬 검색 알고리즘을 병렬화하기 위한 다양한 접근 방식이 존재합니다.

국제 SAT 해결사 대회는 최근 SAT 병렬 해결의 발전을 반영한 병렬 트랙이 있습니다.2016년,[13][15] 2017년[14] 및 2018년에는 24개의 프로세싱 코어를 가진 공유 메모리 시스템에서 벤치마크가 실행되었기 때문에 분산 메모리 또는 많은 코어 프로세서를 위한 솔버가 부족했을 수 있습니다.

포트폴리오

일반적으로 모든 SAT 문제에 대해 다른 모든 해결사보다 성능이 뛰어난 SAT 해결사는 없습니다.알고리즘은 다른 사용자가 어려움을 겪는 문제 인스턴스에서는 잘 수행될 수 있지만 다른 인스턴스에서는 잘 수행되지 않습니다.또한, SAT 인스턴스를 고려할 때, 어떤 알고리즘이 이 인스턴스를 특별히 빠르게 해결할지를 예측할 수 있는 신뢰할 수 있는 방법이 없습니다.이러한 제한은 병렬 포트폴리오 접근 방식에 동기를 부여합니다.포트폴리오는 서로 다른 알고리즘의 집합이거나 동일한 알고리즘의 서로 다른 구성입니다.병렬 포트폴리오의 모든 해결사는 동일한 문제를 해결하기 위해 서로 다른 프로세서에서 실행됩니다.한 해결사가 종료되면 포트폴리오 해결사는 이 한 해결사에 따라 문제를 만족 또는 불만족 상태로 보고합니다.다른 모든 해결사는 종료됩니다.다양한 해결사를 포함하여 포트폴리오를 다양화하면 해결사의 견고성을 높일 수 있습니다.[16]

많은 해결사들이 내부적으로 난수 생성기를 사용합니다.그들의 씨앗을 다양화하는 것은 포트폴리오를 다양화하는 간단한 방법입니다.다른 다양화 전략은 순차 해결사에서 특정 휴리스틱을 활성화, 비활성화 또는 다양화하는 것을 포함합니다.[17]

병렬 포트폴리오의 한 가지 단점은 중복 작업의 양입니다.순차적 해결사에서 절 학습을 사용하면 병렬 실행 해결사 간에 학습된 절을 공유하면 중복 작업을 줄이고 성능을 높일 수 있습니다.그러나 최고의 해결사 포트폴리오를 병렬로 운영하는 것만으로도 경쟁력 있는 병렬 해결사가 됩니다.그러한 해결사의 예로는 PPfolio가 있습니다.[18][19]병렬 SAT 해결사가 제공할 수 있는 성능에 대한 하한값을 찾도록 설계되었습니다.최적화가 되지 않아 많은 양의 중복 작업이 있었음에도 불구하고 공유 메모리 시스템에서 좋은 성능을 보였습니다.HordeSat은[20] 컴퓨팅 노드의 대규모 클러스터를 위한 병렬 포트폴리오 해결사입니다.핵심에 동일한 순차적 해결사의 구성 인스턴스를 다르게 사용합니다.특히 하드 SAT 인스턴스의 경우 HordeSat은 선형 속도를 높일 수 있으므로 런타임을 크게 줄일 수 있습니다.

최근 몇 년 동안 병렬 포트폴리오 SAT 해결사는 국제 SAT 해결사 대회의 병렬적인 흐름을 주도해 왔습니다.그러한 해결사의 주목할 만한 예로는 플링겔링(Plingeling) 및 무통-mcomposes(무통-mcomposes)가 있습니다.[21]

분할 정복

병렬 분할-정복은 병렬 포트폴리오와 대조적으로 처리 요소 간에 검색 공간을 분할하려고 합니다.순차적 DPLL과 같은 분할 및 정복 알고리즘은 이미 검색 공간을 분할하는 기술을 적용하므로 병렬 알고리즘으로의 확장은 간단합니다.그러나 분할 후에는 단위 전파와 같은 방법으로 인해 부분적인 문제가 복잡성에 큰 차이가 있을 수 있습니다.따라서 DPLL 알고리즘은 일반적으로 검색 공간의 각 부분을 동일한 시간에 처리하지 않으므로 로드 밸런싱 문제가 발생합니다.[16]

Tree illustrating the look-ahead phase and the resulting cubes.
공식 에 대한 큐브 위상 결정 휴리스틱은 어떤 변수(원)를 할당할지 선택합니다.컷오프 휴리스틱이 추가 분기를 중단하기로 결정한 후 부분 문제(직각)는 CDCL을 사용하여 독립적으로 해결됩니다.

비시동적 역추적으로 인해 갈등 중심 조항 학습의 병렬화는 더 어렵습니다.이를 극복하기 위한 하나의 방법이 큐브 앤 컨커 패러다임입니다.[22]그것은 두 단계로 나누어 해결할 것을 제안합니다."큐브" 단계에서 문제는 수천 개에서 최대 수백만 개의 섹션으로 나뉩니다.이 작업은 "큐브"라고 하는 부분 구성 집합을 찾는 미리 보기 해결사에 의해 수행됩니다.입방체는 원래 공식의 변수 부분 집합의 연결로 볼 수도 있습니다.공식과 함께 각 정육면체는 새로운 공식을 형성합니다.이러한 공식은 갈등 주도형 해결사에 의해 독립적으로 동시에 해결될 수 있습니다.이 공식들의 분배는 원래 공식과 동일하므로 공식들 중 하나가 만족스러운 경우 문제는 만족스러운 것으로 보고됩니다.미리 보기 해결사는 작지만 어려운 문제에 유리하기 [23]때문에 문제를 여러 개의 하위 문제로 점진적으로 나누는 데 사용됩니다.이러한 하위 문제는 더 쉽지만 여전히 크기 때문에 갈등을 유발하는 해결사에게 이상적인 형태입니다.또한 갈등 중심의 해결사는 훨씬 더 로컬한 정보를 기반으로 결정을 내리는 반면, 미래 지향적인 해결사는 전체 문제를 고려합니다.큐브 단계에는 세 가지 휴리스틱이 관련되어 있습니다.큐브의 변수는 의사결정 휴리스틱에 의해 선택됩니다.방향 휴리스틱은 먼저 탐색할 변수 할당(참 또는 거짓)을 결정합니다.만족스러운 문제 사례에서는 만족스러운 분기를 먼저 선택하는 것이 좋습니다.컷오프 휴리스틱은 큐브 확장을 중단하고 대신 순차적 충돌 중심 해결사로 전달할 시기를 결정합니다.가급적이면 정육면체는 해결하기에 비슷하게 복잡합니다.[22]

트리엔젤링은 큐브 앤 컨커(Cube-and-Conquer) 패러다임을 적용하는 병렬 솔버의 예입니다.2012년 도입 이후 국제 SAT 해결사 대회에서 많은 성공을 거두었습니다.큐브 앤 컨커는 부울 피타고라스 삼중항 문제를 푸는 데 사용되었습니다.[24]

큐브 앤 컨커(Cube-and-Conquer)는 2010년에 DPLL을 사용하여 (부분 문제를 분할하고 해결하는) 두 단계가 모두 수행된 반데르 웨르덴 수 w(2;3,17)와 w(2;3,18)를 계산하는 데 사용된 DPLL 기반 분할 앤 컨커 접근법의 수정 또는 일반화입니다.

로컬 검색

SAT 해결을 위한 병렬 로컬 검색 알고리즘을 향한 한 가지 전략은 서로 다른 처리 장치에서 동시에 여러 개의 가변 플립을 시도하는 것입니다.[26]다른 하나는 위와 같은 포트폴리오 방식을 적용하는 것이지만, 로컬 검색 해결사는 조항을 생성하지 않기 때문에 조항 공유가 불가능합니다.또는 로컬에서 생성된 구성을 공유할 수도 있습니다.이러한 구성은 로컬 해결사가 검색을 다시 시작하기로 결정할 때 새 초기 구성을 생성하는 데 사용할 수 있습니다.[27]

적용들

수학에서

SAT 해결사는 컴퓨터 지원 증명을 통해 수학적 정리를 증명하는 데 도움을 주기 위해 사용되었습니다.램지 이론에서, 이전에 알려지지 않은 여러 반데르 워든 수는 FPGA에서 실행되는 전문 SAT 솔버의 도움으로 계산되었습니다.[28][29]2016년 Marijn Hole, Oliver Kullmann, Victor Marek는 SAT 솔버를 사용하여 정수를 7825까지 요구되는 방식으로 색칠할 수 있는 방법이 없음을 보여줌으로써 부울 피타고라스 삼중 문제를 해결했습니다.[30][31]Schur number의 작은 값도 Hule이 SAT 솔버를 사용하여 계산했습니다.[32]

소프트웨어 검증중

SAT 솔버는 하드웨어 및 소프트웨어의 공식 검증에 사용됩니다.모델 검사(특히, 경계 모델 검사)에서 SAT 해결사는 유한 상태 시스템이 의도된 동작의 사양을 충족하는지 여부를 검사하는 데 사용됩니다.[33][34]

SAT 해결사는 만족도 모듈로 이론(SMT) 해결사가 구축되는 핵심 구성 요소로 작업 스케줄링, 기호 실행, 프로그램 모델 검사, 호어 로직 기반의 프로그램 검증 등의 문제에 사용됩니다.[35]이러한 기법은 제약 조건 프로그래밍 및 논리 프로그래밍과도 밀접한 관련이 있습니다.

기타지역

운영 연구에서는 최적화 및 스케줄링 문제를 해결하기 위해 SAT 솔버를 적용해 왔습니다.[36]

사회적 선택 이론에서 SAT 해결사는 불가능한 정리를 증명하는 데 사용되었습니다.[37]Tang과 Lin은 Arrow의 정리와 다른 고전적인 불가능성 정리를 증명하기 위해 SAT 해결사를 사용했습니다.가이스트와 엔드리스는 집합 확장과 관련된 새로운 불가능성을 찾기 위해 이를 사용했습니다.Brandt와 Geist는 이 접근 방식을 사용하여 전략적 토너먼트 솔루션에 대한 불가능성을 입증했습니다.다른 저자들은 이 기술을 사용하여 노쇼 역설, 반단일성, 확률적 투표 규칙에 대한 새로운 불가능성을 증명했습니다.Brandl, Brandt, Peters 및 Stricer는 이를 사용하여 부분적인 사회적 선택을 위한 전략적 증명, 효율적, 공정한 규칙의 불가능성을 증명했습니다.[38]

참고 항목

참고문헌

  1. ^ Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Propagation = Lazy Clause Generation", Principles and Practice of Constraint Programming – CP 2007, Lecture Notes in Computer Science, vol. 4741, pp. 544–558, CiteSeerX 10.1.1.70.5471, doi:10.1007/978-3-540-74970-7_39, modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables
  2. ^ Davis, M.; Putnam, H. (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201. doi:10.1145/321033.321034. S2CID 31888376.
  3. ^ Davis, M.; Logemann, G.; Loveland, D. (1962). "A machine program for theorem-proving" (PDF). Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
  4. ^ a b c Zhang, Lintao; Malik, Sharad (2002), "The Quest for Efficient Boolean Satisfiability Solvers", Computer Aided Verification, Springer Berlin Heidelberg, pp. 17–36, doi:10.1007/3-540-45657-0_2, ISBN 978-3-540-43997-4
  5. ^ Schöning, Uwe (Oct 1999). "A probabilistic algorithm for k-SAT and constraint satisfaction problems" (PDF). 40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039). pp. 410–414. doi:10.1109/SFFCS.1999.814612. ISBN 0-7695-0409-4. S2CID 123177576.
  6. ^ "k-SAT를 위한 향상된 지수 시간 알고리즘", Paturi, Pudlak, Saks, Zani
  7. ^ "편파 PPSZ를 이용한 더 빠른 k-SAT 알고리즘", Hansen, Kaplan, Zamir, Zwick
  8. ^ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
  9. ^ Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S. (2001). "Chaff: Engineering an Efficient SAT Solver" (PDF). Proceedings of the 38th conference on Design automation (DAC). p. 530. doi:10.1145/378239.379017. ISBN 1581132972. S2CID 9292941.
  10. ^ Marques-Silva, J. P.; Sakallah, K. A. (1999). "GRASP: a search algorithm for propositional satisfiability" (PDF). IEEE Transactions on Computers. 48 (5): 506. doi:10.1109/12.769433. Archived from the original (PDF) on 2016-11-04. Retrieved 2015-08-28.
  11. ^ http://www.cril.univ-artois.fr/ ~jabbour/manysat.htm[bare URL]
  12. ^ "The international SAT Competitions web page". Retrieved 2007-11-15.
  13. ^ "SAT Competition 2016". baldur.iti.kit.edu. Retrieved 2020-02-13.
  14. ^ "SAT Competition 2017". baldur.iti.kit.edu. Retrieved 2020-02-13.
  15. ^ "SAT Competition 2018". sat2018.forsyte.tuwien.ac.at. Retrieved 2020-02-13.
  16. ^ a b Balyo, Tomáš; Sinz, Carsten (2018), "Parallel Satisfiability", Handbook of Parallel Constraint Reasoning, Springer International Publishing, pp. 3–29, doi:10.1007/978-3-319-63516-3_1, ISBN 978-3-319-63515-6
  17. ^ Biere, Armin. "Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010" (PDF). SAT-RACE 2010.
  18. ^ "ppfolio solver". www.cril.univ-artois.fr. Retrieved 2019-12-29.
  19. ^ "SAT 2011 Competition: 32 cores track: ranking of solvers". www.cril.univ-artois.fr. Retrieved 2020-02-13.
  20. ^ Balyo, Tomáš; Sanders, Peter; Sinz, Carsten (2015), HordeSat: A Massively Parallel Portfolio SAT Solver, Lecture Notes in Computer Science, vol. 9340, Springer International Publishing, pp. 156–172, arXiv:1505.03340, doi:10.1007/978-3-319-24318-4_12, ISBN 978-3-319-24317-7, S2CID 11507540
  21. ^ "SAT Competition 2018". sat2018.forsyte.tuwien.ac.at. Retrieved 2020-02-13.
  22. ^ a b Heule, Marijn J. H.; Kullmann, Oliver; Wieringa, Siert; Biere, Armin (2012), "Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads", Hardware and Software: Verification and Testing, Lecture Notes in Computer Science, Springer Berlin Heidelberg, vol. 7261, pp. 50–65, doi:10.1007/978-3-642-34188-5_8, ISBN 978-3-642-34187-8
  23. ^ Heule, Marijn J. H.; van Maaren, Hans (2009). "Look-Ahead Based SAT Solvers" (PDF). Handbook of Satisfiability. IOS Press. pp. 155–184. ISBN 978-1-58603-929-5.
  24. ^ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016), "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer", Theory and Applications of Satisfiability Testing – SAT 2016, Lecture Notes in Computer Science, Springer International Publishing, vol. 9710, pp. 228–245, arXiv:1605.00723, doi:10.1007/978-3-319-40970-2_15, ISBN 978-3-319-40969-6, S2CID 7912943
  25. ^ Ahmed, Tanbir (2010). "Two new van der Waerden numbers w(2;3,17) and w(2;3,18)". Integers. 10 (4): 369–377. doi:10.1515/integ.2010.032. MR 2684128. S2CID 124272560.
  26. ^ Roli, Andrea (2002), "Criticality and Parallelism in Structured SAT Instances", Principles and Practice of Constraint Programming - CP 2002, Lecture Notes in Computer Science, vol. 2470, Springer Berlin Heidelberg, pp. 714–719, doi:10.1007/3-540-46135-3_51, ISBN 978-3-540-44120-5
  27. ^ Arbelaez, Alejandro; Hamadi, Youssef (2011), Improving Parallel Local Search for SAT, Lecture Notes in Computer Science, vol. 6683, Springer Berlin Heidelberg, pp. 46–60, doi:10.1007/978-3-642-25566-3_4, ISBN 978-3-642-25565-6, S2CID 14735849
  28. ^ Kouril, Michal; Paul, Jerome L. (2008). "The van der Waerden Number $W(2,6)$ Is 1132". Experimental Mathematics. 17 (1): 53–61. ISSN 1058-6458.
  29. ^ Kouril, Michal (2012). "Computing the van der Waerden number W(3,4)=293". Integers. 12: A46. MR 3083419.
  30. ^ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016), Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer, vol. 9710, pp. 228–245, retrieved 2023-10-26
  31. ^ Lamb, Evelyn (2016-06-01). "Two-hundred-terabyte maths proof is largest ever". Nature. 534 (7605): 17–18. doi:10.1038/nature.2016.19990. ISSN 1476-4687.
  32. ^ "Schur Number Five". www.cs.utexas.edu. Retrieved 2023-10-26.
  33. ^ Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan (2001-07-01). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design. 19 (1): 7–34. doi:10.1023/A:1011276507260. ISSN 1572-8102.
  34. ^ Biere, Armin; Cimatti, Alessandro; Clarke, Edmund M.; Strichman, Ofer; Zhu, Yunshan (2003). "Bounded Model Checking" (PDF). Advances in Computers. 58 (2003) – via Academic Press.
  35. ^ De Moura, Leonardo; Bjørner, Nikolaj (2011-09-01). "Satisfiability modulo theories: introduction and applications". Communications of the ACM. 54 (9): 69–77. doi:10.1145/1995376.1995394. ISSN 0001-0782.
  36. ^ Coelho, José; Vanhoucke, Mario (2011-08-16). "Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers". European Journal of Operational Research. 213 (1): 73–82. doi:10.1016/j.ejor.2011.03.019. ISSN 0377-2217.
  37. ^ 로봇이 곧 이 인용을 완료할 것입니다.대기열 arXiv:2104.08594를 이동하려면 여기를 클릭합니다.
  38. ^ Brandl, Florian; Brandt, Felix; Peters, Dominik; Stricker, Christian (2021-07-18). "Distribution Rules Under Dichotomous Preferences: Two Out of Three Ain't Bad". Proceedings of the 22nd ACM Conference on Economics and Computation. EC '21. New York, NY, USA: Association for Computing Machinery. pp. 158–179. doi:10.1145/3465456.3467653. ISBN 978-1-4503-8554-1.