Affordable Access

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

Authors
Publisher
Springer Verlag
Publication Date
Disciplines
  • Computer Science
  • Design

Abstract

Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability Lu´ıs Baptista and Joa˜o Marques-Silva Department of Informatics, Technical University of Lisbon, IST/INESC/CEL, Lisbon, Portugal {lmtb,[email protected] Abstract. This paper addresses the interaction between randomization, with restart strategies, and learning, an often crucial technique for prov- ing unsatisfiability. We use instances of SAT from the hardware veri- fication domain to provide evidence that randomization can indeed be essential in solving real-world satisfiable instances of SAT. More inter- estingly, our results indicate that randomized restarts and learning may cooperate in proving both satisfiability and unsatisfiability. Finally, we utilize and expand the idea of algorithm portfolio design to propose an alternative approach for solving hard unsatisfiable instances of SAT. 1 Introduction Recent work on the Satisfiability Problem (SAT) has provided experimental and theoretical evidence that randomization and restart strategies can be quite ef- fective at solving hard satisfiable instances of SAT [4]. Indeed, backtrack search algorithms, randomized and run with restarts, were shown to perform signifi- cantly better on specific problem instances. Recent work has also demonstrated the usefulness of learning in solving hard instances of SAT [2,6,8]. Learning, in the form of clause (nogood) recording, is the underlying mechanism by which non- chronological backtracking, relevance-based learning, and other search pruning techniques, can be implemented. In this paper we propose to conduct a preliminary study of the interaction be- tween randomization and learning in solving real-world hard satisfiable instances of SAT. Moreover, we propose a new problem solving strategy for solving hard unsatisfiable instances of SAT. Throughout the paper we focus on real-world instances of SAT from the hardware verification domain, namely superscalar processor verification [7]1. These i

There are no comments yet on this publication. Be the first to share your thoughts.