Document Open Access Logo

Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms

Authors Alexander Semenov, Daniil Chivilikhin, Artem Pavlenko, Ilya Otpuschennikov, Vladimir Ulyantsev, Alexey Ignatiev

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.47.pdf
  • Filesize: 0.99 MB
  • 18 pages

Document Identifiers

Author Details

Alexander Semenov
  • ITMO University, St. Petersburg, Russia
Daniil Chivilikhin
  • ITMO University, St. Petersburg, Russia
Artem Pavlenko
  • ITMO University, St. Petersburg, Russia
  • JetBrains Research, St. Petersburg, Russia
Ilya Otpuschennikov
  • ISDCT SB RAS, Irkutsk, Russia
Vladimir Ulyantsev
  • ITMO University, St. Petersburg, Russia
Alexey Ignatiev
  • Monash University, Melbourne, Australia

Funding

This work was supported by the Ministry of Science and Higher Education of Russian Federation, research project no. 075-03-2020-139/2 (goszadanie no. 2019-1339). Ilya Otpuschennikov’s research was funded by Ministry of Science and Higher Education of Russian Federation, project with no. of state registration: 121041300065-9. Artem Pavlenko was supported by JetBrains Research.

Cite AsGet BibTex

Alexander Semenov, Daniil Chivilikhin, Artem Pavlenko, Ilya Otpuschennikov, Vladimir Ulyantsev, and Alexey Ignatiev. Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 47:1-47:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.47

Abstract

Propositional satisfiability (SAT) solvers are deemed to be among the most efficient reasoners, which have been successfully used in a wide range of practical applications. As this contrasts the well-known NP-completeness of SAT, a number of attempts have been made in the recent past to assess the hardness of propositional formulas in conjunctive normal form (CNF). The present paper proposes a CNF formula hardness measure which is close in conceptual meaning to the one based on Backdoor set notion: in both cases some subset B of variables in a CNF formula is used to define the hardness of the formula w.r.t. this set. In contrast to the backdoor measure, the new measure does not demand the polynomial decidability of CNF formulas obtained when substituting assignments of variables from B to the original formula. To estimate this measure the paper suggests an adaptive (ε,δ)-approximation probabilistic algorithm. The problem of looking for the subset of variables which provides the minimal hardness value is reduced to optimization of a pseudo-Boolean black-box function. We apply evolutionary algorithms to this problem and demonstrate applicability of proposed notions and techniques to tests from several families of unsatisfiable CNF formulas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Hardware → Theorem proving and SAT solving
  • Theory of computation → Optimization with randomized search heuristics
  • Mathematics of computing → Combinatorial optimization
