Z3py : picosat에서 사용 조항에 Z3 공식을 변환

Question

링크 : 나는 SAT 해결사로 Z3를 사용했습니다
Z3 theorem prover
picosat with pyhton bindings

. 더 큰 수식의 경우 성능 문제가있는 것 같아서 피코사스가 더 빠른 대안인지 확인하려고했습니다.

from z3 import * 

import pycosat 
from pycosat import solve, itersolve 

# 
#1 2 3 4 5 6 7 8 (variable names in picosat are numbers!) 
# 
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B') 
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True)))) 

# formula in Z3: 
f = simplify(C) 

print f 

OUTPUT/RESULT Picosat 그러나 다음의 예와 같이 목록/숫자 배열을 사용

And(S, 
    Or(Not(S), P), 
    Or(Not(P), S), 
    Or(Not(P), B), 

    Or(Not(C), P), 
    Or(Not(G), P), 
    Or(Not(M), P), 
    Or(Not(R), P), 
    Or(Not(SN), P), 
    Or(Not(B), P)) 

("clauses1 : 기존 파이썬 코드 Z3 구문 명제 화학식 생성 ": 6은 변수 P를, -6은"P가 아닙니다 "를 의미합니다.

import pycosat 
from pycosat import solve, itersolve 
# 
# use pico sat 
# 
nvars = 8 
clauses =[ 
    [6], 
    [-6, 4], ## "Or(Not(S), P)" from OUPUT above 
    [-4, 6], 
    [-4, 8], 
    [-1, 4], 
    [-2, 4], 
    [-3, 4], 
    [-5, 4], 
    [-7, 4], 
    [-8, 4]] 

# 
# efficiently find all models of the formula 
# 
sols = list(itersolve(clauses, vars=nvars)) 
print "result:" 
print sols 
print "\n\n====\n" 

르 솔루션을 사용하여 CNF의 수식을 나타내는 Z3 변수 (코드 예제 에서처럼 "f"와 같이)를 CNF의 수식을 나타내는 데 사용되는 앞의 형식으로 변환합니다. 나는 Z3의 python API를 사용하려고 시도했지만, 문서로는 문제를 해결하기에 충분하지 않았습니다.

(단지 개념을 도시 상기 변수 C로 표시되는 화학식을 동적으로 생성 할 것이다. 예를 참고 직접 Z3에 의해 효율적으로 처리하기에 너무 복잡 할 것이다)

Answer 1

첫째, 우리는 Z3 수식 변환해야 CNF에 다음 포스트 주소이 문제

• Z3 and DIMACS output

, 우리는 그냥 통과하는 기능을 쓸 수 DIMACS에 Z3 CNF 공식을 변환하고 정수의 목록의 목록을 생성합니다. 다음 두 글은 당신이 값 표현에서지도를 필요로하는 경우, 마지막으로 Z3 공식

• Substituting function symbols in z3 formulas
• Is there a way of querying or accessing the structure of a Z3 expression via the API

을 통과하는 방법에 대해 설명합니다, 당신은 다음과 같은 방법을 사용할 수 있습니다

• Hashing expressions in Z3Python