zbMATH — the first resource for mathematics

Using randomization and learning to solve hard real-world instances of satisfiability. (English) Zbl 1044.68736
Dechter, Rina (ed.), Principles and practice of constraint programming - CP 2000. 6th international conference, Singapore, September 18–21, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41053-8). Lect. Notes Comput. Sci. 1894, 489-494 (2000).
Summary: This paper addresses the interaction between randomization, with restart strategies, and learning, an often crucial technique for proving unsatisfiability. We use instances of SAT from the hardware verification domain to provide evidence that randomization can indeed be essential in solving real-world satisfiable instances of SAT. More interestingly, 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.
For the entire collection see [Zbl 0947.00041].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T05 Learning and adaptive systems in artificial intelligence
68T27 Logic in artificial intelligence
Full Text: Link