Quali sono i limiti del ragionamento nell'aritmetica quantificata in SMT?

Question

Ho provato diversi solutori SMT (CVC3, CVC4 e Z3) sul seguente parametro di riferimento apparentemente banale:

(set-logic LIA) 
(set-info :smt-lib-version 2.0) 
(assert (forall ((x Int)) (forall ((y Int)) (= y x)))) 
(check-sat) 
(exit) 

solutori tutti ritornano sconosciuta. Capisco che questo è un frammento indecidibile (ben non lineare) ma mi aspettavo che ci sarebbe stata una semplice euristica di istanziazione che potesse risolverlo. Ho anche provato ad aggiungere alcune asserzioni extra con costanti, ma non è stato d'aiuto.

C'è un modo per attaccare questi problemi e quali sono i limiti del ragionamento nell'aritmetica quantificata in SMT?

Answer 1

Il tuo esempio rientra nella categoria Aritmetica lineare (LIA).

LIA, ad esempio Presburger Arithmetic, ammette l'eliminazione del quantificatore (qe) anche se la complessità del tempo delle procedure qe è proibitivamente alta.

non sono sicuro che l'eliminazione sostegno CVC3 e CVC4 quantificatore per LIA, ma in Z3 si può fare

(set-logic LIA) 
(set-info :smt-lib-version 2.0) 
(assert (forall ((x Int)) (forall ((y Int)) (= y x)))) 
(check-sat-using (then qe smt)) 

Da Rise4Fun execution, ho unsat risultato.

Qui la tattica qe è una fase di pre-elaborazione prima dell'applicazione della tattica di fine partita smt.

Answer 2

Il pad è corretto, il preprocessore qe può essere piuttosto costoso. Inoltre, non è efficace nelle formule provenienti da strumenti di verifica del software come VCC, Poirot, Dafny, VeriFast, Why3 e ESCJava2. Non è efficace perché le formule prodotte da queste applicazioni contengono anche funzioni non interpretate, array, ecc.

Come suggerisce la risposta di Pad, Z3 è una raccolta di motori. Fornisce API e comandi che consentono agli utenti di selezionare quale motore (o combinazione di motori) verrà utilizzato per risolvere un problema. Quando l'utente dice semplicemente (check-sat) prova a indovinare qual è il miglior motore per risolvere la formula di input. L'ipotesi si basa sulla struttura della formula di input e delle annotazioni fornite dall'utente (esempio: il comando set-logic). Stiamo espandendo continuamente il set di frammenti che vengono rilevati automaticamente e il set di motori che forniamo.

Detto questo, è imbarazzante che Z3 abbia perso un frammento come LIA e non abbia applicato automaticamente la procedura qe. Per le formule LIA, l'opzione qe è in genere l'opzione migliore. Le alternative basate su E-matching o MBQI non sono efficaci poiché sono pensate per frammenti completamente diversi.

Sono appena committed code che rileva LIA (anche quando non si utilizza set-logic). La modifica è già disponibile nel ramo unstable (working-in-progress). Sarà disponibile domani nelle build notturne e nella prossima versione ufficiale.