Ho ottenuto diverse statistiche dalle corse di Z3. Devo capire cosa significano. Sono piuttosto arrugginito e non aggiornato per i recenti sviluppi di Sat e SMT solving, per questo motivo ho cercato di trovare spiegazioni da solo e potrei essere completamente sbagliato. Quindi le mie domande sono principalmente:Interpretazione delle statistiche Z3
1) Che cosa significano i nomi delle misure?
2) Se è sbagliato, puoi darmi dei suggerimenti per capire meglio a cosa si riferiscono?
Altre osservazioni sono presentate di seguito e concettualmente appartengono alle due domande precedenti. Grazie in anticipo!
La mia interpretazione segue.
DPLL. Tutte le metriche riportate di seguito si riferiscono al gergo dell'algoritmo DPLL che è alla base della maggior parte dei risolutori.
- : decisioni
- Numero di decisioni
- : propagazioni
- Numero di propagazioni (immagino propagazioni unità)
- : binary-propagazioni,: ternari-propagazioni
- Propagations di due e tre letterali in una volta
- : Conflitti
- Numero di conflitti
- : decisioni
RISOLUZIONE. Le operazioni rendevano le frasi di interpretazione come insiemi, in parole povere; tecniche prese dalla risoluzione che è un altro paradigma per risolvere SAT.
- : sussunto
- : sussunzione risoluzione
- Qual è la differenza tra i due precedenti?
- : dyn-sussunzione risoluzione
- dovrebbe essere descritto qui: apprendimento per Dynamic Sussunzione, da Hamadi et al.
ALTRE TECNICHE
- : minimizzate-lits
- un'idea chiara. È probabilmente correlato all'apprendimento delle clausole?
- : Sondaggio-assegnato
- Credo che conta il numero di assegnazione fatta quando "sondare", che credo sia una sorta di tecnica di lookahead.
- : del-clausola
- Numero di clausole eliminate (per quale motivo ridondanti??)
- : Elim-letterali: Elim-clausole: elimi- bool-vars: clausole bloccate dall'eliminazione
- Numero di entità dopo lo elim- eliminato. Queste metriche riferiscono a particolari SAT tecniche soluzione (vedi per riferimento bloccati clausola eliminazione, da M.Järvisalo et al.)
- : riavvia
- Numero di riavvii.
- : minimizzate-lits
ALTRI ASPETTI
- : mk-bool-var: mk-binario-clausola: mk-ternario-clausola: mk-clausola
- Numero di variabili booleane e binari , clausole ternarie e generiche create.
- : memoria
- massima quantità di memoria utilizzata.
- : gc-clausola
- clausole di garbage collection ...?
- Questa interpretazione è plausibile secondo i miei esperimenti dal momento che è sempre il caso che
- : gc-clausola < =: del-clausola; nel mio caso la disuguaglianza è severa.
- Non è sempre il caso che
- : gc-clausola < =: Elim-clausole; può anche essere: gc-clausola>: Elim-clausole
- : mk-bool-var: mk-binario-clausola: mk-ternario-clausola: mk-clausola
Questa è una buona domanda (insieme a risposte parziali) che non vengono affrontate in altre domande su SO completamente, ma qui ci sono alcune domande correlate che potrebbero essere utili: http://stackoverflow.com/questions/17856574/how- to-interpretation-statistics-z3 http://stackoverflow.com/questions/10949633/z3-real-arithmetic-and-statistics http://stackoverflow.com/questions/7340888/z3-statistics-what-does-time- misurare http://stackoverflow.com/questions/6841193/which-statistics-indicate-an-efficient-run-of-z3 – Taylor