HUANG Shaobin, LI Ya, LI Yanmei. An SVM-Based Prediction Method for Solving SAT Problems[J]. Chinese Journal of Electronics, 2019, 28(2): 246-252. doi: 10.1049/cje.2019.01.004
Citation: HUANG Shaobin, LI Ya, LI Yanmei. An SVM-Based Prediction Method for Solving SAT Problems[J]. Chinese Journal of Electronics, 2019, 28(2): 246-252. doi: 10.1049/cje.2019.01.004

An SVM-Based Prediction Method for Solving SAT Problems

doi: 10.1049/cje.2019.01.004
More Information
  • Corresponding author: LI Ya (corresponding author) was born in 1985. She is a Ph.D. candidate in College of Computer Science and Technology of Harbin Engineering University. Her research area covers software engineering, fault locations and model checking. (
  • Received Date: 2016-06-12
  • Rev Recd Date: 2017-02-13
  • Publish Date: 2019-03-10
  • 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.
  • loading
  • F. Lardeux, F. Saubion and J.K. Hao, “GASAT: A genetic local search algorithm for the satisfiability problem”, Evolutionary Computation, Vol.14, No.2, pp.223-253, 2006.
    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.
    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.
    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.
    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.
    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.
    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.
    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.
    H. Zhang, “SATO: An efficient propositional prover”, Proc. of International Conference on Automated Deduction, London, UK, pp.272-275, 2006.
    J.W. Freeman, “Improvements to propositional satisfiability search algorithms”, Ph.D.Thesis, University of Pennsylvania, USA, 1995.
    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.
    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.
    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.
    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.
    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.
    M. Zbigniew, “Genetic algorithms+ data structures= evolution programs”, Computational Statistics & Data Analysis, Vol.24, No.3, pp.372-373, 1999.
    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.
    V. Černý, “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.
    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)
    C. Cortes and V. Vapnik, “Support-vector networks”, Machine Learning, Vol.20, No.3, pp.273-297, 1995.
    R.G. Jeroslow and J. Wang, “Solving propositional satisfiability problems”, Annals of Mathematics & Artificial Intelligence, Vol.1, No.1, pp.167-187, 1990.
    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.
  • 加载中


    通讯作者: 陈斌,
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (139) PDF downloads(233) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint