È possibile utilizzare Z3 per eseguire il preprocesso dei problemi?

Question

Fare nuove ricerche sui risolutori SMT è spesso ostacolato dal fatto che i problemi disponibili richiedono molti trucchi e tecniche di pre-elaborazione non direttamente correlate alle procedure decisionali. Questi sono spesso inediti o richiedono tempo per implementarli e ottimizzarli in modo appropriato, e inoltre rende piuttosto difficile il confronto e la comprensione dei diversi solutori.

E 'possibile utilizzare Z3 come un pre-processore in grado di risolvere un problema e scaricarlo in una forma preelaborata (quella che lo stesso z3 utilizza per risolvere il problema)?

Non vedo alcuna opzione da riga di comando, ma suppongo che ci possa essere un modo per raggiungere questo risultato, tramite strategie, attraverso l'interfaccia python, o anche scrivere un codice extra.

Answer 1

Sì, Z3 può essere utilizzato come pre-processore. Il comando apply consente all'utente di applicare una tattica e dump come benchmark SMT 2.0. Ecco un esempio (disponibile anche online all'indirizzo http://rise4fun.com/Z3/eutO):

(declare-const x Real) 
(declare-const y Real) 

(assert (forall ((n Real)) (or (< x n) (< n y)))) 
(assert (= (< x y) (< x 100.0))) 

(apply (then qe nnf) :print false :print-benchmark true) 

Nell'esempio precedente, qe (eliminazione quantificatore) e NNF (forma negazione normale) tattiche vengono applicate al problema di input.

Alcuni punti aggiuntivi:

• diverse tattiche producono solo risultati equisatisfiable. Pertanto, un modello per il benchmark risultante non è necessariamente un modello per la formula originale. Possiamo chiedere a Z3 di scaricare il "convertitore modello" associato (opzione :print-model-converter true). Il convertitore del modello codifica i passaggi utilizzati da Z3 per convertire un modello per la formula risultante in un modello per la formula originale. Tuttavia, non esiste uno standard per la stampa di convertitori di modelli e Z3 non può leggere queste descrizioni. Ovviamente, possiamo incollare tutto insieme utilizzando le API programmatiche.

• Un piccolo insieme di tattiche produce sotto (solo i risultati sat possono essere attendibili) o sopra (solo i risultati unsat possono essere considerati attendibili) approssimazioni. Di solito vengono utilizzati nel modello o nella ricerca di prove. Quando Z3 visualizza l'obiettivo risultante, informerà che il risultato è preciso (sat e unsat possono essere considerati attendibili).