"En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donnée une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité. Il a été mis en lumière par le théorème de Cook, qui est à la base de la théorie de la NP-complétude et du problème P = NP. Le problème SAT a aussi de nombreuses applications notamment en satisfaction de contraintes, planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation : on se ramène à des formules propositionnelles et on utilise un solveur SAT." (Wikipédia).

Je propose ici un solveur SAT écrit en Javascript.

Voir la source du programme - Github
La fonction principale est la fonction "bruteforce".

Le programme parcourt une seule fois chaque variable de chaque clause et enregistre les variables qui sont contrariées, c'est-à-dire, une même variable qui est présente au moins deux fois dans l'équation logique et qui est au moins une fois positive, et une autre fois négative.
En suite, le programme parcourt chaque variable contrariée 2 fois (pour 0 et 1) et pour déterminer si l'équation possède au moins une seule solution.

Les variables qui ne sont pas contrariées sont par défaut valorisées à vrai si elles sont positives, ou à faux si elles sont négatives.
Ce qui simplifie le bruteforce.
L'évaluation de l'équation dans son ensemble se fait par simple expression de logique booléenne, exemple :
(v[1]|!v[3]) & (!v[1]|v[2]) & (v[3]) renverra vrai ou faux en fonction des valeurs des variables booléennes "v".

Ci-dessous vous avez la possibilité de tester l'algorithme en Javascript, soit en générant une équation logique aléatoirement, soit en entrant l'équation logique de votre choix sous la forme d'un tableau JSON à deux dimensions.