anldp – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

anldp – Implementierung des Davis-Putnam-Verfahrens zur Erfüllbarkeit von Aussagen

ZUSAMMENFASSUNG

andp [Optionen]] Eingabedatei > Ausgabedatei

BESCHREIBUNG

Diese Handbuchseite dokumentiert kurz die andp Befehl.

andp ist eine Implementierung eines Davis-Putnam-Verfahrens für den Satz
Erfüllbarkeitsproblem. andp legt das von verwendeten Verfahren offen mace2(1) zu bestimmen
Erfüllbarkeit. andp kann auch Aussagen in der Logik erster Ordnung mit Gleichheit und a annehmen
Domänengröße n Suchen Sie dann nach Größenmodellen n. Der Modellsuchcode erster Ordnung
wandelt die Aussagen in Satzsätze erster Ordnung um
Aussagen haben ein Größenmodell n genau dann, wenn die Satzsätze vorhanden sind
erfüllbar. Die Aussagenmenge wird dann dem Davis-Putnam-Code übergeben; beliebig
Gefundene Aussagenmodelle können in Modelle erster Ordnung übersetzt werden
Aussagen. Das Modellsuchprogramm erster Ordnung akzeptiert Anweisungen nur in abgeflachter Form
relationale Satzform ohne Funktionssymbole.

OPTIONAL

-s Subsumtion durchführen. (Die Subsumtion wird immer während der Unit-Vorverarbeitung durchgeführt.)

-p Drucken Sie Modelle so aus, wie sie gefunden werden.

-m n Stoppen Sie, wenn die nDas Modell ist gefunden.

-t n Stopp nach n Sekunden.

-k n Höchstens zuteilen n KB zur Speicherung von Klauseln.

-x n Quasigruppenexperiment n.

-B Datei
Sicherungszuweisungen zu einer Datei.

-b n Sicherungsaufgaben alle n Sekunden.

-R Datei
Stellen Sie Aufgaben aus einer Datei wieder her. Die Datei enthält normalerweise nur die letzte Zeile von
eine Sicherungsdatei. Sonstige Eingaben, insbesondere die Klauseln, müssen genau wie in erfolgen
die ursprüngliche Suche.

-n n Diese Option wird für die Suche nach Modellen erster Ordnung verwendet. Der Parameter n spezifiziert das
Die Domänengröße weist das Programm darauf hin, abgeflachte Daten erster Ordnung zu lesen
relationale Eingabeklauseln statt Aussagenklauseln.

Nutzen Sie anldp online über die Dienste von onworks.net