Il s'agit de la commande depqbf qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
depqbf - un solveur pour les formules booléennes quantifiées
SYNOPSIS
depqbf [Options ...] [NUM] [DOSSIER]
DESCRIPTION
depqbf est un solveur basé sur la recherche pour les formules booléennes quantifiées (QBF) dans prenex
forme normale conjonctive. Il est basé sur l'algorithme DPLL pour QBF avec
clause et apprentissage du cube axé sur les solutions. En analysant la structure d'une formule, DepQBF
essaie d'identifier des variables indépendantes. En plus d'autres avantages, cela
augmente la liberté de décision. Voir aussi la description du système JSAT de DepQBF 0.1
de QBFEVAL'10 pour les références et un bref aperçu de l'idée.
depqbf lit les formules QBF au format QDIMACS. Si DOSSIER n'est pas donné, il lit son entrée à partir de
stdin. Il est conforme aux normes d'entrées/sorties requises par QBFEVAL'10.
OPTIONS
depqbf accepte les options suivantes :
-h, --Aidez-moi
Imprimer les informations d'utilisation.
--version
Version imprimée.
--joli-impression
Seulement analyser et imprimer la formule.
-v Augmentez progressivement la verbosité.
NUM Facultatif : délai d'attente après NUM secondes.
DOSSIER Facultatif : lire l'entrée de FILE.
EXIT STATUT
Le statut de sortie est 10 si la formule QBF donnée en entrée est satisfiable, et 20 si elle est
insatisfaisant ; tout autre code de sortie indique que la formule n'a pas été résolue.
Utilisez depqbf en ligne en utilisant les services onworks.net
