Possible topics for master and bachelor thesis

Here I have collected possible topic areas in which I offer master thesis and bachelor thesis. In general if you are interested in thesis from the area of boolean function, do not hesitate to contact me. The particular topic can be adjusted according to your current interests.

• Modifications and heuristics in SAT solvers
• Applications of SAT solvers on concrete problems
• Knowledge compilation — compilation to various representations of boolean functions (e.g. DNNFs and related structures, disjunctions of renamable Horn fomulas)
• Encodings of problems and constraints into a CNF suitable for SAT solver calls
• Parameterized and heuristic algorithms for tasks related to SAT and representations of boolean functions
• Minimum representations of boolean functions

A Possible Topics

Please, contact me, if you are interested in more topics.

Effective DP elimination

Davis-Putnam algorithm for checking satisfiability of propositional formulas is based on resolution which is used to consecutively eliminate all variables from a formula. The algorithm uses a specific form of resolution which is also called a DP resolution. Nowadays, DP resolution is used to eliminate variables from a CNF. The goal of the project would be an effective implementation of DP elimination that could be used also on large formulas. This includes selecting suitable data structures for representing sets of clauses (e.g. set-trie) and selecting suitable heuristics for picking the next variable for elimination.