Thanh Hung Nguyen

• In this thesis, we combine Groebner basis with SAT Solver in different manners. Both SAT solvers and Groebner basis techniques have their own strength and weakness. Combining them could fix their weakness. The first combination is using Groebner techniques to learn additional binary clauses for SAT solver from a selection of clauses. This combination is first proposed by Zengler and Kuechlin. However, in our experiments, about 80 percent Groebner basis computations give no new binary clauses. By selecting smaller and more compact input for Groebner basis computations, we can significantly reduce the number of inefficient Groebner basis computations, learn much more binary clauses. In addition, the new strategy can reduce the solving time of a SAT Solver in general, especially for large and hard problems. The second combination is using all-solution SAT solver and interpolation to compute Boolean Groebner bases of Boolean elimination ideals of a given ideal. Computing Boolean Groebner basis of the given ideal is an inefficient method in case we want to eliminate most of the variables from a big system of Boolean polynomials. Therefore, we propose a more efficient approach to handle such cases. In this approach, the given ideal is translated to the CNF formula. Then an all-solution SAT Solver is used to find the projection of all solutions of the given ideal. Finally, an algorithm, e.g. Buchberger-Moeller Algorithm, is used to associate the reduced Groebner basis to the projection. We also optimize the Buchberger-Moeller Algorithm for lexicographical ordering and compare it with Brickenstein's interpolation algorithm. Finally, we combine Groebner basis and abstraction techniques to the verification of some digital designs that contain complicated data paths. For a given design, we construct an abstract model. Then, we reformulate it as a system of polynomials in the ring \({\mathbb Z}_{2^k}[x_1,\dots,x_n]\). The variables are ordered in a way such that the system has already been a Groebner basis w.r.t lexicographical monomial ordering. Finally, the normal form is employed to prove the desired properties. To evaluate our approach, we verify the global property of a multiplier and a FIR filter using the computer algebra system Singular. The result shows that our approach is much faster than the commercial verification tool from Onespin on these benchmarks.
• In dieser Arbeit kombinieren wir Gröbnerbasen mit SAT-Lösern auf unterschiedliche Weise. Beides, SAT-Löser sowie Gröbnerbasis-Techniken haben ihre eigenen Stärken und Schwächen. Die Kombination von ihnen könnte ihre Schwächen beheben. Die erste Kombination besteht darin mit Hilfe von Gröbnerbasis-Techniken zusätzliche binäre Klauseln für SAT-Löser aus einer Auswahl von Klauseln zu lernen. Dies wird zunächst durch Zengler und Küchlin vorgeschlagen. Jedoch geben über 80 Prozent der Gröbnerbasis-Berechnungen in unseren Experimenten keine neuen binären Klauseln. Durch die Wahl kleiner und kompakter Eingaben für die Gröbnerbasis-Berechnungen können wir deutlich die Zahl der ineffizienten Gröbnerbasis-Berechnungen reduzieren und so mehr binäre Klauseln lernen. Diese neue Strategie kann somit auch die benötigte Rechenzeit eines SAT-Lösers, vor allem f\"{u}r groß e und schwere Probleme, reduzieren. Die zweite Kombination nutzt all-solution-SAT-Löser und Interpolationsmethoden, um Boolesche Gröbnerbasen der Booleschen Eliminierungsideale eines gegebenen Ideals zu berechnen. Die Berechnung einer Booleschen Gröbnerbasis eines solchen Ideals ist sehr ineffizient, wenn wir die meisten der Variablen eines großen Systems Boolscher Polynome eliminieren wollen. Daher schlagen wir für diesen Fall einen effizienteren Ansatz vor. Dabei wird zuerst die gegebene Ideal-CNF-Formel umgerechnet und ein all-solution-SAT-Löser verwendet, um die Projektion aller Lösungen des gegebenen Ideals zu finden. Schließlich wird ein Algorithmus, beispielsweise der Buchberger-Möller-Algorithmus, verwendet, um die reduzierte Gröbnerbasis mit der Projektion zu verbinden. Weiter optimieren wir den Buchberger-Moeller-Algorithmus für lexikographische Ordnungen und vergleichen sie mit Brickensteins Interpolationsalgorithmus. Letztendlich kombinieren wir Gröbnerbasis- und Abstraktionstechniken, um die Verifikation mehrerer digitaler Designs, die komplizierte Datenpfade enthalten, durchzuführen. F\"{u}r eine gegebenes Design konstruieren wir ein abstraktes Modell und formulieren es als ein System von Polynomen im Ring \({\mathbb Z}_{2^k}[x_1,\dots,x_n]\). Die Variablen sind in einer Weise geordnet, dass das System bereits eine Gröbnerbasis gegenüber der lexikographischen monomialen Ordnung darstellt. Schließlich wird die Normalform verwendet, um die gewünschten Eigenschaften zu beweisen. Um unseren Ansatz zu bewerten, überprüfen wir die globalen Eigenschaften eines Multiplikators und eines FIR-Filters mit Hilfe des Computer-Algebra-Systems Singular. Das Ergebnis zeigt, dass unser neu entwickelter Ansatz eine Beschleunigung im Vergleich zum kommerziellen Verifikationstool OneSpin in den verwendeten Benchmarks bringt.