Dominik Wagner:
SAT-Solving with a Condensed Representation of Periodic Patterns
Kurzbeschreibung
In light of the established NP-hardness of the Boolean Satisfiability Problem (SAT), contemporary SAT-solvers showcase remarkable prowess in tackling even large instances of the problem. This proficiency has been honed over decades through the refinement of two prominent solving paradigms: the DPLL-algorithm and stochastic local search (SLS). The former stands out as the preferred choice for exact solutions, while the latter sacrifices reliability in favor of speed.
In this work we try to break away from these established paradigms by introducing an alternative approach to solving the SAT-Problem. Similar to DPLL, our method yields exact results. However, instead of systematically searching for a singular solution, we leverage periodic patterns inherent in the structure of truth tables. These patterns allow us to model the entire solution space of a formula in a highly condensed form, reminiscent of a binary decision diagram. Although still inherently exponential, our algorithm exhibits promising performance characteristics and provides all solutions for a given problem. Furthermore, we give a comprehensive overview on our optimization efforts and provide performance metrics based on test results from variously sized uniform random 3-SAT formulas to underscore the algorithm's effectiveness.