만족도 모듈로 이론

컴퓨터 과학과 수학 논리학에서 만족도 모듈로 이론(SMT)은 수학적 공식의 만족 여부를 결정하는 문제다.그것은 실제 숫자, 정수 및/또는 목록, 배열, 비트 벡터 및 문자열과 같은 다양한 데이터 구조를 포함하는 더 복잡한 공식에 부울 만족도 문제(SAT)를 일반화한다.이러한 표현들이 평등한(종종 정량자를 허용하지 않는) 1차 논리학에서 일정한 형식 이론 내에서 해석된다는 사실에서 유래한 이름이다.SMT 솔루션이란 입력의 실질적인 부분 집합에 대한 SMT 문제를 해결하는 것을 목적으로 하는 툴이다.Z3와 CVC4와 같은 SMT 해결사는 자동화된 정리 증명, 프로그램 분석, 프로그램 검증, 소프트웨어 테스트 등 컴퓨터 과학 전반에 걸쳐 광범위한 응용 프로그램의 구성 요소로 사용되어 왔다.

Boolean 만족도는 이미 NP-complete이기 때문에 SMT 문제는 일반적으로 NP-hard이며, 많은 이론의 경우 불찰할 수 없다.연구자들은 어떤 이론이나 이론의 하위 집합이 해독 가능한 시만텍 문제와 해독 가능한 사례의 계산적 복잡성으로 이어지는지를 연구한다.결과적인 의사결정 절차는 종종 시만텍 해결사에서 직접 구현된다. 예를 들어 프레스버거 산술의 결정성을 참조한다.SMT는 제약조건 만족도 문제, 따라서 제약조건 프로그래밍에 대한 어떤 정형화된 접근법이라고 생각할 수 있다.

기본 용어

정식으로 말하면, SMT 인스턴스는 1차 로직의 공식으로, 일부 함수와 술어 기호에는 추가적인 해석이 있으며, SMT는 그러한 공식의 만족 여부를 판단하는 문제다.즉, 적절한 비이진 변수 집합에 대해 이진 변수 중 일부가 술어로 대체되는 부울 만족도 문제(SAT)의 예를 상상해 보십시오.술어는 비이항 변수의 이항 값 함수다.Example predicates include linear inequalities (e.g., $3x+2y-z\geq 4$ ) or equalities involving uninterpreted terms and function symbols (e.g., $f(f(u,v),v)=f(u,v)$ where $f$ is some unspecified function of two arguments).이들 술어는 할당된 각각의 이론에 따라 분류된다.예를 들어, 실제 변수에 대한 선형 불평등은 선형실제산술 이론의 규칙을 사용하여 평가되는 반면, 해석되지 않은 용어와 함수 기호를 포함하는 술어는 동등하게 해석되지 않은 함수 이론의 규칙을 사용하여 평가된다(때로는 빈 이론이라고도 한다).다른 이론으로는 배열과 목록 구조의 이론(컴퓨터 프로그램 모델링 및 검증에 유용함)과 비트 벡터 이론(하드웨어 설계 모델링 및 검증에 유용함)이 있다.하위 이론도 가능하다: 예를 들어 차이 논리는 $변수$ x $x$ 과 $x$ y $y$ 에 $x-y>c$ $y$ 대해 각 불평등이 $x-y>c$ - y $x-y>c$ > $x-y>c$ $x-y$ 의 형식과 상수 $c$ $c$ 을 갖는 선형 산술의 하위 이론이다 $c$

대부분의 시만텍 솔루션에서는 로직의 정량화되지 않은 부분만 지원한다.

표현력

SMT 인스턴스는 다양한 기본 이론의 술어로 다양한 변수 집합이 대체되는 부울 SAT 인스턴스의 일반화다.SMT 공식은 부울 SAT 공식보다 훨씬 풍부한 모델링 언어를 제공한다.예를 들어, 시만텍 공식은 마이크로프로세서의 데이터패스 작동을 비트 레벨이 아닌 단어로 모델링할 수 있게 해준다.

