Features

Before having better, here's the README file like it's written.

Solver qbfl version 0.2 :

Reads "gzipped" (.gz) instances but accepts too non zipped ones.
Uses the SAT-solver Limmat version 1.3 as a SAT oracle for trivial falsity and trivial truth.
Written in recursive, qbfl.0.2 has the particularity to check trivial truth and trivial falsity on Σ with an evolutive frequency.

• Trivial falsity on Σ and Π,
• Trivial truth,
• Unit propagation,
• Pure or monotone literals propagation,
• Heuristics :
  • HEURISTIQUE_PREMIER : chooses the first possible literal and always in the same order,
  • HEURISTIQUE_RANDOM : a literal is randomly choosed,
  • HEURISTIQUE_JW : R. J. Jeroslow and J. Wang's heuristics adapted,
  • HEURISTIQUE_LEXICO : M. Bohm and E. Speckenmeyer's heuristics, on a lexicographic order,
  • HEURISTIQUE_QBFL : our own heuristics inspired from M. Bohm and E. Speckenmeyer's.

To compile :
     > make

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

where <option> is one of the following options

-c | --contact	display the adress where to contact the developper
-h | --help	display this short help about qbfl
-p | --pretty-print	clear the instance and display it
-t<sec> | --time-out=<sec>	to specify a timeout (in seconds)
-v | --version	display the version and out
-H<heur> | --<HEUR>	to specify the variable selection heuristics :
	- heur = 0 or HEUR = HEUR_PREMIER
	- heur = 1 or HEUR = HEUR_RANDOM
	- heur = 2 ou HEUR = HEUR_JW
	- heur = 3 or HEUR = HEUR_LEXICO
	- heur = 4 or HEUR = HEUR_QBFL
-vt<freq> | --vrai-trivial=<freq>	to specify the trivial truth testing frequency
-ft<freq> | --faux-trivial=<freq>	to specify the trivial falsity testing frequency on Σ

Per default :

• the lexicographic heuristics,
• trivial truth and trivial falsity's are checked each 100 branching,
• timeout is fixed to 1800 secondes.

Display :
    If -p (or -pretty-print) option is switched on, the instance in which we removed unused variables in the prefix and to which we add some comment lines is displayed.
    Else, if the instance can't be solved by our solver before the timeout, qbfl displays :
          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
    Else, displays :
          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>
    With :

• qdimacs_file : the name of the QDimacs specified instance,
• NBVARS (resp. NBCLS, NBQUANTS) : the number of variables (resp. clauses, quantifiers alternances) the instance contains,
• PREMQ : A if the most external quantifier is universal, else E,
• TPS_CHARGE : the time (in hours/minutes/seconds) needed to read the instance,
• TPS_EVAL : the time needed to evaluate the QBF and to obtain a result,
• TPS_TOTAL : execution's total time,
• RESULTAT : 0 if <qdimacs_file> is a negative instance of QBF, else 1,
• CAUSE_RES :
  • "Formule trivialement fausse sur Pi" if the formula countains some null clauses or universal ones (trivial falsity on Π),
  • "Formule trivialement fausse sur Sigma" if the set of existential clauses is UNSAT (using Limmat),
  • "Formule trivialement vraie" if the formula to which we catch universal variables of is SAT (using Limmat),
  • "La solution n'est pas triviale" in every other case,
• RES : TRUE if resultat = 1 and FALSE if resultat = 0.

• NBE = the number of branching variables,
• NBFTP (resp. NBFTS) = the number of trivial falsity on Π (resp. Σ) met,
• NBVT = the number of trivial truth met,
• NBTV = the number of times all clauses were satisfied,
• TPSP = the total time to check triviality.