Cache Conscious Data Structures for Boolean Satisfiability Solvers

摘要: Current SAT solvers are well engineered and highly efficient, significant research effort has been put into creating data structures that can produce maximal efficiency for the core propagation engine within solvers. However, there is still substantial room improvement. As disparity between CPU speeds cache sizes have increased, conscious algorithms become very important. They even more important in context of parallel solving, as issues like contention main memory dramatically slow down a solver. We present series structure algorithmic modifications able to increase speed MiniSat 2.0 by an average 80% on set medium sized industrial instances, parallelized version running with 8 threads 140% those same instances.