그에 비해, 해답 집합 프로그래밍은 술어(더 정확히 말하면, 원자 공식에서 생성된 원자 문장에 기초한다)에 기초하기도 한다.SMT와 달리, 응답 프로그램에는 정량자가 없으며, 선형 산술이나 차이 논리 같은 제약조건을 쉽게 표현할 수 없다.ASP는 기껏해야 해석되지 않은 함수의 자유 이론으로 축소되는 부울 문제에 적합하다.32비트 정수를 ASP에서 비트 벡터로 구현하는 것은 초기 SMT 해결사들이 직면했던 것과 거의 동일한 문제들로 인해 어려움을 겪고 있다: x+y=y+x와 같은 "확실한" 정체성은 추론하기 어렵다.

제약조건 논리 프로그래밍은 선형 산술적 제약조건에 대한 지원을 제공하지만 완전히 다른 이론적 프레임워크 내에서 제공한다.^{[citation needed]}시만텍 해결사들도 고차 논리로 수식을 풀 수 있도록 확장했다.^[1]

해결사가 접근하다

SMT 인스턴스를 해결하기 위한 초기 시도에는 이를 Boolean SAT 인스턴스로 변환(예: 32비트 정수 변수는 적절한 가중치를 가진 32개의 단일 비트 변수로 인코딩되며, 'plus'와 같은 워드 레벨 연산은 비트의 하위 레벨 로직 연산으로 대체됨) 및 이 공식을 Boolean SAT 해결사에게 전달하는 작업이 포함되었다.열성적인 접근방식이라고 불리는 이 접근방식은 SMT 공식을 동등한 부울 SAT 공식으로 사전 처리함으로써 기존 부울 SAT 해결기를 "있는 그대로" 사용할 수 있으며, 시간이 지남에 따라 성능과 용량 향상이 활용된다는 장점이 있다.한편, 기초 이론의 높은 수준의 의미론의 상실은 부울 SAT 해결사가 "의견적인" 사실들을 발견하기 위해 필요 이상으로 훨씬 더 열심히 일해야 한다는 것을 의미한다(정수 덧셈을 $x+y=y+x$ $x+y=y+x$ x + $x+y=y+x$ = $x+y=y+x$ + $x+y=y+x$ + x ${\displaystyle$ x $+y=y+x}$ 등).이러한 관찰을 통해 DPLL식 검색의 부울 추론을 특정 이론의 술어 접속사(AND)를 취급하는 이론별 해결사(T-솔버)와 긴밀하게 통합하는 다수의 SMT 해결사가 개발되었다.이 접근법을 게으른 접근법이라고 한다.

DPLL(T)로 불리는 ^[2]이 아키텍처는 잘 정의된 인터페이스를 통해 이론 T를 위한 해결사와 상호작용하는 DPLL 기반 SAT 해결사에게 부울 추론의 책임을 부여한다.이론 해결사는 공식의 부울 검색 공간을 탐색하면서 SAT 해결사로부터 이론 술어의 접속사 타당성을 확인하는 것에 대해서만 걱정하면 된다.그러나 이러한 통합이 잘 작동하기 위해서는 이론 해결자가 전파와 갈등 분석에 참여할 수 있어야 하며, 즉 이미 확립된 사실로부터 새로운 사실을 유추할 수 있어야 하며, 이론 갈등이 발생했을 때 실현 불가능에 대한 간결한 설명을 제공할 수 있어야 한다.즉, 이론 해결자는 증분적이고 역추적이 가능해야 한다.

인식할 수 없는 이론에 대한 SMT

대부분의 일반적인 SMT 접근법은 해독 가능한 이론을 지원한다.그러나 많은 실제 시스템은 예를 들어 항공기 및 그 거동과 같은 초월적 기능을 포함하는 실제 숫자에 대한 비선형 산술만을 사용하여 모델링할 수 있다.이러한 사실은 시만텍 문제를 비선형 이론으로 확장시키는 동기를 부여한다. 예를 들어, 시만텍 문제를 비선형 이론으로 확장시키는 동기를 부여한다.

