Aperçu des sections

  • Max 3-SAT

    L'objectif de ces deux séances est de travailler sur des formules 3-SAT, via le problème MAX 3-SAT:

    https://en.wikipedia.org/wiki/MAX-3SAT

    Vocabulaire:

    • Variables: les variables qui composent une formule sont des variables booléennes, pouvant prendre pour valeur vrai ou faux.
    • Littéraux: un littéral est constitué d'une variable ou de sa négation.
    • Clause: une clause est une disjonction de littéraux (un ou logique). Dans 3 SAT, on ne s'occupe que de clauses composées de exactement 3 littéraux.
    • Formule (sous forme normale conjonctive): une formule est une conjonction de clauses.  Dans le problème présent, on peut simplement la voir comme un ensemble de clauses.
    Un exemple de formule pourrait être:

    Le problème

    Le problème Max 3-SAT se décrit ainsi:
    Entrée:
    une formule 3-SAT. Ou encore, simplement un ensemble de 3-clauses.
    Sortie:
    Le nombre maximum de clause pouvant être satisfaite dans la formule.
    On peut aussi fournir un certificat, c'est à dire une affectation des variables qui valide ce nombre de clauses.

    • Icône Dossier
      Ressources pour SAT. Dossier

    • Implémentez le contenu des classes correspondant aux interfaces proposées, et ajoutez dans SatFormula une méthode:

          public static SatFormula random3Sat(int nbVars, int nbClauses,Random randomGen);

      qui génére une formule aléatoire. (Le randomGen vous permet de fixer la graine).