0
방정식 세트를 풀기 위해 z3py를 사용하고 있습니다. 어떻게 런타임 순서를 계산합니까? 선형 방정식 집합에서 만족되어야하는 bitvecs 변수가 있습니다. 설명서 및 안내서는 런타임을 계산하는 방법을 제공하지 않습니다.Z3 sat 솔버 런타임을 계산하는 방법
A
답변
1
시간 복잡도가 (최악)입니까? 그렇다면 좋은 대답을 얻을 수 없을 것이라고 생각합니다. 문제가 발생한 논리 (조합)에 따라 다릅니다. QF_BV 또는 UFNIA를 선택한 다음 솔버가 해당 논리 연산에 대해 구현하는 ((반) 결정) 절차를 수행합니다.
Z3 저자 (https://github.com/Z3Prover/z3/wiki/Publications)의 자료를 살펴보십시오. 일부 세부 정보를 제공 할 수도 있습니다.