{\b\beve}&(\sin(x)^{3}=\cos(\log(y)\cdot x)\ve b\ve -x^{2}\geq 2.3y)\reft \reft(\neg b\vee y<-34).4\vee \exp(x)}{y \over x}\오른쪽)\end{array}}

어디에

b\in {\mathb {B}},x,y\in {\mathb {R}}}}

만족스럽다그러면 그러한 문제들은 일반적으로 해석할 수 없는 문제가 된다.(실제 폐쇄장 이론, 따라서 실수의 완전한 첫 번째 순서 이론은 정량자 제거를 사용하여 해석할 수 없다.이것은 알프레드 타르스키 덕분이다.)프레스버거 산술이라 불리는 덧셈이 있는 자연수의 제1순서 이론도 해독할 수 있다.상수에 의한 곱셈은 내포된 덧셈으로 구현할 수 있기 때문에, 많은 컴퓨터 프로그램의 산술은 Presburger 산술로 표현할 수 있어, 해독 가능한 공식이 된다.

SMT사용 풀 사람들의 예는 결정할 수 없는 연산 이론들은 reals에 이론의 원자로 불 조합을 찾는 건 ABsolver,[3]는( 불가피하게 불완전한)부하 이론으로 비선형적 최적화 패킷 해결사, 그리고 iSAT과, DPLL SAT-solving의 통일과 시간 간격으로 만들기 위해 고전 DPLL(T)건축을 해소했다. 사기iSAT 알고리즘이라 불리는 지속적 전파.^[4]

해결사

아래 표에는 많은 시만텍 해결사의 기능이 요약되어 있다."SMT-LIB" 열은 SMT-LIB 언어와의 호환성을 나타내며, '예'로 표시된 많은 시스템은 이전 버전의 SMT-LIB만 지원하거나 부분적으로만 지원할 수 있다.열 "CVC"는 CVC 언어에 대한 지원을 나타낸다.DIMACS 열은 DIMACS 형식에 대한 지원을 나타낸다.

프로젝트는 특징과 성능뿐만 아니라 주변 커뮤니티의 생존 가능성, 프로젝트에 대한 지속적인 관심, 문서화, 수정, 테스트 및 개선사항에 기여하는 능력에서도 차이가 있다.

