risolutore per formule booleane quantificate
DepQBF è un risolutore basato su ricerca per le QBF (Quantified Boolean
Formulae, formule booleane quantificate) in forma normale congiuntiva
prenessa. È basato sull'algoritmo DPLL per QBF, chiamato QDPLL, con
clausola guidata dai conflitti e apprendimento del cubo guidato dalla
soluzione. Analizzando la struttura sintattica di una formula, DepQBF tenta
di identificare le variabili indipendenti. In generale, le informazioni
sulle variabili indipendenti possono essere rappresentate
nell'infrastruttura formale degli schemi di dipendenza. DepQBF calcola il
cosiddetto "schema di dipendenza standard" di una data formula. In aggiunta
ad altri benefici, le informazioni sulle variabili indipendenti spesso
aumentano la libertà per prendere le decisioni e per l'apprendimento delle
clausole.
