Z3에서 증명 목표를 사용하여 사용 된 절 수를 줄입니다.

Question

저는 1 차 이론에 대한 사실을 증명하기 위해 Z3 사용을 최적화하는 실험을하고 있습니다. 현재, 파이썬에서 1 차 이론을 지정하고 그 안에 한정어를 사용하고 Z3에 대한 증명 목표의 부인과 함께 모든 절을 보냅니다. 나는 결과를 최적화 할 수 있기를 희망하는 다음과 같은 생각을 가지고 있습니다. 나는 Z3에 이론상의 수식을 관련 증명 목표에 보내기를 원합니다. 이 개념에 대해서는 자세히 이야기하지는 않겠지 만 직감은 간단하다고 생각합니다. 제 이론은 수식의 결합이며, 증명 목표의 진실 가치에 영향을 미칠 수있는 결합 만 보내고 싶습니다.

제 질문은 다음과 같습니다. 효율성 향상으로 이어질 수 있습니까, 아니면 Z3에서 이미 비슷한 방법을 사용하고 있습니까? 나는 Z3이 항상 마지막 주장이 증명 목표라고 가정하지 않기 때문에 나는 이것을 추측 할 수 없다. 그래서 그것을 최적화 할 방법이 없다.

Answer 1

예, 관련없는 사실을 제거하면 큰 차이가 발생할 수 있습니다. 우리가 F_1 and F_2 and (not G)이라는 만족할만한 공식을 가지고 있지 않다고 가정 해보십시오. 또한, F_1 and (not G)이 만족스럽지 않고 F_2이 만족 스럽다고 가정합시다. F_2은 부적절한 호출입니다. Z3으로 formulat을 보내기 전에 F_2을 제거 할 수있는 저렴한 방법이 있다면 큰 차이를 만들 수 있습니다.

Z3에는 관련없는 사실을 "무시"하는 추론이 있지만 단지 지능형입니다. 예를 들어, 최악의 시나리오는 Z33이 만족하기에 정말로 어려운 F_2입니다. Z3은 본질적으로 입력 공식을 만족하는 해석/솔루션을 만들려고합니다 (우리의 작업 예제에서는 F_1 an F_2 and (not G) 공식). Z3이 해석을 구축하는 것이 불가능할 때 수식은 만족스럽지 않습니다. 실제로, 수식 F_2은 만족할 만하다고 신속하게 나타낼 수 있고 F_2에 대한 해석/해법이 F_1 and (not G)과 충돌하지 않는 경우에만 Z3과 관련이 없습니다. 그렇지 않은 경우 Z3은 F_2으로 많은 리소스를 낭비 할 수 있습니다.