0
Z3py를 처음 사용하면서 과제 (sat 및 unsat)에 대한 카운터 예제를 생성했습니다.
unsat 솔루션에 대한 반례를 생성하는 함수가 있습니까?z3py의 일부 Implies 조건에서 부울 수식 증명
A
답변
0
unsat은 제공된 어설 션을 만족하는 모델이 없음을 의미합니다. 문제가 sat 일 때만 모델을 추출 할 수 있습니다. 따라서 질문에 대답 할 때 unsat 솔루션에서 모델을 만들 수는 없습니다. 단지 존재하지 않습니다.
일반적인 접근 방식은 입증하려는 수식의 negation을 어설 션하는 것입니다. 그 수식이 만족 스럽다면 원래 수식이 위조 될 수 있습니다. 즉, 이에 대한 반례가있다. 아마도 그게 당신이하려는 것일까요? 즉, 수식의 부정이 만족스러운 모델을 갖는 경우 해당 모델은 원래 수식의 반대 사례입니다. SMT 솔버의 가장 위에 구축 된 대부분의 프로 버가 어떻게 증명하려고하는지 부정한 것을 보냄으로써 unsat.이 반환됩니다. 피 인증자가 모델을 반환하면 반증입니다.