Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability

摘要: This paper addresses the interaction between randomization, with restart strategies, andl earning, an often crucial technique for proving unsatisfiability. We use instances of SAT from hardware verification domain to provide evidence that randomization can indeed be essential in solving real-world satisfiable SAT. More interestingly, our results indicate randomized restarts and learning may cooperate both satisfiability andu nsatisfiability. Finally, we utilize expand idea algorithm portfolio design propose alternative approach harduns atisfiable