Un article de WikiProg.

Satisfaction (I can't get no)

Ce mini-projet est à rendre pour le 9 janvier 2012 à 23h42. Ouverture du rendu prévu le vendredi 6.

Le rendu est ouvert à l'adresse: http://teach.kh405.net/TP/EPITA2015/index.php?TP=20120109

Logique propositionnelle classique

Syntaxe

Avant de rentrer dans le vif du sujet, nous allons définir la notion d'expressions logiques (pour la logique propositionnelle classique.) Les expressions logiques sont soit des:

Atomes (une variable booléenne): $p$
La négation d'une expression logique: $\neg p$
La conjonction (et) de deux expressions logiques: $p\wedge q$
La disjonction (ou) de deux expressions logiques: $p \vee q$
L'implication entre deux expressions logiques: $p \Rightarrow q$
L'équivalence entre deux expressions logiques: $p \Leftrightarrow q$

Chaque variable (atome) d'une expression logique est soit vraie, soit fausse. Les connecteurs logiques ont leur sens classique: la négation est vraie si l'expression est fausse, la conjonction est vraie si et seulement si les deux expressions sont vraie, la disjonction est vraie si au moins l'une des deux expressions est vraie, l'implication $p \Rightarrow q$ correspond à $\neg p \vee q$ et enfin l´équivalence $p \Leftrightarrow q$ correspond à $(p \Rightarrow q) \wedge (q \Rightarrow p)$

Example

$a \wedge b$ : est vraie quand $a$ et $b$ sont vraie
$a \vee b$ : est vraie quand $a$ est vraie ou $b$ est vraie.
$a \vee \neg a$ est toujours vraie
$a \wedge \neg a$ est toujours faux

Formes normales

Forme Normale Conjonctive

Une expression est en forme normale conjonctive si:

L'opérateur de négation ne porte que sur des atomes;
L'opérateur de disjonction ne porte que sur des atomes ou des négations d'atomes.
L'opérateur de conjonction ne porte que sur des disjonctions.

En résumé une expression logique en forme normale conjonctive est une grande conjonction dont chaque membre est une disjonction d'atome ou de négation d'atome. Ce qui correspond à la forme suivante:

$\bigwedge_i\left(\bigvee_j\left(p^i_j\right) \vee \bigvee_j\left(\neg p^i_j\right)\right)$

Example L'expression $(a \Rightarrow (\neg b \wedge c)) \vee (a \wedge c)$ s'exprime en forme normale conjonctive:

$( \neg a \vee \neg b \vee a) \wedge (\neg a \vee \neg b \vee c) \wedge (\neg a \vee c \vee a) \wedge (\neg a \vee c \vee c)$

Forme Normale Disjonctive

Une expression est en forme normale disjonctive si:

L'opérateur de négation ne porte que sur des atomes;
L'opérateur de conjonction ne porte que sur des atomes ou des négations d'atomes.
L'opérateur de disjonctive ne porte que sur des conjonctions.

En résumé une expression logique en forme normale disjonctive est une grande disjonction dont chaque membre est une conjonction d'atome ou de négation d'atome. Ce qui correspond à la forme suivante:

$\bigvee_i\left(\bigwedge_j\left(p^i_j\right) \vee \bigwedge_j\left(\neg p^i_j\right)\right)$

Example L'expression $(a \Rightarrow (\neg b \wedge c)) \vee (a \wedge c)$ s'exprime en forme normale disjonctive:

$\neg a \vee (\neg b \wedge c) \vee (a \wedge c)$

Une formule en forme normale disjonctive peut être vu comme l'union (le ou logique) de pairs d'ensembles $(P, N)$ où $P$ est l'ensemble des atomes positifs et $N$ l'ensemble des atomes négatifs. Chaque paire $(P, N)$ peut être vu comme une valuation possible des variables de la formule. En effet, si nous prenons l'exemple suivant:

$\left(a \wedge b \wedge \neg c\right) \vee \left(a \wedge \neg b \wedge c\right)$

, sous forme d'ensemble cette formule correspond à:

$\left(\left\{a,b\right\},\left\{c\right\}\right) \cup \left(\left\{a,c\right\},\left\{b\right\}\right)$

Maintenant supposons que pour un couple $(P, N)$ , l'ensemble $P$ contient les variables vraies et $N$ les variables fausses. Regardons ce qui passe pour notre expression: $a$ et $b$ sont vraies et $c$ fausses, du coup la sous-expression $a \wedge b \wedge \neg c$ est vraie, et donc notre expression également. Le raisonnement s'applique également pour le couple $\left(\left\{a,c\right\},\left\{b\right\}\right)$ . De manière générale, en posant que les variables de $P$ sont vraies et celles de $N$ sont fausses, alors tous les membres de la conjonction correspondante sont vrais et donc la conjonction l'est également. Par conséquent, l'une des conjonctions de la grande disjonction étant vraie, la disjonction l'est aussi.

Le raisonnement précédant n'est possible que s'il n'y a aucun élément commun entre $P$ et $N$ . Ce qui nous donne un guide pour simplifier une expression en forme normale disjonctive. Pour chaque conjonction de la forme $(P, N)$ :

On élimine les doublons dans $P$ et $N$ ;
Si $P\cap N \not= \emptyset$ alors la conjonction est supprimée de la disjonction;
S'il n'y a plus de conjonction dans la disjonction alors l'expression est toujours fausse.

Transformations

On peut montrer que pour toute expression, il existe une expression équivalente en forme normale (conjonctive ou disjonctive.) Il existe même des algorithmes pour passer n'importe quelles expressions en forme normale. Ces algorithmes reposent sur les règles d'équivalences classiques de la logique:

$\begin{array}{rcl} \neg (\neg p) & \leftrightarrow & p\\ \neg (q \wedge p) & \leftrightarrow & (\neg q \vee \neg p)\\ \neg (q \vee p) & \leftrightarrow & (\neg q \wedge \neg p)\\ (p\wedge q) \vee r & \leftrightarrow & (p \vee r) \wedge (q \vee r)\\ (p\vee q) \wedge r & \leftrightarrow & (p \wedge r) \vee (q \wedge r)\\ p \Rightarrow q & \leftrightarrow & \neg p \vee q\\ p \Leftrightarrow q & \leftrightarrow & (p \wedge q) \vee (\neg p \wedge \neg q)\\ \end{array}$

Satisfiabilité

Un expression logique est dite satisfiable, s'il existe un choix de valeur pour ses variables tel que l'expression soit vraie. Une expression logique est insatisfiable si, quelque soit les valeurs prises par ses variables, elle est fausse. Enfin une expression est une tautologie si elle est vraie quelque soit les valeurs prises par ses variables.

Déterminer la satisfiabilité d'une expression logique est un problème classique. L'objectif est de savoir s'il existe un choix de valeurs pour les variables de l'expression qui la rendent vraie. Ce problème est NP-complet: il existe une solution déductible en un temps polynomial, mais par un procédé non déterministe (impliquant des choix.) À l'heure actuelle, on ne sait pas s'il est possible de trouver une solution en temps polynomial déterministe (le déterminisme est nécessaire pour avoir un algorithme.)

Le problème de la NP-complétude (déterminer si l'ensemble des problèmes de complexité NP-time est équivalent à l'ensemble des problèmes de complexité P-time) est un problème ouvert important de l'informatique théorique. Intuitivement, les problèmes des NP: sont des problèmes à choix: la recherche de la solution implique de choisir une voie plutôt qu'une autre. Dans une version non-déterminise, les choix effectués sont toujours les bons, mais dans une version déterministe il faut essayer l'ensemble complet des choix.

Comme ce problème a été longuement étudié, il existe de nombreux algorithme pour le résoudre. Chaque solution à ses avantages et ses inconvénients. La méthode la plus classique est l'algorithme de Davis et Putnam^[1] et ses variantes. Elle donne les meilleurs résultats pour la satisfiabilité des expressions en forme normales conjonctives (conjonction de disjonction d'atomes positif ou négatif.)

