Markus Iser, Tomas Balyo

At present, the best performing sequential SAT solvers implement the Conflict-Driven Clause Learning (CDCL) algorithm. CDCL is a combination of backtrack search and conflict resolution, thus conceptually, the algorithm can be understood as search-guided resolution. Recent successes have in common that they use some kind of hybrid approach. Hybridization can be observed in schedules for combinining branching heuristics, or combinations of clause forgetting policies. Hybridization of solving paradigms can also be observed. CDCL itself is the best example as it combines search and resolution. In the most successful solvers, we recently observe the integration of short runs of stochastic local search (SLS) solvers. Further potential for hybrid propositional reasoning can be found, e.g., in Binary Decision Diagrams (BDD).

The idea is to design a SAT solver where the notion of a clause is generalized, such that a clause can be anything that implements a certain interface. A clause could then be a cardinality constraint, DNF formula or a BDD. This way we could integrate available knowledge about various Boolean function representations into SAT solvers. The topic of the thesis is to design and implement a new kind of SAT solver and compare it experimentally with current state-of-the-art SAT solvers.