Z3의 해결 전략을 제어하십시오.

Question

그래서 Z3에서 풀어야 할 큰 문제가 있다고 가정하고, 한 번에 해결하려고하면 너무 많은 시간이 걸릴 것입니다. 그래서 저는이 문제를 부분적으로 나누어서 개별적으로 풀어냅니다. 장난감 예를 들어 내 복잡한 문제가 그 3 개 방정식을 해결하는 것으로 가정 할 수 있습니다으로 :

eq1: x>5 
eq2: y<6 
eq3: x+y = 10 

그래서 제 질문은, 예를 들어 처음 EQ1과 EQ2를 해결할 수있을 것입니다 여부입니다. 그런 다음 결과를 사용하여 eq3를 해결하십시오.

assert eq1 
assert eq2 

(check-sat) 

assert eq3 
(check-sat) 
(get-model) 

효과가있는 것처럼 보이지만 실적이 좋은지 확실하지 않습니까? 점진적 해결이 도움이 될까요? 아니면 내 문제를 파티션하기 위해 사용할 수있는 z3의 다른 기능이 있습니까?

Answer 1

일반적으로 고려해야 할 문제는 만족할만한 문제입니다. 즉, 해결책 1 (모델)을 찾는 것이 목표입니다. 을 만족하는 솔루션 (모델)이 반드시 eq3을 만족시키지 않아 문제를 절반으로 줄일 수 없습니다. 에 대한 솔루션 (모델)을 찾아서 eq3에있는 x을 해당 솔루션으로 바꿀 수 있도록해야합니다. 예를 들어 행렬이 대각선이 된 후에 가우스 제거에서 일어나는 일입니다.