|
Direi che hai un buon gusto per i problemi difficili. Quello che hai scelto è il problema della soddisfacibilità booleana ed è un problema NP-completo, ossia è risolvibile in tempo polinomiale solo da un algoritmo non deterministico.
La difficoltà, quindi, non è tanto eseguire un parsing, ma piuttosto risolvere il problema in tempo ridotto, il che non è possibile dato che lo spazio delle soluzioni cresce esponenzialmente.
Una cosa leggermente più semplice è verificare se un insieme di formule logiche è consistente mediante risoluzione logica. Per la logica proposizionale, la risoluzione è corretta e completa per refutazione. Perciò se non trovi un risolvente puoi star sicuro che non esiste.
| 