Mais, comme vous l'aurez noté, il faut passer l'expression en forme normale conjonctives. D'un autre côté, la forme normale disjonctive simplifier permet de déterminer immédiatement si l'expression est satisfiable.

Toutes ces approches sont valables, dans le cas qui nous concerne les expressions n'étant pas en forme normale à l'origine, l'avantage de la méthode Davis&Putnam n'est pas probant.

Projet

L'objectif final est tester la satisfiabilité d'expression logique.

Le projet se découpe en différents niveaux, certains éléments de certains niveaux sont nécessaires pour l'évaluation des niveaux suivants (correction de la tarball, compilation ... )

Je vous fournit un parser tout fait pour lire les expressions, l'ensemble des fichiers se trouve ici: media:ModulesFournits.tar.bz2.

Pour l'utilisation de ce code voyez les explications du niveau 2.

Niveau 0 : structure du rendu

2 points

Votre rendu devra avoir la forme suivante:

L'archive (au format tar/bzip2) devra se nommer: login-20120109-sat.tar.bz2
Votre répertoire de rendu devra se nommer: login-20120109-sat
Votre répertoire de rendu devra contenir:
- un fichier AUTHORS au format habituel
- un fichier Makefile proposant les règles suivantes:
  - clean: qui nétoie le répertoire de travail
  - all: qui construit le binaire demandé (sat)
  - sat: comme la règle précédante
- les fichiers fournis (lexer.mll, lexer.ml, parser.mly, parser.ml, parser.mli et ast.mli)
- vos fichiers sources.

L'évaluation de ce niveau est bloquante si:

L'archive n'est pas au bon format
L'archive ne se décompresse pas
La commande make ou make sat ne produit pas le binaire sat

La moulinette suivra la procédure suivante pour tester votre rendu:

tar xjf login-20120109-sat.tar.bz2 login-20120109-sat
cd login-20120109-sat
make clean
make
# et, si sat n'est pas produit avant
make sat

Niveau 1: gestion des options

niveau nécessaire à la suite, pas de point

Votre programme devra supporter les options suivantes:

-pp: le programme effectue un pretty-print des expressions lues sur l'entrée standard (niveau 2) et ne calcule pas (et donc n'affiche pas) la satisfiabilité de ces expressions.
-help et --help affichage d'une aide en ligne.

Sans option, votre programme devra calculer la satisfiabilité des expressions lues sur l'entrée standard (niveaux 3 et supérieurs.)

La méthode la plus simple pour gérer les options est d'utiliser le module Arg d'OCaml

Niveau 2: pretty-print

5 points

Syntaxe des expressions

Je vous fournit pour ce projet un parser pour des fichiers représentant des expressions logiques. Ce parser se présente sous la forme de deux modules: lexer.ml et parser.ml. Ces deux fichiers sont obtenues automatiquement via ocamllex et ocamlyacc, ainsi que les fichiers sources lexer.mll et perser.mly.

L'utilisation de ces fichiers est relativement simple. On retrouve les connecteurs logiques usuels: ! (négation), & (et), | (ou), => (implication), <=> (équivalence), ainsi que les parenthèses et le point virgule (;) marquant la fin des expressions.

Example Si nous reprenons l'exemple du début, on obtient la formule suivante:

(a => !b & c) | (a & c);

Sa forme normale conjonctive:

(!a | !b | a) & (!a | !b | c) & (!a | c | a) & (!a | c | c);

Et sa forme normale disjonctive:

!a | (!b & c) | (a & c);

AST

Le parser construit une représentation (AST) de l'expression lue dans le type décrit dans le fichier ast.mli (il n'y a pas de .ml, il n'y a qu'un type.)

Le type est le suivant:

type expr =
    Atom of string
  | Not of expr
  | And of expr * expr
  | Or of expr * expr
  | Imp of expr * expr
  | Eq of expr * expr

Le nom des éléments parlent d'eux mêmes.

Usage du parser

Votre binaire prendra sur l'entrée standard les expressions logiques séparées par des points virgules. L'utilisation du parser et du lexer à cette fin ressemble à :

