Parallel software system for counting finite models

Abstract

<p>This dissertation is about the development of a parallel software system for<br />representing and solving problems of finite model theory and its application.<br />The theoretical foundation of the system is presented, as well as an in-depth<br />explanation of the implementation in Python. In particular, a parallel method<br />for computing Boolean expressions based on the properties of finite free<br />Boolean algebras is developed. It is also shown how various finite<br />combinatorial objects can be coded in the formalism of Boolean algebras and<br />counted by this procedure. Specifically, using a translation of first order<br />predicate formulas to propositional formulas, we developed a technique for<br />constructing and counting finite models of first order theories. Finally, we<br />have developed some general techniques that enable more effective use of<br />our system. We illustrate these techniques on two examples. The first one<br />deals with partial orders, while the other one is about random graphs.</p>

<p>Ова дисертација се бави развојем паралелног софтверског система за<br />представљање и решавање проблема теорије коначних модела и<br />његовом применом. Износи се теоријска основа система, као и детаљно<br />објашњење имплементације у Пајтону. Конкретно, развијен је<br />паралелан метод за рачунање Булових израза заснован на особинама<br />коначних слободних Булових алгебри. Такође се показује како се<br />различити коначни комбинаторни објекти могу кодирати у формализму<br />Булових алгебри и избројати применом овог поступка. Конкретно,<br />користећи транслацију предикатских формула првог реда на исказне<br />формуле развили смо технику за конструисање и бројање коначних<br />модела теорија првог реда. На крају, развили смо неке опште технике<br />које омогућавају ефективније коришћење нашег система. Ове технике<br />приказујемо на два примера. Први се бави парцијалним уређењима, а<br />други се односи на случајне графове.</p>

<p>Ova disertacija se bavi razvojem paralelnog softverskog sistema za<br />predstavljanje i rešavanje problema teorije konačnih modela i<br />njegovom primenom. Iznosi se teorijska osnova sistema, kao i detaljno<br />objašnjenje implementacije u Pajtonu. Konkretno, razvijen je<br />paralelan metod za računanje Bulovih izraza zasnovan na osobinama<br />konačnih slobodnih Bulovih algebri. Takođe se pokazuje kako se<br />različiti konačni kombinatorni objekti mogu kodirati u formalizmu<br />Bulovih algebri i izbrojati primenom ovog postupka. Konkretno,<br />koristeći translaciju predikatskih formula prvog reda na iskazne<br />formule razvili smo tehniku za konstruisanje i brojanje konačnih<br />modela teorija prvog reda. Na kraju, razvili smo neke opšte tehnike<br />koje omogućavaju efektivnije korišćenje našeg sistema. Ove tehnike<br />prikazujemo na dva primera. Prvi se bavi parcijalnim uređenjima, a<br />drugi se odnosi na slučajne grafove.</p>