Keywords
  • SAT solving
  • Boolean formula hardness
  • Backdoors
  • Evolutionary algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. In STOC, pages 448-456, 2002. Google Scholar
  2. Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Measuring the hardness of SAT instances. In AAAI, pages 222-228, 2008. Google Scholar
  3. Gilles Audemard, Jean-Marie Lagniez, and Laurent Simon. Improving Glucose for incremental SAT solving with assumptions: Application to MUS extraction. In SAT, pages 309-317, 2013. Google Scholar
  4. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res., 22:319-351, 2004. Google Scholar
  5. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In FOCS, pages 274-282, 1996. Google Scholar
  6. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Comb., 24(4):585-603, 2004. Google Scholar
  7. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  8. Christian Bessiere, George Katsirelos, Nina Narodytska, and Toby Walsh. Circuit complexity and decompositions of global constraints. In IJCAI, pages 412-418, 2009. Google Scholar
  9. Armin Biere. CaDiCaL at the SAT Race 2019. In SAT Race, pages 8-9, 2019. Google Scholar
  10. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability (Second Edition), 2021. Google Scholar
  11. Christian Blum and Andrea Roli. Metaheuristics in combinatorial optimization: Overview and conceptual comparison. ACM Comput. Surv., 35(3):268-308, 2003. Google Scholar
  12. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. Propositional proof systems based on maximum satisfiability. Artif. Intell., 300:pages to appear, 2021. Google Scholar
  13. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. Exponential separations between restricted resolution and cutting planes proof systems. In FOCS, pages 638-647, 1998. Google Scholar
  14. Edmund Burke and Graham Kendall. Search Methodologies. Springer, 2014. Google Scholar
  15. Samuel R. Buss and György Turán. Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci., 62(3):311-317, 1988. Google Scholar
  16. Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Inc., 1973. Google Scholar
  17. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In TACAS, pages 168-176, 2004. Google Scholar
  18. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. Google Scholar
  19. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discret. Appl. Math., 18(1):25-38, 1987. Google Scholar
  20. Thomas Cormen, Charles Leiserson, and Ronald Rivest. Introduction to Algorithms. MIT Press, 1990. Google Scholar
  21. Nicolas T. Courtois and Gregory V. Bard. Algebraic cryptanalysis of the data encryption standard. In IMACC, pages 152-169, 2007. Google Scholar
  22. Guoli Ding, Robert F. Lax, Jianhua Chen, Peter P. Chen, and Brian D. Marx. Transforms of pseudo-boolean random variables. Discret. Appl. Math., 158(1):13-24, 2010. Google Scholar
  23. Benjamin Doerr, Huu Phuoc Le, Régis Makhmara, and Ta Duy Nguyen. Fast genetic algorithms. In GECCO, pages 777-784, 2017. Google Scholar
  24. William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Log. Program., 1(3):267-284, 1984. Google Scholar
  25. Stefan Droste, Thomas Jansen, and Ingo Wegener. On the analysis of the (1+1) evolutionary algorithm. Theor. Comput. Sci., 276(1-2):51-81, 2002. Google Scholar
  26. Tobias Eibach, Enrico Pilz, and Gunnar Völkel. Attacking bivium using SAT solvers. In SAT, pages 63-76, 2008. Google Scholar
  27. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Inf. Comput., 171(1):84-97, 2001. Google Scholar
  28. William Feller. An Introduction to probability theory and its applications, volume 2. John Wiley & Sons, Inc., 2 edition, 1971. Google Scholar
  29. William H. Gates and Christos H. Papadimitriou. Bounds for sorting by prefix reversal. Discret. Math., 27(1):47-57, 1979. Google Scholar
  30. Carla P. Gomes and Ashish Sabharwal. Exploiting runtime variation in complete solvers. In Handbook of Satisfiability (Second Edition), pages 463-480. IOS Press, 2021. Google Scholar
  31. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. Google Scholar
  32. Marijn Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In HVC, pages 50-65, 2011. Google Scholar
  33. Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown, and Thomas Stützle. Paramils: An automatic algorithm configuration framework. J. Artif. Intell. Res., 36:267-306, 2009. Google Scholar
  34. Frank Hutter, Marius Lindauer, Adrian Balint, Sam Bayless, Holger H. Hoos, and Kevin Leyton-Brown. The configurable SAT solver challenge (CSSC). Artif. Intell., 243:1-25, 2017. Google Scholar
  35. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pages 428-437, 2018. Google Scholar
  36. Richard M. Karp, Michael Luby, and Neal Madras. Monte-carlo approximation algorithms for enumeration problems. J. Algorithms, 10(3):429-448, 1989. Google Scholar
  37. Stepan Kochemazov and Oleg Zaikin. ALIAS: A modular tool for finding backdoors for SAT. In SAT, pages 419-427, 2018. Google Scholar
  38. Daniel Kroening. Software verification. In Handbook of Satisfiability (Second Edition), pages 791-818, 2021. Google Scholar
  39. Andreas Kuehlmann and Florian Krohm. Equivalence checking using cuts and heaps. In DAC, pages 263-268, 1997. Google Scholar
  40. Oliver Kullmann. Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Ann. Math. Artif. Intell., 40(3-4):303-352, 2004. Google Scholar
  41. Sean Luke. Essentials of Metaheuristics. Lulu, second edition, 2013. Google Scholar
  42. Joao Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability (Second Edition), pages 133-182. IOS Press, 2021. Google Scholar
  43. Nicholas Metropolis and S. Ulam. The Monte Carlo Method. J. Amer. Statistical Assoc., 44(247):335-341, 1949. Google Scholar
  44. Heinz Mühlenbein. How genetic algorithms really work: Mutation and hillclimbing. In PPSN, pages 15-26, 1992. Google Scholar
  45. Jakob Nordström. On the interplay between proof complexity and SAT solving. SIGLOG News, 2(3):19-44, 2015. Google Scholar
  46. Ilya V. Otpuschennikov, Alexander A. Semenov, Irina Gribanova, Oleg Zaikin, and Stepan Kochemazov. Encoding cryptographic functions to SAT using TRANSALG system. In ECAI, pages 1594-1595, 2016. Google Scholar
  47. Artem Pavlenko, Alexander A. Semenov, and Vladimir Ulyantsev. Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis. In EvoApplications, pages 237-253, 2019. Google Scholar
  48. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. Google Scholar
  49. Stuart J. Russell and Peter Norvig. Artificial Intelligence: A Modern Approach (4th Edition). Pearson, 2020. Google Scholar
  50. Alexander Semenov and Oleg Zaikin. Algorithm for finding partitionings of hard variants of boolean satisfiability problem with application to inversion of some cryptographic functions. SpringerPlus, 5(1), 2006. Article no. 554. Google Scholar
  51. Alexander A. Semenov, Ilya V. Otpuschennikov, Irina Gribanova, Oleg Zaikin, and Stepan Kochemazov. Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Log. Methods Comput. Sci., 16(1), 2020. Google Scholar
  52. Alexander A. Semenov, Oleg Zaikin, Ilya V. Otpuschennikov, Stepan Kochemazov, and Alexey Ignatiev. On cryptographic attacks using backdoors for SAT. In AAAI, pages 6641-6648, 2018. Google Scholar
  53. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In SAT, pages 244-257, 2009. Google Scholar
  54. Ivor T. A. Spence. Weakening cardinality constraints creates harder satisfiability benchmarks. ACM J. Exp. Algorithmics, 20:1.4:1-1.4:14, 2015. Google Scholar
  55. Grigoriy Tseitin. On the complexity of derivation in propositional calculus. Studies in Constr. Math. and Math. Logic, pages 115-125, 1970. Google Scholar
  56. Alasdair Urquhart. The complexity of propositional proofs. Bull. Symb. Log., 1(4):425-467, 1995. Google Scholar
  57. Ingo Wegener. Theoretical aspects of evolutionary algorithms. In ICALP, pages 64-78, 2001. Google Scholar
  58. Samuel S. Wilks. Mathematical statistics. John Wiley and Sons, 1962. Google Scholar
  59. Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. In IJCAI, pages 1173-1178, 2003. Google Scholar
  60. Oleg S. Zaikin and Stepan E. Kochemazov. On black-box optimization in divide-and-conquer SAT solving. Optimization Methods and Software, pages 1-25, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact