Caractéristiques

En attendant d'avoir mieux, voici le fichier README tel qu'il est écrit à l'heure actuelle.

Prouveur qbfl version 0.2 :

Lit des instances "gzipées" (.gz) mais accepte également les instances non zipées.
Utilise pour le faux et le vrai trivial le prouveur Limmat dans sa version 1.3.
Ecrit en récursif, qbfl.0.2 présente la particularité d'avoir une vérification du faux trivial sur Σ et du vrai trivial a fréquence évolutive.

• Faux trivial sur Σ et Π,
• Vrai trivial,
• Propagation unitaire,
• Propagation des littéraux purs ou monotones,
• Heuristiques :
  • HEURISTIQUE_PREMIER : Choisit toujours les litteraux dans le meme ordre,
  • HEURISTIQUE_RANDOM : Choisit un litteral au hasard parmi ceux possibles,
  • HEURISTIQUE_JW : Choisit un litteral selon l'heuristique de Jerolow-Wang adaptee,
  • HEURISTIQUE_LEXICO : Choisit selon l'ordre lexicographique de Bohm-Speckenmeyer d'apparition des litteraux dans les clauses.

Pour compiler :
     > make

Usage : qbfl.0.2 [<option> ...] [ <qdimacs_file.gz> ]

où <option> est l'une ou plusieur des options suivantes

-c | --contact	affiche l'adresse où contacter le développeur
-h | --help	affiche cette aide succinte de qbfl
-p | --pretty-print	purifie l'instance et l'affiche
-t<sec> | --time-out=<sec>	specifier le temps limite
-v | --version	affiche la version et sort
-H<heur> | --<HEUR>	specifier l'heuristique de choix de variable :
	- heur = 0 ou HEUR = HEUR_PREMIER
	- heur = 1 ou HEUR = HEUR_RANDOM
	- heur = 2 ou HEUR = HEUR_JW
	- heur = 3 ou HEUR = HEUR_LEXICO
	- heur = 4 ou HEUR = HEUR_QBFL
-vt<freq> | --vrai-trivial=<freq>	specifier la frequence de verification du vrai trivial
-ft<freq> | --faux-trivial=<freq>	specifier la frequence de verification du faux trivial sur Σ

Par defaut :

• l'heurisique lexicographique,
• le vrai trivial et le faux trivial sur Σ sont verifiés à tous les 100 choix de variable,
• le temps limite est fixé à 1800 secondes.

Affichage :
    Si l'option -p (ou --pretty-print) est enclanchée, affiche l'instance à laquelle nous retirons les variables inutiles dans le prefixe et nous ajoutons des lignes de commentaires
    Si l'instance ne peut être resolue dans le temps imparti, affiche :
          c qbfl.0.2 -t<sec> -H<heur> -vt<freqv> -ft<freqf>
          c <qdimacs_file> : CNF(<NBVARS>,<NBCLS>)-<NBQUANTS>QBF(<PREMQ>)
          c Charge : <TPS_CHARGE>
          c Temps ecoule
          s UNKNOWN
    Sinon, affiche :
          c qbfl.0.2 -t<sec> -H<heur> -vt<freqv> -ft<freqf>
          c <qdimacs_file> : CNF(<NBVARS>,<NBCLS>)-<NBQUANTS>QBF(<PREMQ>)
          c Charge : <TPS_CHARGE>, Evalue : <TPS_EVAL>, Total : <TPS_TOTAL>
          c Res = <RESULTAT> : [CAUSE_RES]
          s <RES>
    Avec :

• qdimacs_file : le nom de l'instance DIMACS specifiée
• NBVARS (resp. NBCLS, NBQUANTS) : le nombre de variables (resp. de clauses, d'alternances de quantificateurs) que l'instance contient,
• PREMQ : A si le premier quantificateur est universel, E sinon,
• TPS_CHARGE : temps mis pour charger l'instance,
• TPS_EVAL : temps mis pour evaluer la QBF et obtenir RESULTAT,
• TPS_TOTAL : temps total de l'execution,
• RESULTAT : 0 si <qdimacs_file> est une instance negative de QBF, 1 sinon,
• CAUSE_RES :
  • "Formule trivialement fausse sur Pi" si la formule contient des clauses nulles ou universelles,
  • "Formule trivialement fausse sur Sigma" si l'ensemble des clauses existentielles est UNSAT (utilisation de Limmat),
  • "Formule trivialement vraie" si la formule a laquelle on a retire les variables universelles est SAT (utilisation de Limmat),
  • "La solution n'est pas triviale" dans tous les autres cas,
• RES : TRUE si resultat = 1 ou FALSE si resultat = 0.

• NBE = le nombre de choix de variable,
• NBFTP (resp. NBFTS) = le nombre de faux triviaux sur Π (resp. Σ) rencontrés,
• NBVT = le nombre de vrais triviaux rencontrés,
• NBTV = le nombre de fois où toutes les clauses ont été satisfaites,
• TPST = le temps nécessaire à la vérification de la trivialté.