Quantum Algorithm for the Boolean Satisfiability Problem

In questo rapporto tecnico faremo una breve introduzione alla computazione quantistica, per poi presentare l'algoritmo di Grover ed una sua applicazione. La computazione quantistica si basa sui qubits, sistemi quantistici a due livelli che possono trovarsi in sovrapposizioni di stati. Un generico algoritmo quantistico può essere espresso come l'applicazione di una sequenza di gates, ossia operatori unitari che agiscono su un qubit o su una coppia di qubits. Grover presenta una soluzione al problema della ricerca lineare: abbiamo un database non strutturato di N elementi di cui soltanto uno soddisfa una determinata condizione, ed è questo che dobbiamo trovare. L'algoritmo di Grover introduce uno speed-up quadratico rispetto all'algoritmo classico, che consiste nell'esaminare singolarmente gli elementi nel database. Ciò deriva dalla possibilità dei qubits di stare in sovrapposizione di stati che porta al parallelismo intrinseco della computazione quantistica. Utilizzeremo infine l'algoritmo di Grover per affrontare il problema SAT, cioé trovare la soluzione di una formula logica booleana espressa in forma normale congiuntiva, ovvero come una congiunzione di disgiunzioni.