플랫폼			특징들						메모들
이름	OS	면허증	SMT-LIB	CVC	디맥스	빌트인	API	SMT-COMP [1]
AB솔버	리눅스	CPL	v1.2	아니요.	네	선형 산술, 비선형 산술	C++	아니요.	DPLL 기반
알트 에르고	Linux, Mac OS, Windows	CeCIL-C(LGPL과 상당히 동등한)	부분 v1.2 및 v2.0	아니요.	아니요.	빈 이론, 선형 정수 및 합리적인 산술, 비선형 산술, 다형 배열, 열거된 데이터 유형, AC 기호, 비트벡터, 레코드 데이터 유형, 정량자	OCAML	2008	폴리모픽 1차 입력 언어 a la ML, SAT-솔버 기반 넬슨-오펜은 모듈로 이론을 추론하기 위한 접근법처럼 Shostak와 Nelson-Open을 조합한다.
바르셀로그어	리눅스	소유권	v1.2			빈 이론, 차이 논리	C++	2009	DPLL 기반, 결합형 폐쇄
비버	Linux, Windows	BSD	v1.2	아니요.	아니요.	비트 벡터	OCAML	2009	SAT-솔버 기반
불렉터	리눅스	MIT	v1.2	아니요.	아니요.	비트 벡터, 배열	C	2009	SAT-솔버 기반
CVC3	리눅스	BSD	v1.2	네		빈 이론, 선형 산술, 배열, 튜플, 유형, 레코드, 비트벡터, 정량자	C/C++	2010	HOL에 대한 교정 출력물
CVC4	Linux, Mac OS, Windows, FreeBSD	BSD	네	네		합리적 및 정수 선형 산술, 배열, 튜플, 레코드, 귀납적 데이터 유형, 비트 벡터, 문자열 및 해석되지 않은 함수 기호에 대한 동등성	C++	2010	버전 1.5 2017년 7월 출시
의사 결정 절차 툴킷(DPT)	리눅스	아파치	아니요.				OCAML	아니요.	DPLL 기반
iSAT	리눅스	소유권	아니요.			비선형 산술		아니요.	DPLL 기반
수학SAT	Linux, Mac OS, Windows	소유권	네		네	빈 이론, 선형 산술, 비선형 산술, 비트 벡터, 배열	C/C++, Python, Java	2010	DPLL 기반
미니Smt	리눅스	LGPL	부분 v2.0			비선형 산술		2010	SAT-솔버 기반, Yys 기반
Norn									문자열 제약 조건을 위한 SMT 해결사
오픈코그	리눅스	AGPL	아니요.	아니요.	아니요.	확률론적 논리, 산술적 논리관계형 모델	C++, Scheme, Python	아니요.	부표상 이형성
오픈SMT	Linux, Mac OS, Windows	GPLv3	부분 v2.0		네	빈 이론, 차이, 선형 산술, 비트 벡터	C++	2011	게으른 SMT솔버
raSAT	리눅스	GPLv3	v2.0			실제와 정수 비선형 산술		2014, 2015	시험과 중간값 정리를 통한 구간 구속조건 전파의 확장
새틴	?	소유권	v1.2			선형 산술, 차이 논리	없는	2009
SMTInterpoll	Linux, Mac OS, Windows	LGPLv3	v2.5			해석되지 않은 함수, 선형 실제 산술 및 선형 정수 산술	자바	2012	고품질의 소형 보간물을 생산하는 데 초점을 맞춘다.
SMCHR	Linux, Mac OS, Windows	GPLv3	아니요.	아니요.	아니요.	선형 산술, 비선형 산술, 힙스	C	아니요.	제약 처리 규칙을 사용하여 새로운 이론을 구현할 수 있다.
SMT-RAT	Linux, Mac OS	MIT	v2.0	아니요.	아니요.	선형 산술, 비선형 산술	C++	2015	시만텍 호환 구현 모음으로 구성된 전략적 및 병렬 시만텍 해결을 위한 툴박스.
소놀랄라	Linux, Windows	소유권	부분 v2.0			비트 벡터	C	2010	SAT-솔버 기반
창	Linux, Mac OS, Windows	소유권	v1.2			비트 벡터		2008
STP	Linux, OpenBSD, Windows, Mac OS	MIT	부분 v2.0	네	아니요.	비트 벡터, 배열	C, C++, Python, OCaml, Java	2011	SAT-솔버 기반
검	리눅스	소유권	v1.2			비트 벡터		2009
UCLID	리눅스	BSD	아니요.	아니요.	아니요.	빈 이론, 선형 산술, 비트 벡터 및 제한된 람다(수치, 메모리, 캐시 등)		아니요.	SAT-솔버 기반, 모스크바 ML로 작성. 입력 언어는 SMV 모델 체커다.잘 문서화되었다!
veriT	Linux, OS X	BSD	부분 v2.0			해석되지 않은 함수 기호에 대한 빈 이론, 합리적 및 정수 선형 산술, 정량자 및 동등성	C/C++	2010	SAT-솔버 기반
예스	Linux, Mac OS, Windows, FreeBSD	GPLv3	v2.0	아니요.	네	해석되지 않은 함수 기호에 대한 합리적 및 정수 선형 산술, 비트 벡터, 배열 및 동등성	C	2014	온라인에서 소스 코드를 사용할 수 있음
Z3 정리 프로베라	Linux, Mac OS, Windows, FreeBSD	MIT	v2.0		네	빈 이론, 선형 산술, 비선형 산술, 비트 벡터, 배열, 데이터 유형, 정량자, 문자열	C/C++, .NET, OCaml, Python, Java, Haskell	2011	온라인에서 소스 코드를 사용할 수 있음

표준화와 SMT-COMP 해결사 경쟁

