University of Miami School of Business Administration
The recent improvements in SAT solving algorithms, driven by the quest to solve increasingly complex problem instances, have produced techniques whose objective is to prune large portions of the search space to converge quickly to a solution (for instance, conflict-driven learning). In particular, solutions have been suggested in this area which attacks the problem by attempting to parallelize DPLL-based SAT. However, so far the results have been mixed, which, consequently, have led to a scarcity of research in this space. One of the challenges of this direction is that finding a good partitioning of the space is not straightforward when using a DPLL-based algorithm. Moreover, partitioning the problem limits the benefits that can be ripped from effective learning and good variable ordering heuristics in sequential solvers.