- A Comparison of SAT Heuristic-Based Markov Chains
- Project Year:
2018
- REU Student (s):
Sherry Sarkar | Georgia Institute of Technology-Main Campus GA
- Student 1 Institution:
Georgia Institute of Technology-Main Campus
- Project Mentor:
Periklis Papakonstantinou
- Project Mentor Area:
Management Science and Information Systems
- Project Abstract:
Schoning's algorithm and the break algorithm are SAT heuristic based Markov chains
that have performed exceptionally fast compared to a brute force exponential approach. These
Markov chains have been known to work well on random SAT instances over industrial SAT instances.
In the first half of this paper, we discuss some sufficient conditions and examples in which one
algorithm would perform better than the other in an effort to answer the general question of which
SAT solver works better given a random SAT formula. In the second half of this paper, we construct
a set of operations on Markov chains that preserve mixing time. Two operations in particular have
been stated and proved here - the splitting of a state and the merge of two states.
