Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision
Révision précédente
enseignement:logique:projet:2013 [2013/11/25 22:56]
rthion [Exploration de l'espace de recherche]
enseignement:logique:projet:2013 [2013/12/19 12:53] (Version actuelle)
ecoquery [Organisation du projet]
Ligne 55: Ligne 55:
 <note important> <note important>
 Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. //Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles//. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci //n'implique pas// de devoir s'échanger les sources entre binômes. Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. //Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles//. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci //n'implique pas// de devoir s'échanger les sources entre binômes.
-Le projet est à rendre après les vacances de Noël sous la forme d'une archive comme celle qui vous est fournie. //Les modalités exactes du rendu seront données en temps utile//. 
 </note> </note>
  
Ligne 257: Ligne 256:
  
 La fonction procèdera comme suit: La fonction procèdera comme suit:
-  - mettre la valeur de ''suiv'' à VRAI dans ''valeurs'' +  - si ''suiv'' est supérieur à la taille de ''valeurs'', alors évaluer la CNF et renvoyer VRAI si elle est satisfaite. 
-  s'il reste des variables à affecter, appeler récursivement la fonction avec ''suiv+1'' +  - sinon: 
-  sinon tester la valeur de la cnf +    - mettre la valeur de ''suiv'' à VRAI dans ''valeurs'' 
-    * si la formule est vaut VRAI, renvoyer ''true'' +    Appeler récursivement la fonction avec ''suiv+1'' 
-    sinonmettre la valeur de ''suiv'' à FAUX et tester à nouveau la satisfiabilité de la formule (comme en 2/3) +      - si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' 
-      si la formule est satisfiablerenvoyer ''true'' +      sinon mettre la valeur de ''suiv'' à FAUX dans ''valeurs'' 
-      sinonremettre la valeur de ''suiv'' à INDETERMINEE, puis renvoyer ''false''.+    - Appeler à nouveau récursivement la fonction avec ''suiv+1'' 
 +      si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' 
 +      sinon la CNF n'est pas satisfiable pour l'affectation courante: remettre la valeur de ''suiv'' à INDETERMINEE, puis renvoyer ''false''. 
  
 <note warning>Dans la définition de la fonction ''cherche'', on suppose que la longueur du tableau ''vector<val_t> & valeurs'' passé en paramètre est //égale au nombre de variables (différentes) de la cnf//. Ainsi: <note warning>Dans la définition de la fonction ''cherche'', on suppose que la longueur du tableau ''vector<val_t> & valeurs'' passé en paramètre est //égale au nombre de variables (différentes) de la cnf//. Ainsi:
Ligne 304: Ligne 306:
  
 La génération de cette spécification par récurrence pour //n//-bits peut être définie comme suit:  La génération de cette spécification par récurrence pour //n//-bits peut être définie comme suit: 
-  * Additionneur 1-bit: +  * Additionneur 1-bit : on retourne le vecteur V=[B,A1] de taille //2// avec  
-    * A1 = S [ p1/t, q1 / u, ⊥ / w] +    * A1 = S [ p1/t, q1 / u, ⊥ / w], on calcule cette formule en construisant la substitution  [ p1/t, q1 / u, ⊥ / w] en en l'appliquant à S avec la méthode ''applique'' 
-    * B = R [ p1/t, q1 / u, ⊥ / w] +    * B = R [ p1/t, q1 / u, ⊥ / w], idem que précédemment, sauf que c'est R qui est modifiée et plus S. 
-  * Additionneur //n//-bits: +  * Additionneur //n//-bits : soit V'[B',A'n-1,...,A'1] le vecteur de taille //n// obtenu pour un additionneur de taille //n-1//, on va construire le vecteur résultat V =[B,An,An-1,...,A1] de taille //n+1// 
-    * A//n// = S [ p//n// / t, q//n// / u, B' / w ], où  B' est le dernier bit de sortie d'un additionneur à //n-1//-bits (récurrence) +    * A//1// à A//n-1// : on ne change rien : A'//i//=A//i// ; 
-    * B = R [ p//n// / t, q//n// / u, B' / w ], où  B' est le dernier bit de sortie d'un additionneur à //n-1//-bits (récurrence)+    * A//n// = S [ p//n// / t, q//n// / u, B' / w ], B' est le dernier bit de sortie d'un additionneur à //n-1//-bit que l'on va l'additionner aux bits p//n//et  q//n//. Autrement dit, B', est la retenue de la somme de  p//n-1//et  q//n-1// quand on pose l'addition ; 
 +    * B = R [ p//n// / t, q//n// / u, B' / w ], où  B' est le dernier bit de sortie d'un additionneur à //n-1//-bits, c'est le bit de poids le plus fort du vecteur V', c'est la retenue de l'addition de  p//n// et  q//n// evec la retenue  de p//n-1//et  q//n-1//.
  
  
Ligne 409: Ligne 412:
   * v4, 16/11/13: aide sur erreur ''m[]'' qui n'est pas const   * v4, 16/11/13: aide sur erreur ''m[]'' qui n'est pas const
   * v5, 24/11/13: modif partie sur additionneur   * v5, 24/11/13: modif partie sur additionneur
 +  * v6, 18/12/13: mise à jour de la description de la fonction ''cherche'' dans sa première version