smt.arith.nl.gb가 (구문) 평등을 가진 추론에 예기치 않은 영향을 미쳤습니까?

Question

(rise4fun here)에 다음과 같은 SMTLIB 프로그램을 고려 :

(set-option :auto_config false) 
(set-option :smt.mbqi false) 
(set-option :smt.arith.nl.gb false) 

(declare-const n Int) 
(declare-const i Int) 
(declare-const r Int) 

(assert (= i n)) 
(assert (= r (* i n))) 

(push) 
(assert (not (= r (* n n)))) 
(check-sat) ; unknown 
(pop) 

을 단지 구문 평등과 추론, Z3 (4.3.2 공식 출시하고, 또한 4.4.0 b6c40c6c0eaf)를 필요로 보이지만 그럼에도 불구 보여 실패 최종 어설 션은 unsat입니다.

예기치 (적어도 내게) smt.arith.nl.gbtrue로 설정하는 것은 예 (즉 check-satunsat 수율)을 확인한다. 그것은 가치가 무엇인지에 대한

, 여기에 몇 가지 더 관찰은 다음과 같습니다

• 각각 곱셈 (* i n) 또는 (* n i)로 변경되는 경우unsat를 표시 할 수 있습니다 마지막 주장,

• 그것은 수 없습니다은 (* i i)

로 변경하면 unsat으로 표시됩니다. 그들이 설명 관찰

에 영향을주지 않고 제거 할 수 있습니다 즉

(push) 및 (pop)이 버그가, 예에 영향을 나타나지 않습니다 또는 smt.arith.nl.gb이 예제를 제시해야되는 이유가있다 unsat?

Answer 1

이것은 반드시 버그 일 필요는 없습니다. Groebner 기반 계산은 문제를 해결하므로, 결과를 빨리 찾을 수 있습니다 (좋으므로 기본적으로 활성화되어 있습니다). 또한 auto_config를 비활성화하면 다른 옵션 호스트가 문제에 따라 설정되지 않는다는 것을 의미합니다 (그러나이 경우에는 차이가 없습니다).

일부 전술, 해결사 또는 단순화자는 사람이나 다른 해결사가 쉽게 문제를 해결할 수 있는지 여부와 상관없이 단순히 곱셈 식을 볼 때 포기합니다. 이 특별한 경우 비선형 솔버는 smt.arith.nl.rounds가 고갈 된 후에 포기합니다 (기본적으로 1024). 따라서 unknown을 반환합니다.

이 문제를 신속하게 해결하는 방법 중 하나는 solve-eqs이지만이 방법은 기본 전략 (이 경우 qfnia 전략을 실행 함)의 일부가 아닙니다. 이 문제에 떨어져 지불하는 경우,이 기본이 논쟁의 여지가 벤치마킹까지 수 있는지 여부는

(check-sat-using (then solve-eqs qfnia)) 

와 체크 토 명령을 대체하여 쉽게 그것을 추가 할 수 있습니다,하지만 정말 버그가 아닙니다.

빨리이 문제를 해결 NLSAT 해결사 또 다른 전술, 예를 들어,

(check-sat-using nlsat)