C/C++ - Formule logiche

Mentre stavo leggendo un po di logica proposizionale, mi è venuta voglia di creare un programma in linguaggio C che poteva essere interessante:
acquisire da tastiera un formula logica (esempio: a or b and c implica d), e verificare se esiste un assegnamento di verità che la soddisfi.
Allora... io mi ci sono messo giù a pensare e ripensare su come fare ma....
l'unica cosa che so è che è necessario creare un array di caratteri (per poter acquisire le lettere e i numeri (i numeri, per semplicità, sostituiscono i connettivi logici); però non riesco proprio a capire come fare verificare l'assegnamento di verità della formula.
Io ci ho pensato per molto tempo e per il momento non mi è venuto in mente praticamente niente.
Volevo chiedervi se potevate aiutarmi, fatemi sapere.
Ciao.

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.