0
Profitieren Max-SMT von inkrementellen Lösungen? Wenn ja, unterstützt Z3 das? und wie kann ich es benutzen? Vielen Dank.Profitieren Max-SMT von inkrementellen Lösungen?
A
Antwort
1
stackoverflow erlaubt inkrementelle Fragen, aber die Optimierungsroutinen von Z3 sind nicht inkrementell :-) Die API macht Push/Pop-Funktionen verfügbar, aber sie dienen nur der Bequemlichkeit. Wenn es um das Lösen geht, führt Z3 eine Vorverarbeitung für den gesamten Satz von aktivierten Formeln durch und ruft dann Maximierungsroutinen auf. Selbst wenn es keine Vorverarbeitung gäbe, ist es möglicherweise eine interessante Frage, was es bedeuten würde, kern- (und Korrekturmengen-) basierte Max-sat-Löser inkrementell sinnvoll zu machen.
Verwandte Themen
- 1. Threejs - wie viel profitieren Sie von puffergeometries?
- 2. Werden Web-Mitarbeiter von ionic app profitieren?
- 3. Wo profitieren Sie von dynamischer Typisierung?
- 4. Speichern von inkrementellen Preisen in MongoDB
- 5. Wird Sternschema in Rotverschiebung profitieren?
- 6. Create Array von inkrementellen Int mit Stream anstelle von Schleife
- 7. Könnte ich vom Frühling mit BlazeDS profitieren
- 8. Doppelte Lösungen
- 9. Welche Algorithmen profitieren am meisten von fusioniertem Multiply Add?
- 10. Ermitteln, welche Klassen am besten von Komponententests profitieren würden?
- 11. Profitieren Sie von gprof basierend auf der Wanduhrzeit?
- 12. Wird in SQLite3 diese SELECT-Anweisung von zwei Indizes profitieren?
- 13. Einfügen von inkrementellen Werten in einem Insert ... Select-Anweisung mysql
- 14. So aktualisieren Sie eine Gruppe von Datensätzen mit inkrementellen Werten
- 15. Erstellen von Datenrahmen mit inkrementellen Minuten als Zeilen (R)
- 16. Kann RESTful-Webdienst vom SPDY-Protokoll profitieren?
- 17. SQL-Insert-Funktion (Inkrementellen Wert einfügen)
- 18. C Probleme und Lösungen
- 19. Server-chart-Lösungen
- 20. Caching-Lösungen und Abfragen
- 21. Mehrere Lösungen bei ILP
- 22. Samt Origin Policy Lösungen
- 23. LinkButton Übergabe von mehrwertigen möglichen sauberen Lösungen
- 24. Lösungen zum Einfügen von doppelten Schlüsseln
- 25. Webseiten zum Drucken von Medien - Lösungen?
- 26. Django 1.2 Objektebene Berechtigungen - Lösungen von Drittanbietern?
- 27. Vorkompilieren von ASP.net-Lösungen für die Bereitstellung
- 28. Lösungen zum Organisieren von Guice-Binding-Konfigurationen
- 29. Lösungen zum Verfolgen von Gurkenfunktionen und Szenarien?
- 30. EAV Lösungen/Pakete/Lieferanten?
Da dies eine allgemeine algorithmische Frage ist, erhalten Sie möglicherweise eine bessere Antwort auf Programmers.SE. Du könntest einen Moderator bitten, es zu portieren. – msanford
@msanford Algorithmus Fragen sind auf beiden Seiten zum Thema, und diese Frage ist ein wenig unklar. Es sollte verbessert werden, bevor die Migration in Betracht gezogen wird. –
@Snowman Guter Punkt (vor allem angesichts Ihrer Abstammung). Ich habe oft Schwierigkeiten herauszufinden, wo eine Frage dieser Art gehört. – msanford