Dies ist der Befehl depqbf, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
depqbf – ein Löser für quantifizierte boolesche Formeln
ZUSAMMENFASSUNG
depqbf [Optionen ...] [NUM] [FILE]
BESCHREIBUNG
depqbf ist ein suchbasierter Löser für quantifizierte boolesche Formeln (QBF) in Prenex
konjunktive Normalform. Es basiert auf dem DPLL-Algorithmus für QBF mit Konfliktsteuerung
Klausel und lösungsgesteuertes Würfellernen. Durch die Analyse der Struktur einer Formel kann DepQBF
versucht, unabhängige Variablen zu identifizieren. Neben anderen Vorteilen ist dies häufig der Fall
erhöht die Entscheidungsfreiheit. Siehe auch die JSAT-Systembeschreibung von DepQBF 0.1
von QBFEVAL'10 für Referenzen und einen kurzen Überblick über die Idee.
depqbf liest QBF-Formeln im QDIMACS-Format. Wenn FILE nicht gegeben ist, liest es seine Eingabe aus
stdin. Es entspricht den Eingabe-/Ausgabestandards gemäß QBFEVAL'10.
OPTIONAL
depqbf akzeptiert die folgenden Optionen:
-H, --help
Nutzungsinformationen drucken.
--Version
Druckversion.
--schöner Druck
Nur Formeln analysieren und drucken.
-v Erhöhen Sie die Ausführlichkeit schrittweise.
NUM Optional: Timeout nach NUM Sekunden.
FILE Optional: Eingabe aus FILE lesen.
EXIT STATUS
Der Exit-Status ist 10, wenn die als Eingabe angegebene QBF-Formel erfüllbar ist, und 20, wenn dies der Fall ist
unerfüllbar; Jeder andere Exit-Code zeigt an, dass die Formel nicht gelöst wurde.
Verwenden Sie depqbf online über die Dienste von onworks.net