SMT 해결사(및 자동화된 정리 프로버, 흔히 동의어로 사용되는 용어)에 대한 표준화된 인터페이스를 설명하려는 여러 시도가 있다.가장 눈에 띄는 것은 ^{[citation needed]}S-expression을 기반으로 언어를 제공하는 SMT-LIB 표준이다.일반적으로 지원되는 다른 표준화된 형식은 많은 부울 SAT 솔버에 의해 지원되는 DIMACS^{[citation needed]} 형식과 CVC 자동 정리 프로베이어가 사용하는 CVC^{[citation needed]} 형식이다.

그 SMT-LIB 방식도 표준화된 벤치 마크의 수로 나누고 SMT사용 풀 사람들 SMT-COMP. 처음에는 경쟁의 검증 회의(CAV)[5][6]에서 2020년 경쟁은 SMT사용 워크숍은 인터 계열이다의 일환으로 개최된다 발생의 연간 경쟁 활성화되어 가진다.국가al 자동 추론 공동 회의(IJCAR).^[7]

적용들

시만텍 해결사는 프로그램의 정확성 입증, 상징적 실행을 기반으로 한 소프트웨어 테스트, 가능한 프로그램의 공간을 검색해 프로그램 조각을 생성하는 합성 등에 모두 유용하다.소프트웨어 검증 외에서는 SMT 솔버를 유형 추론^[8]^[9] 및 핵 무기 제어에 대한 행위자 신념 모델링 등 이론적 시나리오 모델링에도 사용하였다.^[10]

검증

시스템 프로그램의 시스템 지원 검증은 시만텍 해결사를 사용하는 경우가 많다.일반적인 기법은 전제조건, 자세, 루프 조건 및 주장을 SMT 공식으로 변환하여 모든 속성이 수용할 수 있는지 여부를 결정하는 것이다.

Z3 SMT 해결사 위에는 여러 검증기가 구축돼 있다.부기는 Z3를 이용해 간단한 명령어 프로그램을 자동으로 점검하는 중간 검증 언어다.동시 C를 위한 VCC 검증기는 필수 객체 기반 프로그램에는 Boogie, 동시 프로그램에는 Chalice, C#에 대해서는 Spec#을 사용하고 있다.F*는 증거를 찾기 위해 Z3를 사용하는 의존적으로 타이핑된 언어로서, 컴파일러는 이러한 증명들을 가지고 다니면서 증명-반송 바이트 코드를 만든다.Viper 검증 인프라는 검증 조건을 Z3에 인코딩한다.sbv 라이브러리는 해스켈 프로그램에 대한 시만텍 기반 검증을 제공하며, 사용자가 Z3, ABC, 부렉터, CVC4, MathSAT, Yys 등 다수의 해결사 중에서 선택할 수 있도록 한다.

Alt-Ego SMT 해결사 위에는 여러 검증기들이 구축되어 있다.다음은 성숙한 애플리케이션 목록:

연역 프로그램 검증을 위한 플랫폼인 Why3는 Alt-Ego를 주요 프로베러로 사용한다.
CEA에 의해 개발되고 에어버스에서 사용되는 C-검증기인 COVERAT; Alt-Ego는 최근 항공기 중 하나의 DO-178C 자격에 포함되었다.
C-코드를 분석하는 프레임워크인 Frama-C는 제시와 WP 플러그인의 Alt-Ego를 사용한다("고교 프로그램 검증" 전용).
SPAK는 2014년 SPAK의 일부 주장에 대한 검증을 자동화하기 위해 CVC4 및 Alt-Ego(GNATProve 후면)를 사용한다.
아틀리에-B는 메인 프로베러 대신 Alt-Ego를 사용할 수 있다(ANR Bware 프로젝트 벤치마크에서 84%에서 98%로 성공률 증가).
로댕은 시스테렐이 개발한 B-method 프레임워크로 Alt-Ego를 백엔드로 사용할 수 있다.
어레이 기반 전환 시스템의 안전 특성을 검증하기 위한 오픈 소스 모델 체커인 큐비클.
EasyCrypt, 대립 코드와의 확률론적 계산의 관계적 특성에 대한 추론을 위한 도구 모음입니다.

