Improving a Language for a Compiler of Propositional Formulae

Alo Aasmäe
Many combinatorial problems can be described by propositional formulae. By finding possible interpretations that satisfy a given formula, it is possible to find the solution to the problem by counting the number of satisfiable interpretations. There has been created a translator for propositional formulae to tackle combinatorial problems in such a way, which translates a parametrized formula described in LaTeX to a formula without parameters. This new formula can be used to find the number of satisfiable interpretations by using a satisfiability counter.
The aim of this thesis is to give an overview of how to modify and improve a programming language using this existing translator as an example. As a result of the work of this thesis the translator is now able to process more complicated descriptions of logical formulae, for example such formulae that describe a problem using complements of a graph. To show this result, a formula for describing the cliques of a graph by Stamm-Wilbrandt, a problem that was not previously processable by the translator, was analyzed and validated. The improved translator is useful for conducting scientific experiments, where there is known the amount of satisfiable solutions, but the descriptions of those solutions is not entirely known.
Graduation Thesis language
Graduation Thesis type
Bachelor - Computer Science
Ahti Peder
Defence year
PDF Extras