Improving Synthesis of Skolem Functions and Boolean Circuits

Abstract

Vom Standpunkt der Komplexitätstheorie geht man davon aus, dass es für das Erfüllbarkeitsproblem der Aussagenlogik (SAT) keinen effizienten Algorithmus gibt.Nichtsdestotrotz können moderne Entscheidungsprozeduren für SAT Formeln mit Millionen von Variablen und Klauseln lösen.Der Erfolg dieser Prozeduren motiviert die Arbeit an Entscheidungsprozeduren für stärkere Logiken, wie abhängigkeitsquantifizierte boolsche Formeln (DQBF).Aufgrund der effizienten Entscheidungsprozeduren für das SAT-Problem wurden viele verschiedene Probleme mittels einer Kodierung in Aussagenlogik gelöst.Dies umfasst im Speziellen das Problem der Berechnung von kleinen Schaltkreisen. DQBF erweitern die Aussagenlogik mit universellen und existenziellen Quantoren über Wahrheitswerte.Im Gegensatz zu quantifizierten boolschen Formeln (QBF) werden in DQBF die Abhängigkeiten von existentiellen Variablen explizit angegeben und nicht implizit durch die Ordnung der Quantoren bestimmt.Wir präsentieren einen neuen Algorithmus für das Erfüllbarkeitsproblem von DQBF, der direkt mit Skolemfunktionen arbeitet.Der Algorithmus nutzt Definitionen im Sinne der Aussagenlogik, um eindeutig bestimmte Skolemfunktionen zu berechnen.Des Weiteren nutzt der Algorithmus durch Gegenbeispiele geleitete induktive Synthese (CEGIS), um die Skolemfunktionen der verbleibenden Variablen zu adaptieren.Dadurch kann der Algorithmus für erfüllbare DQBF Skolemfunktionen ohne Mehraufwand bestimmen.Wir werden zeigen, dass der Algorithmus tatsächlich das Entscheidungsproblem für DQBF löst.Dieser Algorithmus wurde in einem Programm names Pedant implementiert.In einer experimentellen Evaluierung werden wir zeigen, dass Pedant für Standardbenchmarks mehr Formeln als andere aktuelle Entscheidungsprozeduren lösen kann. Es gibt keine effizienten Algorithmen, um kleinstmögliche Schaltkreise für eine bestimmte boolsche Funktion zu bestimmen. Aus diesem Grund müssen heuristische Methoden angewandt werden, um kleine Schaltkreise zu berechnen.Wir schlagen eine neue Methode zum Minimieren von Schaltkreisen vor.Diese Methode ist eine SAT-basierte lokale Verbesserungsmethode (SLIM).Um einen Schaltkreis zu verkleinern, werden iterativ Teilschaltkreise eines gegebenen Schaltkreises durch kleinstmögliche Schaltkreise ersetzt.Die für die Ersetzungen verwendeten Schaltkreise werden dabei entweder mittels einer SAT- oder einer QBF-Kodierung ermittelt.Hierfür ist es möglich, sowohl Teilschaltkreise mit einem einzelnen Ausgang als auch Schaltkreise mit mehreren Ausgängen zu betrachten.Um eine möglichsts große Freiheit für das Auffinden einer Ersetzung zu erhalten, werden don't cares des Teilschaltkreises berücksichtigt.Diese Minimierungsmethode wurde in einem Programm namens eSLIM implementiert.Basierend auf einer experimentellen Evaluierung zeigen wir, dass eSLIM zusammen mit dem Standardprogramm für die Schaltkreissynthese ABC bessere Ergebnisse liefert als ABC alleine.Schlussendlich zeigen wir auch, dass mit eSLIM viele der aktuell kleinsten Schaltkreise der EPFL Benchmarkmenge weiter verkleinert werden können.

While the propositional satisfiability problem SAT is intractable, from a theoretical perspective, modern SAT solvers can still handle formulas with millions of variables and clauses.This success of SAT solving motivates research on decision procedures for even stronger logics like Dependency Quantified Boolean Formulas (DQBF).To make use of the capabilities of modern SAT solvers, various different problems have been encoded in propositional logic.In particular, this includes the problem of finding small circuits. DQBF extend propositional logic by universal and existential quantification over truth values.Unlike to Quantified Boolean Formulas (QBF), in DQBF, dependencies of existentially quantified variables are explicitly stated and not implicitly determined by the ordering of quantifiers.We propose a new decision procedure for DQBF that directly reasons at the level of Skolem functions.The procedure makes use of propositional definitions to extract uniquely defined Skolem functions and counter-example guided inductive synthesis (CEGIS) to refine Skolem functions for the remaining variables.This allows to derive Skolem functions for satisfiable DQBF with no overhead.We will proof that the proposed algorithm is indeed a decision procedure for DQBF.Moreover, in an experimental evaluation, we will show that our solver Pedant that implements the proposed algorithm, surpassed the performance of state-of-the-art DQBF solvers on standard benchmarks. Determining provably minimum size circuits computing a given Boolean function is computationally intractable.For this reason heuristic, methods need to be considered for obtaining small circuits.We propose a new circuit minimization approach that belongs to the SAT-based Local Improvement Method (SLIM) framework.In this approach, we incrementally replace subcircuits of a given circuit by minimum size replacement circuits.This is achieved by either making use of a QBF or of a SAT encoding.The presented method allows to consider both single- and multi-output subcircuits.Additionally, it makes use of the full implementational freedom for determining a replacement circuit by taking don't cares into account.We implemented this minimization method in the tool eSLIM.In an experimental evaluation, we show that using eSLIM together with the state-of-the-art synthesis tool ABC results in significantly smaller circuits compared to applying ABC alone.Moreover, we used eSLIM to further improve the current best solutions for the EPFL benchmark set.