nips nips2012 nips2012-267 nips2012-267-reference knowledge-graph by maker-knowledge-mining
Source: pdf
Author: Alex Flint, Matthew Blaschko
Abstract: Boolean satisfiability (SAT) as a canonical NP-complete decision problem is one of the most important problems in computer science. In practice, real-world SAT sentences are drawn from a distribution that may result in efficient algorithms for their solution. Such SAT instances are likely to have shared characteristics and substructures. This work approaches the exploration of a family of SAT solvers as a learning problem. In particular, we relate polynomial time solvability of a SAT subset to a notion of margin between sentences mapped by a feature function into a Hilbert space. Provided this mapping is based on polynomial time computable statistics of a sentence, we show that the existance of a margin between these data points implies the existance of a polynomial time solver for that SAT subset based on the Davis-Putnam-Logemann-Loveland algorithm. Furthermore, we show that a simple perceptron-style learning rule will find an optimal SAT solver with a bounded number of training updates. We derive a linear time computable set of features and show analytically that margins exist for important polynomial special cases of SAT. Empirical results show an order of magnitude improvement over a state-of-the-art SAT solver on a hardware verification task. 1
[1] K. Appel, W. Haken, and J. Koch. Every planar map is four colorable. Illinois J. Math, 21(3):491 – 567, 1977.
[2] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 193–207, 1999.
[3] M. Buro and H. K. Buning. Report on a sat competition. 1992.
[4] C.-L. Chang and R. C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Inc., Orlando, FL, USA, 1st edition, 1997.
[5] S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, STOC ’71, pages 151–158, New York, NY, USA, 1971. ACM.
[6] H. Daum´ , III and D. Marcu. Learning as search optimization: approximate large margin methods for e structured prediction. In International Conference on Machine learning, pages 169–176, 2005.
[7] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Commun. ACM, 5:394–397, July 1962.
[8] M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7:201–215, 1960.
[9] W. F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. The Journal of Logic Programming, 1(3):267 – 284, 1984.
[10] N. E´ n and N. S¨ rensson. An extensible sat-solver. In Theory and Applications of Satisfiability Testing, e o pages 333–336. 2004.
[11] S. Even, A. Itai, and A. Shamir. On the complexity of time table and multi-commodity flow problems. In Symposium on Foundations of Computer Science, pages 184–193, 1975.
[12] M. Fink. Online learning of search heuristics. Journal of Machine Learning Research - Proceedings Track, 2:114–122, 2007.
[13] J. W. Freeman. Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania, 1995.
[14] E. Goldberg and Y. Novikov. Berkmin: A fast and robust sat-solver. In Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings, pages 142 –149, 2002.
[15] J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
[16] J. N. Hooker and V. Vinay. Branching rules for satisfiability. Journal of Automated Reasoning, 15:359– 383, 1995.
[17] F. Hutter, D. Babic, H. H. Hoos, and A. J. Hu. Boosting verification by automatic tuning of decision procedures. In Proceedings of the Formal Methods in Computer Aided Design, pages 27–34, 2007.
[18] R. G. Jeroslow and J. Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167–187, 1990.
[19] H. A. Kautz. Deconstructing planning as satisfiability. In Proceedings of the Twenty-first National Conference on Artificial Intelligence (AAAI-06), 2006.
[20] M. Kearns, M. Li, L. Pitt, and L. Valiant. On the learnability of boolean formulae. In Proceedings of the nineteenth annual ACM symposium on Theory of computing, pages 285–295, 1987.
[21] D. Le Berra and O. Roussel. Sat competition 2009. http://www.satcompetition.org/2009/.
[22] I. Lynce and J. a. Marques-Silva. Efficient haplotype inference with boolean satisfiability. In Proceedings of the 21st national conference on Artificial intelligence - Volume 1, pages 104–109. AAAI Press, 2006.
[23] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: engineering an efficient sat solver. In Design Automation Conference, 2001. Proceedings, pages 530 – 535, 2001.
[24] F. Rosenblatt. The Perceptron: A probabilistic model for information storage and organization in the brain. Psychological Review, 65:386–408, 1958.
[25] W. Ruml. Adaptive Tree Search. PhD thesis, Harvard University, 2002.
[26] J. a. P. M. Silva. The impact of branching heuristics in propositional satisfiability algorithms. In Proceedings of the 9th Portuguese Conference on Artificial Intelligence: Progress in Artificial Intelligence, EPIA ’99, pages 62–74, London, UK, 1999. Springer-Verlag.
[27] L. Xu, F. Hutter, H. H. Hoos, and K. Leyton-Brown. Satzilla: portfolio-based algorithm selection for sat. J. Artif. Int. Res., 32:565–606, June 2008.
[28] R. Zabih. A rearrangement search strategy for determining propositional satisfiability. In in Proceedings of the National Conference on Artificial Intelligence, pages 155–160, 1988. 9