많은 SMT 해결사가 SMTLIB2라는 공통 인터페이스 형식을 구현(이러한 파일에는 대개 확장자가 ")..smt2"). LiquidHaskell 도구는 CVC4, MathSat 또는 Z3와 같은 SMTLIB2 호환 해결사를 사용할 수 있는 Haskell용 정제 유형 기반 검증기를 구현한다.

기호 실행 기반 분석 및 테스트

시만텍 해결사의 중요한 적용 분야는 특히 보안 취약점을 찾아내는 것을 목적으로 하는 프로그램의 분석 및 테스트(예: 콩쿨 테스트)를 위한 상징적 실행이다.^{[citation needed]}이 범주의 예로는 Microsoft Research, KLEE, S2E 및 Triton의 SAGE가 있다.심볼릭 실행 응용 프로그램에 사용된 SMT 솔버에는 Z3, 웨이백 머신에 STP Archived 2015-04-06, Z3str solvers 제품군 및 Boolector가 있다.^{[citation needed]}

참고 항목

메모들

^ 바르보사, 하니엘 외 "시만텍 해결사들을 고차원의 논리로 확장"국제자동공제회의.스프링거, 챔, 2019.
^ Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), "Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)", Journal of the ACM (PDF), vol. 53, pp. 937–977
^ Bauer, A.; Pister, M.; Tautschnig, M. (2007), "Tool-support for the analysis of hybrid systems and models", Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE'07), IEEE Computer Society, p. 1, CiteSeerX 10.1.1.323.6807, doi:10.1109/DATE.2007.364411, ISBN 978-3-9810801-2-4, S2CID 9159847
^ Fränzle, M.; Herde, C.; Ratschan, S.; Schubert, T.; Teige, T. (2007), "Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure", JSAT Special Issue on SAT/CP Integration (PDF), vol. 1, pp. 209–236
^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "SMT-COMP: Satisfiability Modulo Theories Competition". Computer Aided Verification. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 3576: 20–23. doi:10.1007/11513988_4. ISBN 978-3-540-31686-2.
^ Barrett, Clark; de Moura, Leonardo; Ranise, Silvio; Stump, Aaron; Tinelli, Cesare (2011). Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (eds.). "The SMT-LIB Initiative and the Rise of SMT". Hardware and Software: Verification and Testing. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 6504: 3. Bibcode:2011LNCS.6504....3B. doi:10.1007/978-3-642-19583-9_2. ISBN 978-3-642-19583-9.
^ "SMT-COMP 2020". SMT-COMP. Retrieved 2020-10-19.
^ Hassan, Mostafa; Urban, Caterina; Eilers, Marco; Müller, Peter (2018). "MaxSMT-Based Type Inference for Python 3". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 10982. pp. 12–19. doi:10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5.
^ 외톨이, 캘빈 등"유형추론 오류설명을 위한 실질적인 틀"ACM SIGPlan 공지사항 51.10 (2016): 781-799.
^ Beaumont, Paul; Evans, Neil; Huth, Michael; Plant, Tom (2015). Pernul, Günther; Y A Ryan, Peter; Weippl, Edgar (eds.). "Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks". Computer Security -- ESORICS 2015. Lecture Notes in Computer Science. Cham: Springer International Publishing. 9326: 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6.

참조

