gophersat
1.0.0
이것은 순수하게 Go로 작성된 SAT 및 의사 부울 솔버인 Gophersat입니다. Gophersat는 Artois University 및 CNRS의 CRIL(Centre de Recherche en Informatique de Lens)에 의해 개발되었습니다. MIT 라이선스로 배포됩니다. Gophersat은 다소 효율적입니다. 즉, 일반적인 SAT 벤치마크에서는 강력한 영감을 받은 최상위 솔버(즉, Glucose 또는 minisat)보다 약 2~5배 느리게 실행됩니다. 또한 MAXSAT 문제, 의사 부울 결정 및 최적화 문제를 해결할 수도 있습니다.
Gophersat의 마지막 안정 버전은 버전 1.4입니다. 여기에는 선택적 절단면 해결 전략이 포함됩니다.
유명한 비둘기집 문제와 같은 일부 문제는 순수한 논리적 추론을 사용하여 해결하는 데 매우 오랜 시간이 걸립니다.
비둘기집 문제는 다음과 같이 표현될 수 있습니다. 같은 구멍에 여러 마리의 비둘기를 넣고 모든 비둘기를 한 구멍에 넣지 않고 m = n-1인 m개의 비둘기집에 n마리의 비둘기를 넣는 것이 가능합니까? 대답은 분명합니다. 3개의 구멍에 비둘기 4마리가 있다면 다른 구멍에 모두 넣을 수는 없습니다. 그런데 이것을 어떻게 증명 하나요? SAT 또는 PB 해결사는 가능한 모든 조합을 시도하여 이를 증명하며 가능한 조합의 수는 기하급수적으로 늘어납니다. 따라서 n=20인 문제를 해결하려는 노력은 명확한 답이 있는 문제에도 불구하고 실제로 실현 가능하지 않습니다.
일부 PB 솔버는 대체 전략인 절단면 전략을 구현합니다. 이 문서에서는 자세히 설명하지 않지만 이 상태는 순수한 논리적 추론으로는 효율적으로 해결할 수 없지만 대부분의 문제에서는 속도가 느려지는 비둘기집 문제와 같은 일부 문제에서 매우 효율적일 수 있습니다.
이제 Gophersat에서 절단면을 사용할 수 있습니다. -cp 명령줄 옵션을 사용하면 됩니다. 따라서 전화하는 대신 다음을 수행하세요.
gophersat problem.opb
그냥 전화하세요:
gophersat -cp problem.opb
Gophersat의 마지막 안정 버전은 버전 1.3입니다. MAXSAT 문제를 처리할 때 기본 솔버에 액세스하는 기능을 추가하는 사소한 업데이트입니다.
Gophersat 버전 1.2에는 문제가 UNSAT인 경우 RUP 인증서를 제공하고 공식의 만족스럽지 못한 하위 집합을 추출하는 기능을 제공하여 UNSAT 인스턴스를 이해하는 방법이 포함되어 있습니다. vew 버그도 수정되었으며 증분 SAT 해결에 대한 지원이 개선되었습니다.
이러한 기능에 대해 자세히 알아보려면 UNSAT 인증서 및 MUS에 대한 튜토리얼을 확인하세요.
gophersat 실행 파일로 인증서를 생성하려면 다음을 호출하면 됩니다.
gophersat -certified problem.cnf
그런 다음 인증서는 RUP 표기법을 사용하여 표준 출력에 인쇄됩니다. 인증서는 즉시 생성되므로 문제가 실제로 만족되더라도 부분적이고 쓸모없는 인증서가 생성된다는 점에 유의하세요. 이는 커뮤니티의 일반적인 관행이며, 생성된 조항이 쓸모없는 노이즈가 되더라도 실제로는 문제가 되지 않습니다.
UNSAT 인스턴스에서 MUS를 추출하려면 다음을 호출하세요.
gophersat -mus problem.cnf
MUS는 표준 출력에 인쇄됩니다. 문제가 UNSAT가 아닌 경우 오류 메시지가 표시됩니다.
현재 이러한 기능은 순수한 SAT 문제(즉, 의사 부울 문제가 아닌)에만 사용할 수 있습니다.
버전 1.1부터 Gophersat에는 순수 SAT 문제를 위한 새롭고 더 효율적인 코어 솔버와 MAXSAT 문제를 다루는 패키지가 포함되어 있습니다. 또한 새로운 모델이 발견되는 즉시 채널에 기록되는 최적화 및 모델 계산을 위한 새로운 API도 포함되어 있습니다.
버전 1.0부터 Gophersat의 API는 안정적인 것으로 간주됩니다. 즉, 주요 버전이 변경될 때까지 API가 이전 버전과의 호환성을 유지한다는 의미입니다. 즉, 프로그램이 gophersat 버전 1.0에서 작동하는 경우 버전 1.1 이상에서는 계속 작동하지만 2.0 이상의 버전에서는 반드시 작동할 필요는 없습니다.
"아직 작동 중"이라는 말은 "메모리 측면이나 시간 측면에서 동일한 성능을 갖습니다"가 아니라 "동일한 출력을 컴파일하고 생성합니다"를 의미할 뿐입니다. 이는 중요한 차이점입니다. 마이너 버전 업그레이드 중에 새로운 경험적 방법이나 데이터 유형이 도입될 수 있으며, 이는 특정 문제가 이전보다 더 빠르거나 느리게 해결될 수 있음을 의미합니다.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat는 독립형 솔버(DIMACS CNF 파일 읽기)로 사용하거나 Go 프로그램의 라이브러리로 사용할 수 있습니다.
DIMACS 파일을 해석하려면 다음 구문을 사용하여 gophersat를 호출할 수 있습니다.
gophersat --verbose file.cnf
여기서 --verbose 해석 프로세스 중에 솔버가 정보를 표시하도록 하는 선택적 매개변수입니다.
Gophersat은 또한 사용자에게 친숙하지 않은 DIMACS 형식으로 표현되는 문제뿐만 아니라 보다 일반적인 부울 공식을 읽고 해결할 수 있습니다. 또한 기본적으로 카디널리티 제약 조건, 즉 n > 1인 n 리터럴이 참이어야 하는 절을 처리합니다.
Gophersat는 독립형 솔버(OPB 파일 읽기)로 사용하거나 Go 프로그램의 라이브러리로 사용할 수 있습니다.
의사 부울 문제(결정 문제든 최적화 문제든)를 해결하려면 다음 구문을 사용하여 gophersat를 호출할 수 있습니다.
gophersat --verbose file.opb
여기서 --verbose 해석 프로세스 중에 솔버가 정보를 표시하도록 하는 선택적 매개변수입니다.
현재로서는 작은 정수에 대한 선형 제약 조건(가중치 리터럴의 합)에 대한 소위 DEC-SMALLINT-LIN 문제 및 OPT-SMALLINT-LIN, 즉 결정 문제(해결책이 있는지 없는지)만 해결할 수 있습니다. (n < 2^30) 또는 작은 정수에 대한 선형 제약 조건에 대한 최적화 문제(주어진 비용 함수를 최소화하는 가장 좋은 솔루션은 무엇입니까).
maxsat 패키지 덕분에 Gophersat는 이제 MAXSAT 문제를 해결할 수 있습니다.
가중치 MAXSAT 문제를 해결하려면 다음 구문을 사용하여 gophersat를 호출할 수 있습니다.
gophersat --verbose file.wcnf
여기서 --verbose 해석 프로세스 중에 솔버가 정보를 표시하도록 하는 선택적 매개변수입니다. 파일은 (WCNF 형식)[http://www.maxsat.udl.cat/08/index.php?disp=requirements]로 표현되어야 합니다.
Boolean Satisfiability Problem(부울 만족성 문제)을 의미하는 SAT는 표준 NP-완전 문제, 즉 최악의 경우 기하급수적인 시간이 걸리지 않는 알려진 해결책이 없는 문제입니다. 간단히 말해서, SAT 해결사는 주어진 명제 공식에 대해 이를 참으로 만드는 모든 변수에 대한 할당(해당 할당이 존재하는 경우)을 찾으려고 시도합니다.
단순한 알고리즘을 사용하여 SAT 솔버를 구현하는 것은 쉽지 않지만 실제로는 이러한 구현이 매우 비효율적입니다. Gophersat은 최첨단 기능을 구현하므로 매우 효율적이므로 효율적인 추론 엔진이 필요한 Go 프로그램에서 실제로 사용할 수 있습니다.
이것이 실제적인 이유로 항상 최선의 결정은 아니지만, 모든 NP-완전 문제는 SAT 문제로 변환되어 Gophersat에 의해 해결될 수 있습니다. 이러한 문제에는 여행하는 외판원 문제, 제약 프로그래밍, 배낭 문제, 계획, 모델 확인, 소프트웨어 정확성 확인 등이 포함됩니다.
SAT 문제에 대한 자세한 내용은 SAT에 관한 Wikipedia의 기사에서 찾을 수 있습니다.
또한 "초보자를 위한 SAT" 튜토리얼에서 gophersat에서 사용할 수 있도록 자신만의 부울 공식을 표현하는 방법에 대한 정보를 찾을 수 있습니다.
MAXSAT는 SAT 결정 문제와 동등한 최적화입니다. 순수 SAT 솔버는 모든 조항을 만족하는 모델을 반환하거나 그러한 모델이 없는 경우 UNSAT를 반환하는 반면, MAXSAT 솔버는 가능한 한 많은 조항을 충족하는 모델을 반환합니다.
MAXSAT에는 확장 기능이 있습니다.
부분 MAXSAT는 가능한 한 많은 조항을 충족하려고 하지만 일부 조항( 하드 조항 이라고 함)은 무슨 일이 있어도 충족 되어야 함을 의미합니다. 따라서 부분적인 MAXSAT 문제는 만족스럽지 못한 것으로 선언될 수 있습니다.
예를 들어, 학교의 시간표를 생성하는 것은 부분적인 MAXSAT 문제입니다. 소프트(예를 들어 오후 4시 이후에 시작하는 수업을 가능한 한 적게 갖고 싶음)와 하드(두 교사가 학교의 서로 다른 두 장소에 있을 수 없음)가 모두 있습니다. 동시에) 제약이 있습니다.
Weighted MAXSAT는 조항이 비용과 연관되어 있음을 의미합니다. 선택 사항이지만 일부 조항은 다른 조항보다 더 중요한 것으로 간주됩니다. 예를 들어, 조항 C1의 비용이 3이고 조항 C2와 C3의 비용이 모두 1인 경우 C1을 충족하지만 C2나 C3 모두 충족하지 않는 솔루션은 C2와 C3을 모두 충족하지만 C1은 충족하지 않는 솔루션보다 나은 것으로 간주됩니다. 평등한 것.
부분 가중 MAXSAT는 문제에 소프트 절과 하드 절이 모두 있고 소프트 절에 가중치가 부여됨을 의미합니다. 이와 관련하여 "순수한" MAXSAT는 보다 일반적인 부분 가중 MAXSAT의 특별한 경우입니다. "순수한" MAXSAT 문제는 모든 절이 가중치 1과 연관된 소프트 절인 부분 가중 MAXSAT 문제입니다.
의사 부울 문제는 어떤 면에서 SAT 문제를 일반화한 것입니다. 모든 명제 절은 단일 의사 부울 제약 조건으로 작성될 수 있지만 의사 부울 제약 조건을 표현하려면 기하급수적인 수의 명제 절이 필요할 수 있습니다.
(선형) 의사 부울 표현식은 다음과 같은 표현식입니다.
w1 l1 + w2 x2 + ... + wn xn ≥ y
여기서 y 와 모든 wi 정수 상수이고 모든 li 부울 리터럴입니다.
예를 들어, 다음 표현식이 참이 되려면
2 ¬x1 + x2 + x3 ≥ 3
부울 변수 x1 false여야 하며 x2 와 x3 중 적어도 하나는 true여야 합니다. 이는 명제 공식과 동일합니다.
¬x1 ∧ (x2 ∨ x3)
의사 부울 표현식은 명제 조항을 일반화한 것입니다.
x1 ∨ x2 ∨ ... ∨ xn
다음과 같이 다시 작성할 수 있습니다.
x1 + x2 + ... + xn ≥ 1
의사 부울 문제에 대한 설명은 명제 대응 문제보다 기하급수적으로 작을 수 있지만 의사 부울 문제를 해결하는 것은 여전히 NP-완전합니다.
Gophersat은 의사결정 문제(문제에 대한 해결책이 있습니까?)와 최적화 문제를 모두 해결합니다. 최적화 문제는 비용 함수, 즉 최소화해야 하는 항의 합과 관련된 의사 부울 문제입니다. Gophersat은 단순히 주어진 제약 조건을 충족하는 모델을 찾는 대신 제약 조건을 충족하고 비용 함수를 최소화하는 것이 보장되는 모델을 찾으려고 노력합니다.
최적의 솔루션을 검색하는 동안 gophersat는 차선책 솔루션(즉, 모든 제약 조건을 해결하지만 아직 최적이라고 보장되지 않는 솔루션)을 찾자마자 즉시 제공하므로 사용자는 주어진 시간에 차선책 솔루션을 얻을 수 있습니다. 보장된 최적의 솔루션을 제한하거나 더 오래 기다리십시오.
예, 아니오. 이는 순진한 구현보다 훨씬 빠르며 실제 문제에 사용할 수 있을 만큼 빠르지만, 고도로 최적화된 최상위 수준의 최첨단 솔버보다는 느립니다.
Gophersat은 가장 빠른 SAT/PB 솔버를 목표로 하지 않습니다. 목표는 다른 언어(일반적으로 C/C++)로 작성된 솔버에 대한 인터페이스에 의존하지 않고 고퍼에게 SAT 및 PB 기술에 대한 액세스를 제공하는 것입니다.
그러나 어떤 경우에는 다른 언어로 작성된 솔버와 인터페이스하는 것이 애플리케이션에 가장 적합한 선택입니다. 해결해야 할 작은 문제가 많다면 Gophersat이 가장 빠른 대안이 될 것입니다. 더 큰 문제의 경우 해결 시간을 희생하면서 가능한 한 적은 종속성을 갖고 싶다면 Gophersat도 좋습니다. 어려운 문제를 해결해야 하고 cgo나 외부 프로그램 사용에 개의치 않는다면 Gophersat는 아마도 최선의 선택이 아닐 것입니다.
Go에는 주로 go-sat과 gini와 같은 몇 가지 다른 SAT 해결사가 있습니다. 우리가 실행한 테스트에 따르면 Gini의 성능은 Gophersat과 거의 비슷하지만 평균적으로 약간 느립니다.
Gophersat은 또한 다른 솔버에서는 항상 사용할 수 없는 멋진 기능(예: 사용자 친화적인 입력 형식)을 제공하므로 쉽게 SAT/PB로 축소할 수 있는 NP 하드 문제를 설명하고 해결하는 도구로 사용할 수 있습니다. 문제.
아니요. bf ("부울 공식") 패키지는 모든 부울 공식을 CNF로 변환하는 기능을 제공합니다.
이것을 모델 카운팅이라고 합니다. 그렇습니다. 이를 위한 함수인 solver.Solver.CountModels 가 있습니다.
명령줄에서 모델 수를 계산할 수도 있습니다.
gophersat --count filename
여기서 파일 이름은 .opb 또는 .cnf 파일일 수 있습니다.
