SMT 솔버의 한계

Question

전통적으로 계산 논리를 사용한 대부분의 작업은 명제였습니다.이 경우 SAT (부울 만족 한계) 솔버 또는 1 차 정리를 사용했습니다.이 경우 1 차 정리 해설자를 사용했습니다.

근년에는 산술 이론과 함께 명제 논리를 기본적으로 강화하는 SMT (satisfiability modulo theory) 솔버에 대한 많은 진전이있었습니다. SRI 인터내셔널의 존 러시 비 (John Rushby)는 지금까지도 파괴적인 기술이라고 부릅니다.

1 차 로직에서 처리 할 수 ​​있지만 여전히 SMT가 처리 할 수없는 가장 중요한 실제 사례는 무엇입니까? 무엇보다 소프트웨어 검증 영역에서 SMT가 처리 할 수없는 문제는 무엇입니까?

Answer 1

SMT 솔버는 SAT 해결사보다 강력하지 않습니다. 그들은 여전히 ​​SAT에서 똑같은 문제에 대해 기하 급수적으로 실행되거나 불완전 할 것입니다. SMT의 장점은 SMT에서 명백한 많은 것들이 동일한 토 솔버가 재발견되는 데 오랜 시간이 걸릴 수 있다는 것입니다.

예를 들어 소프트웨어 검증의 경우, QF BV (수량 벡터없는 비트 이론) SMT 솔버를 사용하면 SMT 솔버는 단어에 (a + b = b + a) 레벨 대신에 SAT 솔버가 개별적인 불리언 값을 사용하는 것을 증명하는 데 정말로 오랜 시간이 걸릴 수 있습니다.

소프트웨어 검증이 필요하므로 소프트웨어 검증에서 SMT 또는 SAT 솔버가 어려울 수 있습니다.

먼저 QF BV에서 루프를 풀어야합니다. 즉, 솔버가 확인하는 것을 실질적으로 제한해야한다는 것을 의미합니다. 한정 기호가 허용되면 NPP가 아닌 PSPACE 완전 문제가됩니다.

둘째로, 일반적으로 어려운 것으로 간주되는 문제는 QF BV에서 인코딩하기 쉽습니다. 예를 들어, 다음과 같이 프로그램을 작성할 수 있습니다

void run(int64_t a,int64_t b) 
{ 
    a * b == <some large semiprime>; 

    assert (false); 
} 

지금은 물론 쉽게 주장을 입증 할 SMT 솔버 (false)를 발생하지만, 당신이를 줄 것이다, 카운터 예제를 제공해야합니다 입력 a,b. <some large number>을 RSA 반이 립으로 설정하면 곱셈을 뒤집습니다. 그렇지 않으면 정수 분해 (integer factorization)라고합니다! 따라서 이것은 SMT 솔버에게는 어려울 것이며, 소프트웨어 검증은 일반적으로 어려운 문제 (P = NP 또는 적어도 정수 분해가 쉽게되지 않는 한)임을 입증합니다. 이러한 SMT 솔버는 SAT 솔버에서 쉽게 쓰기가 쉽고 이유가있는 언어로 드레싱하는 것입니다.

고급 이론을 해결하는 SMT 솔버는 더 어려운 문제를 해결하려고하기 때문에 SAT 솔버보다 불완전하거나 더 느립니다.

은 참조 :

• 흥미롭게도, Beaver SMT solver가 CNF에 QF BV를 번역하고 백엔드 같은 SAT 해결사를 사용할 수 있습니다.
• KleeLLVM IR (중간 표현)으로 컴파일 된 프로그램을 사용할 수 있으며 버그를 확인하고 표식에 대한 카운터 예제를 찾습니다. 버그를 발견하면 정답에 반하는 예제를 제공 할 수 있습니다. 버그를 재현 할 수있는 정보를 입력하십시오.)