Z3 결과의 임의성

Question

필자가 연구 도구의 일부로 Z3 Python 인터페이스를 사용하고 있으며 동일한 쿼리에서 Z3 해석기를 반복적으로 실행할 때 매우 이상한 동작을 발견했습니다. 특히 달리기 전에 명시 적으로 솔버를 재설정하더라도 매번 같은 결과를 얻지는 않습니다.

import z3 

with open("query.smt", "r") as smt_reader: 
    query_lines = "".join(smt_reader.readlines()) 
    for i in xrange(3): 
     solver = z3.Solver() 
     solver.reset() 

     queryExpr = z3.parse_smt2_string(query_lines) 
     equivalences = queryExpr.children()[:-1] 
     for equivalence in equivalences: 
      solver.add(equivalence) 

     # Obtain the Boolean variables associated with the constraints. 
     constraintVars = [equivalence.children()[0] for equivalence 
          in equivalences] 
     # Check the satisfiability of the query. 
     querySatResult = solver.check(*constraintVars) 

     print solver.model().sexpr() 
     print solver.statistics() 
     print "" 

위의 코드 Z3 해결사 세 번 다시는-만들고 동일한 쿼리의 satisfiability을 확인 : 참고로, 여기 내 코드입니다. 쿼리는 located here입니다.

위의 코드 섹션은 Z3 Python 인터페이스를 사용하는 방법과 정확히 일치하지 않지만 Z3 솔버는 동일한 쿼리의 코드 지점에서 두 번 호출 될 때 서로 다른 결과를 나타냅니다 결과. 이것이 의도적인지 궁금해하고 있었고, 이것을 불가능하게 만들거나 결정론을 보장 할 방법이 있는지 궁금해하고있었습니다.

Answer 1

나는 다른 모델을 의미한다고 가정하고 있습니다. 결과가 sat에서 unsat로 변경되면 버그입니다.

즉, 동일한 실행 경로에서 동일한 문제를 두 번 해결하면 Z3이 다른 모델을 생성 할 수 있습니다. Z3은 내부 고유 ID를 표현식에 지정합니다. 내부 ID는 Z3에서 사용되는 일부 휴리스틱 스에서 연결을 끊는 데 사용됩니다. 프로그램의 루프가 표현식을 작성/삭제하고 있음에 유의하십시오. 따라서 각 반복에서 제약 조건을 나타내는 식의 내부 ID가 다를 수 있으며 결과적으로 솔루션이 다른 솔루션을 생성 할 수 있습니다.

이

• Z3 timing variation