z3의 메모리 사용

선형 하이브리드 오토 마톤의 연결 가능성 문제를 해결하기 위해 z3을 사용하고 있습니다. 나는 제한된 환경에서 실험을한다. 나는 메모리 사용법에 대해 혼란 스럽다. 제한된 메모리에서 z3을 해결할 수있는 경우가 있습니다. 그러나 제한이 2000 인 경우 z3의 메모리 사용량이 최대 허용량을 초과합니다. 이유는 무엇입니까?z3의 메모리 사용

출처

2013-01-07 Dingbao Xie

자세한 내용을 입력하십시오. 이 문제를 일으키는 사례/문제는 무엇입니까? 그것에 대한 링크를 제공 할 수 있습니까? 그 경계를 어떻게 세웠습니까? API 또는 명령 줄 도구를 사용하고 있습니까? –

이 경우는 온도 제어 시스템 오토 마톤의 접근 가능성 분석입니다. 먼저 automata의 한정된 동작을 SMT 문제로 인코딩 한 다음 z3을 사용하여이를 해결합니다. 사실 2,500 이하의 오토마타에 대한 제약 조건의 수는 2000 년의 제약 조건보다 큽니다. 저는 z3을 명령 줄에 사용합니다 : 'z3 -st tcs_2000.smt2'. 바운드 2000 및 2500에서이 자동 장치에 대한 smt2 파일은 다음과 같습니다. http : //seg.nju.edu.cn/BACH/Demo/tcs_2000.smt2 http://seg.nju.edu.cn/BACH/Demo/tcs_2000 .smt2 –

SMT2 파일의 제약 조건 수가 적을수록 반드시 Z3이 문제를 해결하는 데 더 적은 메모리를 사용한다는 의미는 아닙니다. 예를 들어 작지만 만족스럽지 않은 문제는 큰 만족스러운 문제보다 훨씬 많은 메모리가 필요할 수 있습니다.

오토 마톤을 푸는 것에 대한 하한을 설정하면 만족스런 문제 (bound 2500)가 만족스럽지 않은 문제 (bound 2000)로 바뀌고 Z3에서 문제가 훨씬 더 어려워 질 수 있습니다 제약은 더 적지 만. 따라서 Z3은 더 많은 시간 및/또는 메모리를 사용합니다.

이 문제를 해결하려면 문제의 인코딩을 다르게하거나 해결 방법을 사용하여 더 쉽게 "행운의"길을 찾고 해결책을 더 빨리 찾을 수 있습니다.

출처

2013-01-07 16:56:52

답장을 보내 주셔서 감사합니다. 사실,이 오토 마톤은 도달 할 수 없습니다. bound 2500 아래의 automaton의 동작은 bound 2000 아래의 것을 포함합니다. 만족할 수없는 bounded model checking 문제에 대해, 더 작은 bound는 더 적은 해결 시간을 의미합니까? –

자주는 아니지만 항상 그렇습니다. 이것은 솔버의 휴리스틱에 크게 의존합니다. 그 차이가 얼마나 큰지 알 수 있습니까? –

예를 들어 문제 A는 a -> b, a 또는 b이고 큰 문제 B는 a -> b, b -> c, a 또는 b 또는 c입니다. –

z3의 메모리 사용

답변

관련 문제