Le problème
SAT consiste à déterminer si une formule en FNC est satisfaisable.
Écrire une fonction `sat_brute_force(clauses, variables)` qui résout SAT par force brute (test de toutes les valuations).Tester sur la formule : (p∨q)∧(¬p∨r)∧(¬q∨¬r).Quelle est la complexité de cet algorithme ? Pourquoi ne peut-on pas espérer beaucoup mieux (en l'état des connaissances) ?