Problema de satisfacibilitat booleana

En teoria de complexitat computacional, el problema de satisfacibilitat booleana (també conegut per les sigles SAT) és el problema de determinar si existeix una interpretació que satisfà una fórmula booleana donada. En altres paraules, es qüestiona si les variables d'una fórmula booleana es poden reemplaçar de forma consistent pels valors CERT o FALS de manera que la fórmula s'avalui a CERT. Per exemple, la fórmula "a AND NOT b" es pot satisfer amb els valors a = CERT i b = FALS, que fan la fórmula doni CERT. En canvi, la fórmula "a AND NOT a" no té cap valor d'entrada que pugui donar CERT i no es pot satisfer en cap cas.^[1]

Aquest problema va ser el primer problema identificat dins la classe de complexitat NP-complet, i per tant, tots els problemes dins de la classe NP son tant complexos com SAT però no més que aquest. No es coneix cap algorisme que resolgui el problema SAT de forma òptima i es creu que no existeix, tot i que no s'ha pogut demostrar. De fet, resoldre el problema SAT amb un algorisme de temps polinòmic és equivalent a demostrar que P = NP.

Tot i això, existeixen algorismes heurístics per resoldre SAT capaços de treballar amb instàncies del problema amb desenes de milers de variables i fórmules amb milions de símbols.^[2] Aquests algorismes tenen aplicacions pràctiques en problemes d'inteli·lgència artificial, disseny de circuits i demostracions automàtiques de teoremes.