Finding Effective SAT Partitionings Via Black-Box Optimization

Alexander Semenov (), Oleg Zaikin () and Stepan Kochemazov ()
Additional contact information
Alexander Semenov: Matrosov Institute for System Dynamics and Control Theory SB RAS
Oleg Zaikin: Matrosov Institute for System Dynamics and Control Theory SB RAS
Stepan Kochemazov: Matrosov Institute for System Dynamics and Control Theory SB RAS

A chapter in Black Box Optimization, Machine Learning, and No-Free Lunch Theorems, 2021, pp 319-355 from Springer

Abstract: Abstract In the present chapter we study one method for partitioning hard instances of the Boolean satisfiability problem (SAT). It uses a subset of a set of variables of an original formula to partition it into a family of subproblems that are significantly easier to solve individually. While it is usually very hard to estimate the time required to solve a hard SAT instance without actually solving it, the partitionings of the presented kind make it possible to naturally construct such estimations via the well-known Monte Carlo method. We show that the problem of finding a SAT partitioning with minimal estimation of time required to solve all subproblems can be formulated as the problem of minimizing a special pseudo-Boolean black-box function. The experimental part of the paper clearly shows that in the context of the proposed approach relatively simple black-box optimization algorithms show good results in application to minimization of the functions of the described kind even when faced with hard SAT instances that encode problems of finding preimages of cryptographic functions.

Date: 2021
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:spochp:978-3-030-66515-9_11

Ordering information: This item can be ordered from
http://www.springer.com/9783030665159

DOI: 10.1007/978-3-030-66515-9_11

Access Statistics for this chapter

More chapters in Springer Optimization and Its Applications from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().