An SVM-Based Prediction Method for Solving SAT Problems
|
摘要
We show how Support vector machines(SVM) can be applied to the Satisfiability(SAT) problem and how their prediction results can be naturally applied to both incomplete and complete SAT solvers. SVM is used for the classification of the variables in the SAT problem and the classification results are the assignment of the variables. And we also present empirical results of applying SVM to instances of the SAT problem from the Center for Discrete Mathematics and Theoretical Computer Science(DIMACS) archive and compare them against the results of other incomplete and complete algorithms for the SAT problem.
We show how Support vector machines(SVM) can be applied to the Satisfiability(SAT) problem and how their prediction results can be naturally applied to both incomplete and complete SAT solvers. SVM is used for the classification of the variables in the SAT problem and the classification results are the assignment of the variables. And we also present empirical results of applying SVM to instances of the SAT problem from the Center for Discrete Mathematics and Theoretical Computer Science(DIMACS) archive and compare them against the results of other incomplete and complete algorithms for the SAT problem.
We show how Support vector machines(SVM) can be applied to the Satisfiability(SAT) problem and how their prediction results can be naturally applied to both incomplete and complete SAT solvers. SVM is used for the classification of the variables in the SAT problem and the classification results are the assignment of the variables. And we also present empirical results of applying SVM to instances of the SAT problem from the Center for Discrete Mathematics and Theoretical Computer Science(DIMACS) archive and compare them against the results of other incomplete and complete algorithms for the SAT problem.
引文
[1]F.Lardeux,F.Saubion and J.K.Hao,“GASAT:Agenetic local search algorithm for the satisfiability problem”,Evolutionary Computation,Vol.14,No.2,pp.223-253,2006.
[2]S.A.Cook,“The complexity of theorem-proving procedures”,Proc.of ACM Symposium on Theory of Computing,Shaker Heights,Ohio,USA,pp.151-158,1971.
[3]B.A.Trakhtenbrot,“A survey of russian approaches to perebor(brute-force searches)algorithms”,IEEE Annals of the History of Computing,Vol.6,No.4,pp.384-400,1984.
[4]J.Rintanen,K.Heljanko and I.Niemel?,“Planning as satisfiability:Parallel plans and algorithms for plan search”,Artificial Intelligence,Vol.170,No.12,pp.1031-1080,2006.
[5]A.Biere,A.Cimatti,E.M.Clarke,et al.,“Symbolic model checking using SAT procedures instead of BDDs”,Proc.of Design Automation Conference,New Orleans,Louisiana,USA,pp.317-320,1999.
[6]B.Selman,H.Levesque and D.Mitchell,“A new method for solving hard satisfiability problems”,Proc.of Tenth National Conference on Artificial Intelligence,San Jose,California,USA,pp.440-446,1992.
[7]Y.Shang and B.W.Wah,“A discrete Lagrangian-based global-search method for solving satisfiability problems”,Journal of Global Optimization,Vol.12,No.1,pp.61-99,1998.
[8]Z.Wu and B.W.Wah,“An efficient global-search strategy in discrete lagrangian methods for solving hard satisfiability problems”,Proc.of Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence,Austin,Texas,USA,pp.310-315,2000.
[9]H.Zhang,“SATO:An efficient propositional prover”,Proc.of International Conference on Automated Deduction,London,UK,pp.272-275,2006.
[10]J.W.Freeman,“Improvements to propositional satisfiability search algorithms”,Ph.D.Thesis,University of Pennsylvania,USA,1995.
[11]J.P.Marquessilva and K.A.Sakallah,“GRASP:A search algorithm for propositional satisfiability”,IEEE Transactions on Computers,Vol.48,No.5,pp.506-521,1999.
[12]N.Eén and N.S?rensson,“An extensible SAT-solver”,Proc.of International Conference on Theory and Applications of Satisfiability Testing,Santa Margherita Ligure,Italy,pp.502-518,2003.
[13]M.W.Moskewicz,C.F.Madigan,Y.Zhao,et al.,“Chaff:Engineering an efficient Sat solver”,Proc.of the 38th Annual Design Automation Conference,Nevada,USA,pp.530-535,2001.
[14]S.W.Cai and K.L.Su,“Configuration checking with aspiration in local search for SAT”,Proc.of the Twenty-sixth AAAI Conference on Artificial Intelligence,pp.434-440,2012.
[15]D.L.Berre and S.Roussel,“Sat4j 2.3.2:On the fly solver configuration system description”,Journal on Satisfiability Boolean Modeling&Computation,Vol.8,pp.197-202,2014.
[16]M.Zbigniew,“Genetic algorithms+data structures=evolution programs”,Computational Statistics&Data Analysis,Vol.24,No.3,pp.372-373,1999.
[17]J.G.Klincewicz,“Avoiding local optima in thep-hub location problem using tabu search and GRASP”,Annals of Operations Research,Vol.40,No.1,pp.283-302,1992.
[18]V.?erny,“Thermodynamical approach to the traveling salesman problem:An efficient simulation algorithm”,Journal of Optimization Theory and Applications,Vol.45,No.1,pp.41-51,1985.
[19]J.Liu,W.C.Zhong,F.Liu,et al.,“An organizational evolutionary algorithm for SAT problem”,Chinese Journal of Computers,Vol.27,No.10,pp.1422-1428,2004.(in Chinese)
[20]C.Cortes and V.Vapnik,“Support-vector networks”,Machine Learning,Vol.20,No.3,pp.273-297,1995.
[21]R.G.Jeroslow and J.Wang,“Solving propositional satisfiability problems”,Annals of Mathematics&Artificial Intelligence,Vol.1,No.1,pp.167-187,1990.
[22]C.C.Chang and C.J.Lin,“LIBSVM:A library for support vector machines”,ACM Transactions on Intelligent Systems&Technology,Vol.2,No.3,pp.389-396,2011.
http://www.satlib.org/
[2]S.A.Cook,“The complexity of theorem-proving procedures”,Proc.of ACM Symposium on Theory of Computing,Shaker Heights,Ohio,USA,pp.151-158,1971.
[3]B.A.Trakhtenbrot,“A survey of russian approaches to perebor(brute-force searches)algorithms”,IEEE Annals of the History of Computing,Vol.6,No.4,pp.384-400,1984.
[4]J.Rintanen,K.Heljanko and I.Niemel?,“Planning as satisfiability:Parallel plans and algorithms for plan search”,Artificial Intelligence,Vol.170,No.12,pp.1031-1080,2006.
[5]A.Biere,A.Cimatti,E.M.Clarke,et al.,“Symbolic model checking using SAT procedures instead of BDDs”,Proc.of Design Automation Conference,New Orleans,Louisiana,USA,pp.317-320,1999.
[6]B.Selman,H.Levesque and D.Mitchell,“A new method for solving hard satisfiability problems”,Proc.of Tenth National Conference on Artificial Intelligence,San Jose,California,USA,pp.440-446,1992.
[7]Y.Shang and B.W.Wah,“A discrete Lagrangian-based global-search method for solving satisfiability problems”,Journal of Global Optimization,Vol.12,No.1,pp.61-99,1998.
[8]Z.Wu and B.W.Wah,“An efficient global-search strategy in discrete lagrangian methods for solving hard satisfiability problems”,Proc.of Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence,Austin,Texas,USA,pp.310-315,2000.
[9]H.Zhang,“SATO:An efficient propositional prover”,Proc.of International Conference on Automated Deduction,London,UK,pp.272-275,2006.
[10]J.W.Freeman,“Improvements to propositional satisfiability search algorithms”,Ph.D.Thesis,University of Pennsylvania,USA,1995.
[11]J.P.Marquessilva and K.A.Sakallah,“GRASP:A search algorithm for propositional satisfiability”,IEEE Transactions on Computers,Vol.48,No.5,pp.506-521,1999.
[12]N.Eén and N.S?rensson,“An extensible SAT-solver”,Proc.of International Conference on Theory and Applications of Satisfiability Testing,Santa Margherita Ligure,Italy,pp.502-518,2003.
[13]M.W.Moskewicz,C.F.Madigan,Y.Zhao,et al.,“Chaff:Engineering an efficient Sat solver”,Proc.of the 38th Annual Design Automation Conference,Nevada,USA,pp.530-535,2001.
[14]S.W.Cai and K.L.Su,“Configuration checking with aspiration in local search for SAT”,Proc.of the Twenty-sixth AAAI Conference on Artificial Intelligence,pp.434-440,2012.
[15]D.L.Berre and S.Roussel,“Sat4j 2.3.2:On the fly solver configuration system description”,Journal on Satisfiability Boolean Modeling&Computation,Vol.8,pp.197-202,2014.
[16]M.Zbigniew,“Genetic algorithms+data structures=evolution programs”,Computational Statistics&Data Analysis,Vol.24,No.3,pp.372-373,1999.
[17]J.G.Klincewicz,“Avoiding local optima in thep-hub location problem using tabu search and GRASP”,Annals of Operations Research,Vol.40,No.1,pp.283-302,1992.
[18]V.?erny,“Thermodynamical approach to the traveling salesman problem:An efficient simulation algorithm”,Journal of Optimization Theory and Applications,Vol.45,No.1,pp.41-51,1985.
[19]J.Liu,W.C.Zhong,F.Liu,et al.,“An organizational evolutionary algorithm for SAT problem”,Chinese Journal of Computers,Vol.27,No.10,pp.1422-1428,2004.(in Chinese)
[20]C.Cortes and V.Vapnik,“Support-vector networks”,Machine Learning,Vol.20,No.3,pp.273-297,1995.
[21]R.G.Jeroslow and J.Wang,“Solving propositional satisfiability problems”,Annals of Mathematics&Artificial Intelligence,Vol.1,No.1,pp.167-187,1990.
[22]C.C.Chang and C.J.Lin,“LIBSVM:A library for support vector machines”,ACM Transactions on Intelligent Systems&Technology,Vol.2,No.3,pp.389-396,2011.
http://www.satlib.org/