Verwandte: CNF simplification (in der Tat, ich glaube, die Einreicher dieser Frage nach gewesen sein könnte, was ich hier will)CNF Formel Vereinfachen während alle Lösungen Erhaltung wrt bestimmte Variablen
Eine Reihe von Tools zur Vereinfachung existieren (oder " Preprocessing "vor dem Lösen) DIMACS-Format CNF-Formeln, und die meisten SAT-Löser enthalten einige. Alles, was mir bekannt ist, vereinfacht jedoch eine trivial erfüllbare Formel in eine trivial erfüllbare CNF mit null oder einer Variablen, d.h. sie versuchen nur, die Erfüllbarkeit der Formel zu bewahren. Ich habe zumindest den Vorverarbeitungsmodus von SatELite und cryptominisat ausprobiert.
Um CNF eines großen Problems zu konstruieren, scheint mir jedoch, dass es sehr nützlich wäre, eine gut definierte Teilmenge des Problems zu einer Zeit zu vereinfachen, die dann eine große Anzahl von Mal wiederholt werden kann endgültiger CNF mit zusätzlichen Einschränkungen zwischen einigen Variablen in diesen Teilformeln.
Also, irgendwelche Werkzeuge existieren, oder können gewöhnliche SAT-Löser (oder andere Löser wie Z3, die ich benutze, um den CNF zu produzieren, den ich minimieren möchte) irgendwie mit etwas Klugheit verwendet werden, um eine CNF Formel zu vereinfachen während alle Lösungen für eine gegebene Menge von Variablen erhalten bleiben?
Danke für den Zeiger. Es war sehr schwer, es zur Arbeit zu bringen. Es gibt einen Whitelist-Parameter, um Do-not-Touch-Variablen zu spezifizieren, und das Format dafür ist nicht dokumentiert (es braucht eine Datei, eine Variable pro Zeile oder einen Bereich pro Zeile wie in 1..10). Selbst dann ist es sehr empfindlich auf die Reihenfolge der Befehlszeilenparameter, stürzt auf interessante Weise im Hintergrund ab, wenn die Reihenfolge falsch ist, und schneidet die bereitgestellte Eingabe-.cnf-Datei im Prozess ab. Was für ein Stück Software: D –