let main () =
  try
    (* ouverture du channel sur l'entree standard stdin *)
    let lexbuf =
      Lexing.from_channel stdin
    in
      (* boucle sur les expressions *)
      while true do
        (* result contient l'arbre obtenue *)
	(* result est de type Ast.expr *)
        let result = Parser.main Lexer.token lexbuf in
          (* Votre code ici *)
      done
  (* le lexer leve l'exception Lexer.Eof lorsque la fin de fichier est
     atteinte (Ctrl D sur l'entree standard) *)
  with Lexer.Eof -> exit 0
 
let _ = main ()

Pour votre Makefile, les dépendances des fichiers fournis (à inclure à la fin du Makefile) sont les suivantes:

lexer.cmo: parser.cmi 
lexer.cmx: parser.cmx 
parser.cmo: ast.cmi parser.cmi 
parser.cmx: ast.cmi parser.cmi 
ast.cmi: 
parser.cmi: ast.cmi

Enfin, pour la ligne de compilation finale, il faudra mettre les modules dans cet ordre: parser.cmx lexer.cmx

pretty-print

Le but de cette partie est d'afficher les expressions que le parser a lu dans le même format que le format en entrée.

L'affichage n'a pas besoin d'être (voir ne peut être) identique à l'entrée, du moment que l'expression est syntaxiquement équivalente. Une bonne technique pour vérifier votre pretty-printer est de réinjecter le résultat de votre programme dans lui même:

> cat expr.txt
(a => !b & c) | (a & c);
> cat expr.txt | sat -pp > expr-v1.txt
> cat expr.txt | sat -pp | sat -pp > expr-v2.txt
> diff expr-v1.txt expr-v2.txt

Si tout va bien diff n'affiche rien.

Niveau 3: satisfiabilité

8 points

Dans cette partie, vous devez déterminer si une expression est satisfiable. Le fonction est le même que pour le niveau précédant: les expressions sont lus sur l'entrée standard et le programme affiche un message indiquant si l'expression est satisfiable ou non.

Le message affiché est:

Y si l'expression est satisfiable
N si l'expression n'est pas satisfiable

Les messages devront être suivi d'un passage à la ligne !

Example

> cat expr.txt
p;
p & !p;
p | !p;
> cat expr.txt | ./sat
Y
N
Y
>

Niveau 4: Résistence à la monté en charge

5 point + 2 points bonus

Pour ce niveau, les tests auront la même forme que pour le niveau précédant, mais les expressions testées seront plus grosses: plus de variables et de cas tordus.

Le but est de tester la résistence et la performance de vos algorithmes. Bien évidement, votre programme s'exécutera dans un environnement légèrement restreint (pas plus de 2Go de RAM) et surtout sera interrompu s'il dépasse certaines limites de temps d'exécution (adaptées à chaque test.)

Annexe

Exemple de `Makefile`

Voici un petit exemple de Makefile (on suppose que vous avez un fichier main.ml à vous de remplacer vos noms de fichier dans la liste) :

# Basic Makefile for mini-proj01
 
# Define ML files
ML= parser.ml lexer.ml main.ml # add other files here in right order
MLI= ast.mli parser.mli
 
# Obj files
CMX=${ML:.ml=.cmx}
CMI=${MLI:.mli=.cmi}
 
# Compilers
OPT=ocamlopt.opt
BYTE=ocamlc.opt
 
# Linking main prog
sat: ${CMX}
	${OPT} -o sat ${CMX}
 
# Automatic build
.SUFFIXES: .ml .mli .cmx .cmi .mly .mll
 
.ml.cmx:
	${OPT} -c $<
 
.mli.cmi:
	${OPT} -c $<
 
.mll.ml:
	ocamllex $<
 
.mly.ml:
	ocamlyacc $<
 
# ocamlyacc produces .ml and .mli
parser.mli: parser.ml
 
# Dependencies
 
include .depend
 
.depend: Makefile parser.mli lexer.ml
	rm -f .depend
	ocamldep.opt ${MLI} ${ML} > .depend
 
# Cleaning
 
clean::
	rm -f *~
	rm -f *.cm[iox] *.o
	rm -f sat
 
#
# END
#

Tests simples

Voici quelques exemples basiques, pour tester il faut enlever les commentaires du fichier (ou remplacer lexer.mll par cette version media:lexer.mll et re-généré lexer.ml.) Le commentaire au dessus indique si l'expression est satisfiable ou non.

## Simple 1 var

# One var - SAT
a;

# Always false - NOT SAT
a & !a;

# Always true - SAT
a | !a;

# Always true - SAT
a <=> a;

# Always false - NOT SAT
a <=> !a;

## Basic ops: 2 vars

# And - SAT
a & b;

# Or - SAT
a | b;

# Imply - SAT
a => b;

# Equivalent - SAT
a <=> b;

## Combined op: 2 vars

# Not and : SAT
!(a & b);

# Not or : SAT
!(a | b);

# Not imply : SAT
!(a => b);

# Not eq : SAT
!(a <=> b);

# Not eq 1 var (always false) - NOT SAT
!(a <=> a);

## Some more basics

# Imply is Imply : SAT
(a => b) <=> (!a | b);

# Eq is Eq : SAT
(a <=> b) <=> ((a & b) | (!a & !b));

Tests avancés

Voici quelques exemples de tests un peu plus avancés:

# NOT SAT
((((a & b & c & d & g & h & i & j) => (e & f)) <=> ((a & b & c & d & g
& h & i & j) & !(e & f))) & (((a & b & c & d & g & h & i & j) => (e &
f)) <=> ((a & b & c & d & g & h & i & j) & !(e & f))) | (((a & b & c &
d & g & h & i & j) => (e & f)) <=> ((a & b & c & d & g & h & i & j) &
!(e & f))) & (((aa & bb & cc & dd & gg & hh & ii & jj) => (ee & ff))
<=> ((aa & bb & cc & dd & gg & hh & ii & jj) & !(ee & ff))));

# NOT SAT
((((a & b & c & d & g & h & i & j) => (e & f)) <=> 
((a & b & c & d & g & h & i & j) & !(e & f)))

& (((a & b & c & d & g & h & i & j) => (e & f)) <=>
((a & b & c & d & g & h & i & j) & !(e & f)))

| (((a & b & c & d & g & h & i & j) => (e & f)) <=>
((a & b & c & d & g & h & i & j) & !(e & f)))

 & (((aa & bb & cc & dd & gg & hh & ii & jj) => (ee & ff))
<=> ((aa & bb & cc & dd & gg & hh & ii & jj) & !(ee & ff))));

# SAT
a => b => c => d => e => f => g;

Référence

↑ M. Davis and H. Putnam, A Computing Procedure for Quantification Theory in Journal of The ACM, 1960

[0] M. Davis and H. Putnam, A Computing Procedure for Quantification Theory in Journal of The ACM, 1960

[1]

2012:API:OCaml:MiniProjet:Sat

Un article de WikiProg.

Sommaire

Satisfaction (I can't get no)

Logique propositionnelle classique

Syntaxe

Formes normales

Forme Normale Conjonctive

Forme Normale Disjonctive

Transformations

Satisfiabilité

Projet

Niveau 0 : structure du rendu

Niveau 1: gestion des options

Niveau 2: pretty-print

Syntaxe des expressions

AST

Usage du parser

pretty-print

Niveau 3: satisfiabilité

Niveau 4: Résistence à la monté en charge

Annexe

Exemple de `Makefile`

Tests simples

Tests avancés

Référence

Affichages

Outils personnels

Plan

Rechercher

Boîte à outils

2012:API:OCaml:MiniProjet:Sat

Un article de WikiProg.

Sommaire

Satisfaction (I can't get no)

Logique propositionnelle classique

Syntaxe

Formes normales

Forme Normale Conjonctive

Forme Normale Disjonctive

Transformations

Satisfiabilité

Projet

Niveau 0 : structure du rendu

Niveau 1: gestion des options

Niveau 2: pretty-print

Syntaxe des expressions

AST

Usage du parser

pretty-print

Niveau 3: satisfiabilité

Niveau 4: Résistence à la monté en charge

Annexe

Exemple de Makefile

Tests simples

Tests avancés

Référence

Affichages

Outils personnels

Plan

Rechercher

Boîte à outils

Exemple de `Makefile`