Using support vector machine to evaluate usefulness of conflict clauses in CDCL derivation

Oleg Zaikin, Stepan Kochemazov

Abstract


Many state-of-the-art algorithms for solving Boolean satisfiability problem (SAT) are based on the CDCL algorithm. CDCL generates a lot of so-called conflict clauses that correspond to traversed branches of a tree of possible solutions. To maintain high speed of CDCL-based algorithms, it is required to periodically remove some conflict clauses. Therefore, the problem of evaluating conflict clauses usefulness arises. In the present study, a heuristic for solving this problem is proposed that is based on support vector machines. On the first stage, a family of simplified versions of an original SAT instance is constructed, then they are solved via some SAT solver. On the second stage, a support vector machine is trained. During this process, a conflict clause is considered useful if it is not removed at the time of finding a solution of at least one simplified subproblem. On the third stage, an original SAT instance is solved, while the usefulness of some conflict clauses is evaluated by the trained support vector machine. Based on the proposed heuristic, a modified version of a state-of-the-art CDCL solver is implemented. According to the computational experiments, the modified version is more efficient on a few families of hard SAT instances.

Full Text:

PDF (Russian)

References


M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co. New York, NY, USA, 1979.

J. P. Marques-Silva, K. A. Sakallah, "GRASP-a new search algorithm for satisfiability," in Proc. IEEE International Conference on Computer-Aided Design (ICCAD), 1996, pp. 220–227.

J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, "Learning rate based branching heuristic for SAT solvers," in Proc. Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9710, 2016, pp 123-140.

M. N. Katehakis, A. F. Veinott, "The Multi-Armed Bandit Problem: Decomposition and Computation," Mathematics of Operations Research, vol. 12 (2), 1995, pp. 262–268.

C. Corinna, V. N. Vapnik, "Support-vector networks," Machine Learning, vol. 20 (3), 1995, pp. 273–297.

O. S. Zaikin, "A parallel SAT solving algorithm based on improved handling of conflict clauses," In Proc. International young scientists conference in high performance computing and simulation, Procedia computer science, vol. 12083, 2017, pp. 103-111.

G. Audemard, L. Simon, "On the Glucose SAT solver," International Journal on Artificial Intelligence Tools, vol. 27 (1), 2018, pp. 1-25.

M. Heule, W. A. Hunt Jr., and N. Wetzler, "Trimming while checking clausal proofs," In Proc. FMCAD 2013, pp. 181-188.

A general purpose C++ library Dlib. URL: http://dlib.net.

O. S. Zaikin, S. E. Kochemazov. “"An Improved SAT-Based Guess-and-Determine Attack on the Alternating Step Generator," In Proc. International Conference on Information Security, Lecture Notes in Computer Science, vol. 10599, 2017, pp. 21–38.

A. A. Semenov, O. S. Zaikin, D. V. Bespalov, and M. A. Posypkin, "Parallel Logical Cryptanalysis of the Generator A5/1 in BNB-Grid System," In Proc. Parallel computing technologies (PaCT), Lecture Notes in Computer Science, vol. 6873, 2011, pp 473-483.

O. S. Zaikin, "Application of parallel SAT solving algorithms for cryptanalysis of the shrinking and self-shrinking keystream generators," International Journal of Open Information Technologies, vol. 6 (10), 2018, pp. 29-33.

I. V. Otpuschennikov, A. A. Semenov, I. A. Gribanova, O. S. Zaikin, and S. E. Kochemazov. "Encoding cryptographic functions to SAT using Transalg system," In Proc. ECAI’2016, Frontiers in Artificial Intelligence and Applications, vol. 285, 2016, pp. 1594-1595.

Irkutsk supercomputing center SB RAS. URL: http://hpc.icc.ru.


Refbacks

  • There are currently no refbacks.


Abava  Absolutech Fruct 2020

ISSN: 2307-8162