ctx-solver-simplify의 비대칭 성 동작

Question

https://git01.codeplex.com/z3 (89c1785b)의 마스터 브랜치에서 Z3의 최신 버전을 사용하여 매개 변수의 순서가 중요한 것으로 보이는 ctx-solver-simplify에서 다소 놀라운 결과가 나타납니다.) :

#!/usr/bin/python 
import z3 

a, b = z3.Bools('a b') 
p = z3.Not(a) 
q = z3.Or(a, b) 
for e in z3.And(p, q), z3.And(q, p): 
    print e, '->', z3.Tactic('ctx-solver-simplify')(e) 

가 생성됩니다

And(Not(a), Or(a, b)) -> [[Not(a), Or(a, b)]] 
And(Or(a, b), Not(a)) -> [[b, Not(a)]] 

이 Z3의 버그인가?

Answer 1

아니요, 이것은 버그가 아닙니다. 전술 ctx-solver-simplify은 매우 비싸고 본질적으로 비대칭입니다. 즉, 하위 수식이 방문한 순서가 최종 결과에 영향을줍니다. 이 전략은 src/smt/tactic/ctx_solver_simplify_tactic.cpp 파일에 구현됩니다. 코드는 아주 읽기 쉽습니다. "SMT"솔버 (m_solver)를 사용하고 입력 공식을 탐색하면서 m_solver.check()을 여러 번 호출합니다. 이 통화들 각각은 상당히 비쌀 수 있습니다. 특정 문제 도메인의 경우, 우리는이 전략의 버전을 훨씬 더 비싸게 구현할 수 있으며 질문에 설명 된 비대칭 성을 피할 수 있습니다.

편집 :

또한 전술 ctx-simplify을 고려할 수 있습니다, 그것은 ctx-solver-simplify보다 저렴하지만 대칭이다. F[A]가 A을 포함 할 수있는 공식이다

A \/ F[A] ==> A \/ F[false] 
x != c \/ F[x] ==> F[c] 

: ctx-simplify 것 전술은 기본적으로 다음과 같은 규칙을 적용합니다. 수식을 횡단 할 때 SMT 솔버를 호출하지 않기 때문에 ctx-solver-simplify보다 저렴합니다. 여기에 (online도 가능)이 전술을 사용하는 예입니다 : 어떤 전술을 구현할 때

humand - 가독성에 관한

a, b = Bools('a b') 
p = Not(a) 
q = Or(a, b) 
c = Bool('c') 
t = Then('simplify', 'propagate-values', 'ctx-simplify') 
for e in Or(c, And(p, q)), Or(c, And(q, p)): 
    print e, '->', t(e) 

, 이것은 목표 결코 없었다. 위의 전술이 귀하의 목적에 부적합한 지 알려주십시오.

Answer 2

본질적으로 표준화를 요구할 때 기타 트레이드 오프가 있기 때문에 사용자 지정 전략을 작성하는 것이 더 좋을 것이라고 생각합니다. Z3에는 수식을 표준 형식으로 변환하는 방법이 없습니다. 따라서 수식에 대해 동일한 답을 항상 생성하는 무언가가 필요하다면 이이를 보장하는 새로운 표준화자를 작성해야합니다.

또한 ctx_solver_simplify_tactic은 수식을 단순화 할 때 약간의 단점을 만듭니다. 동일한 하위 수식을 여러 번 단순화하지 않아도됩니다. 그럴 경우 결과식의 크기가 크게 (기하 급수적으로) 증가 할 수 있습니다.