C Barrett, R Sebastiani, Seshia, C Tinelli, "만족성 모둘로 이론"만족도 핸드북에서는 인공지능 및 애플리케이션 분야의 프런티어 185권 (A Biere, M J H Heule, H van Maaren, T Walsh, eds.) IOS Press 2009년 2월 825–885쪽.
Vijay Ganesh (PhD.논문 2007), Bit-벡터, 배열 및 Integer, 컴퓨터 과학 부서, 스탠포드 대학교, 스탠포드, CA, 미국, 2007년 9월 의사 결정 절차
Susmit Jha, Rishikesh Limaye, Sanjit A.세샤.Beaver: 비트 벡터 산술에 효율적인 SMT 해결사 엔지니어링.컴퓨터 지원 검증에 관한 제21차 국제회의의 절차서, 페이지 668–674, 2009.
R. E. Bryant, S. M. 독일어 및 M. N. Vellev, 분석 표 및 관련 방법 페이지 1-13, 1999.에서 "해석되지 않은 기능의 동등성 논리에 대한 효율적인 의사결정 절차를 이용한 마이크로프로세서 검증".
M. Davis와 H. Putnam, 정량화 이론의 계산 절차, 컴퓨터 기계 협회 저널, 제7권, 제201권–215권, 1960.
M. Davis, G. Logemann, D.Loveland, ACM Provisioning, Communications of ACM, vol. 5, no. 7, 페이지 394–397, 1962.
D. 크로닝과 O.Strichman, Decision Procedures – 알고리즘적 관점(2008), Springer(이론적 컴퓨터 과학 시리즈) ISBN 978-3-540-74104-6.
G.J.남, K. A. 사칼라, R.Rutenbar, 검색 기반 부울 만족도, IEEE 통합 회로 및 시스템의 컴퓨터 지원 설계에 관한 새로운 FPGA 상세 라우팅 접근방식, 2002년 제21권, 제6권, 페이지 674–684.
SMT-LIB: 만족도 모듈로 이론 라이브러리
SMT-COMP: 만족도 모듈로 이론 경진대회
의사결정 절차 - 알고리즘적 관점
R. Sebastiani, 게으른 만족 모둘로 이론, Dipartimento di Ingegneria e Scienza 델'2007년 12월 이탈리아 트렌토 우니베르시타 디 트렌토, Informazione
D.유리체프, SAT/SMT 솔버에 대한 빠른 소개 및 상징적 실행

이 기사는 ACM SIGDA e-뉴스레터(E-Newsletter)의 한 칼럼에서 인용한 것이다. 카림 사칼라.원본 텍스트는 여기서 사용할 수 있음

[1] 바르보사, 하니엘 외 "시만텍 해결사들을 고차원의 논리로 확장"국제자동공제회의.스프링거, 챔, 2019.

[2] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), "Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)", Journal of the ACM (PDF), vol. 53, pp. 937–977

[3] Bauer, A.; Pister, M.; Tautschnig, M. (2007), "Tool-support for the analysis of hybrid systems and models", Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE'07), IEEE Computer Society, p. 1, CiteSeerX 10.1.1.323.6807, doi:10.1109/DATE.2007.364411, ISBN 978-3-9810801-2-4, S2CID 9159847

[4] Fränzle, M.; Herde, C.; Ratschan, S.; Schubert, T.; Teige, T. (2007), "Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure", JSAT Special Issue on SAT/CP Integration (PDF), vol. 1, pp. 209–236

[5] Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "SMT-COMP: Satisfiability Modulo Theories Competition". Computer Aided Verification. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 3576: 20–23. doi:10.1007/11513988_4. ISBN 978-3-540-31686-2.

[6] Barrett, Clark; de Moura, Leonardo; Ranise, Silvio; Stump, Aaron; Tinelli, Cesare (2011). Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (eds.). "The SMT-LIB Initiative and the Rise of SMT". Hardware and Software: Verification and Testing. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 6504: 3. Bibcode:2011LNCS.6504....3B. doi:10.1007/978-3-642-19583-9_2. ISBN 978-3-642-19583-9.

[7] "SMT-COMP 2020". SMT-COMP. Retrieved 2020-10-19.

[8] Hassan, Mostafa; Urban, Caterina; Eilers, Marco; Müller, Peter (2018). "MaxSMT-Based Type Inference for Python 3". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 10982. pp. 12–19. doi:10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5.

[9] 외톨이, 캘빈 등"유형추론 오류설명을 위한 실질적인 틀"ACM SIGPlan 공지사항 51.10 (2016): 781-799.

[10] Beaumont, Paul; Evans, Neil; Huth, Michael; Plant, Tom (2015). Pernul, Günther; Y A Ryan, Peter; Weippl, Edgar (eds.). "Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks". Computer Security -- ESORICS 2015. Lecture Notes in Computer Science. Cham: Springer International Publishing. 9326: 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6.

[1]

[2]

[4]

[7]

[8]

[9]

[10]

Search