Parallel software system for counting finite models

Abstract

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

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

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