Finding cores using a Brouwer's fixed point approximation algorithm
Siert Wieringa · 2007
In this Master’s thesis a novel algorithm for finding unsatisfiable cores in sets of Boolean constraints is presented. The algorithm is based on a Brouwers’ fixed point approximation algorithm, which makes its approach to the satisfiability problem unique. An important part of this project was the development of a core finder, named DUC Hunt, which contains an implementation of the algorithm. DUC Hunt has various options that can be used to make it either find multiple cores or to make it find a guaranteed MUS. Using that last feature it can also be used as a “MUS prover” for cores found by other core finders. Although the algorithm is in theory applicable to finding cores in sets of Boolean constraints in general its current implementation is limited to finding cores in sets of clauses. For the application of DUC Hunt to proving that an unsatisfiable formula is a MUS an approach that differs from the algorithm presented was found while evaluating the algorithm. This new approach resulted in a practically useful and well performing MUS prover. Besides that application the current implementation of the algorithm works correctly but it is too slow to be of practical use. As this is a first study into the possibilities of applying a Brouwer’s fixed point approximation algorithm to Boolean satisfiability this leads us to propose future research and implementation improvements.