I circuiti e le formule proposizionali ammettono forme equivalenti di varia grandezza. Per molte applicazioni, una minore dimensione é preferibile. La questione della sintesi di circuiti minimi o più in generale di formule proposizionali minime esiste da numerosi anni. Analogamente, la questione della riduzione di formule mediante eliminazione di variabili esiste in diversi ambiti quali il calcolo proposizionale, la logica del primo ordine, la soddisfazione di vincoli e le ontologie. Il problema che viene studiato in questo progetto é quello della formulazione minima mediante eliminazione o introduzione di nuove variabili. In particolare, viene considerato il problema di esistenza di una formula che abbia grandezza minore di un certo valore dato e che sia equivalente alla formula di partenza a meno di un insieme di variabili da cancellare. Lo stesso problema viene poi considerato mediante aggiunta di variabili piuttosto che eliminazione.
La minimizzazione di formule booleane e la riduzione mediante forget sono problemi analizzati già da diversi anni. Il progetto si prefissa lo scopo di usare la seconda per ottenere la prima: verificare quanto sia possibile ridurre la grandezza di una formula mediante eliminazione di variabili. A questo si aggiunge la possibilità di introdurre nuove variabili, cosa che in alcuni casi può portare a una riduzione ulteriore della grandezza.