수량 한정 제거 - 기타 문의

Question

이전 질문에 대한 답변을 주신 Josh and Leonardo에게 많은 감사를드립니다.

나는 몇 가지 질문이 더 있습니다.

<> 다른 예를 생각해보십시오.

(exists k) i * k > = 4 and k > 1. 

이 난> 0 (모두 지능과 실제 사건에 대한) 나는 다음과 같은 노력

그러나

,

(declare-const i Int) 
(assert (exists ((k Int)) (and (>= (* i k) 4) (> k 1)))) 
(apply (using-params qe :qe-nonlinear true)) 

Z3 여기에 한정 기호를 제거 할 수 없습니다 간단한 솔루션을 제공합니다.

그러나 실제 사례는 없앨 수 있습니다. (i와 k가 모두 실수 일 때) 정수의 경우 수량 자 제거가 더 어렵습니까?

<> 내 시스템에 Z3 C API를 사용하고 있습니다. 필자는 시스템에 한정사가있는 Integer에 비선형 제약 조건을 추가하고 있습니다. Z3은 현재 만족 스러운지 확인하고 시스템이 만족스러운 경우 올바른 모델을 제공합니다.

수량 한정자 제거 후에 이러한 제약 조건이 선형 제약 조건으로 축소된다는 것을 알고 있습니다.

나는 z3가 자동으로 만족 여부를 확인하기 전에 한정사 제거를 수행한다고 생각했습니다. 그러나, 위의 경우 1에서, 이제는 수량 한정자 제거 기능이없는 모델을 일반적으로 발견 할 수 있다고 생각합니다. 나 맞아?

현재 z3은 내 시스템의 제약 조건을 해결할 수 있습니다. 그러나 복잡한 시스템에서는 실패 할 수 있습니다. 그런 경우, z3없이 몇 가지 다른 방법으로 한정 기호 제거를 수행하고 나중에 z3에 제약 조건을 추가하는 것이 좋은 생각입니까?

< 3> 시스템에서 정수 비선형 제약 대신 실제 비선형 제약을 추가 할 수 있습니다. 이 경우 C-API를 사용하여 수량 한정자 제거를 수행하기 위해 z3을 어떻게 적용 할 수 있습니까?

< 4> 마지막으로 z3을 사용하여 한정자 제거를 수행하는 것이 좋습니다. 또는 일반적으로 Quantifier Elimination을 수행하지 않고도 지능적으로 모델을 찾습니다.

감사합니다.

Answer 1

< 1> 비선형 정수 연산의 이론은 한정어 제거 (quantifier elimination, qe)를 ​​인정하지 않습니다. 또한 비선형 정수 연산의 결정 문제는 결정할 수 없습니다.

Z3은 비선형 실수 산술 수식의 한정어 제거에 대한 지원이 제한되어 있습니다. 현재 절차는 가상 용어 대체를 기반으로합니다. 이후 버전에서는 비선형 실수 산술을 완벽하게 지원할 수 있습니다.

< 2> 한정자 제거는 기본적으로 이 아니며입니다. 사용자가 요청해야합니다. 수량 한정자 제거가 활성화되지 않은 경우에도 Z3에서 만족할 수있는 수식에 대한 모델을 찾을 수 있습니다. 모델 기반 수량 화기 인스턴스화 (MBQI)라는 기술을 사용합니다. Z3 online tutorial에는이 기술의 기능 및 한계를 설명하는 몇 가지 예가 있습니다.

< 3> Z3_context 객체를 만들 때 활성화해야합니다. Z3_context 객체 생성 중에 명령 줄에서 설정 한 옵션을 제공 할 수 있습니다. 그 후

Z3_config cfg = Z3_mk_config(); 
Z3_context ctx; 
Z3_set_param_value(cfg, "MODEL", "true"); 
Z3_set_param_value(cfg, "ELIM_QUANTIFIERS", "true"); 
Z3_set_param_value(cfg, "ELIM_NLARITH_QUANTIFIERS", "true"); 
ctx = mk_context_custom(cfg, throw_z3_error); 
Z3_del_config(cfg); 

, ctx 모델 구축 및 정량 제거를 지원하는 Z3 콘텍스트 객체를 가리키는 다음은 예시이고, 그 구성 및 모델 정량 제거 할 수있다.

< 4> 선형 산술 조각의 경우에도 MBQI 모듈이 완료되지 않았습니다. Z3 온라인 자습서는 완료된 부분을 설명합니다. MBQI 모듈은 해석되지 않은 함수가 포함 된 문제에 적합한 옵션입니다. 문제가 산술만을 사용하는 경우 수량 한정자 제거가 일반적으로 더 효율적이고 더 효율적입니다. 즉, MBQI를 사용하면 몇 가지 문제를 신속하게 해결할 수 있습니다.