La détermination de la satisfabilité d'une formule sous forme normale de jonction, où chaque clause se limite à au plus trois caractères, est complète pour le NP ; ce problème est appelé '' 3SAT '', '' 3CNFSAT '' ou '3-satisfabilité'. La détermination de la satisfabilité d'une formule dans laquelle chaque disposition est limitée à au plus deux littéraux est complète à NL ; ce problème est appelé '2SAT' '.
Chaque clause comporte plusieurs termes.