0
Ich suche nach einer Lösung, um (Minimum) Prim Implikant für eine Formel in QF_AUVV Logik mit Z3 Löser zu finden. ist es möglich, einen solchen partiellen Primimplikanten von z3 Solver zu bekommen?Prime Implicant in z3
Vielen Dank für Ihre Antwort. Wenn ich recht habe, meinen Sie, dass ich einen Algorithmus haben muss, um den Primimplikanten zu finden. Ich lese über die Relevanzausbreitung in z3, dass gerade essentielle Wahrheitszuweisungen für das Erfüllen der Formel, zum theoretischen Löser propagieren. kann ich von diesen Aufgaben profitieren? bin ich richtig, dass dies Teilzuteilung ist, die Primzahlimplikant für die Formel sein kann oder nicht. Wenn ja, kann ich die propagierten Zuordnungen zum Theorielöser aus der Formel extrahieren? – Mary
Wenn Sie einen Theorie-Löser implementieren, könnte das vielleicht helfen (beginnen Sie mit relevanter_eh (...) in anderen Theorien), sonst ist es wahrscheinlich nicht die (ziemlich beträchtliche) Anstrengung wert. Beachten Sie, dass die Relevanz auch für nicht-boolesche Unterbegriffe propagiert. Wenn Sie nach allen (Primzahl- oder anderen) Implikanten suchen, benötigen Sie mehrere SAT-Abfragen, nicht nur eine einzelne. Daher ist es wahrscheinlich am besten, all das in einer äußeren Schicht anstatt innerhalb des SMT-Solver zu implementieren. –
vielen Dank. Du hast recht. Könnte ich dir bitte mehr erklären, wenn man quantifiziert, um den Begriff der Implikanten zu axiomatisieren. es ist vage für mich. – Mary