{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,11]],"date-time":"2024-08-11T05:09:26Z","timestamp":1723352966074},"reference-count":0,"publisher":"Association for the Advancement of Artificial Intelligence (AAAI)","issue":"9","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAAI"],"abstract":"The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set (SBS) concept applied to the Boolean Satisfiability Problem (SAT). We call a set of Boolean variables B a \u03c1-backdoor, if for a fraction of at least \u03c1 of possible assignments of variables from B, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas. Clearly, a \u03c1-backdoor with \u03c1=1 is an SBS. For a given set B it is possible to efficiently construct an (\u03b5, \u03b4)-approximation of parameter \u03c1 using the Monte Carlo method. Thus, we define an (\u03b5, \u03b4)-SBS as such a set B for which the conclusion \"parameter \u03c1 deviates from 1 by no more than \u03b5\" is true with probability no smaller than 1 - \u03b4. We consider the problems of finding the minimum SBS and the minimum (\u03b5, \u03b4)-SBS. To solve the former problem, one can use the algorithm described by R. Williams, C. Gomes and B. Selman in 2003. In the paper we propose a new probabilistic algorithm to solve the latter problem, and show that the asymptotic estimation of the worst-case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams et al. For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal (\u03b5, \u03b4)-SBS. Results of computational experiments show that the use of (\u03b5, \u03b4)-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.<\/jats:p>","DOI":"10.1609\/aaai.v36i9.21277","type":"journal-article","created":{"date-parts":[[2022,7,4]],"date-time":"2022-07-04T09:53:43Z","timestamp":1656928423000},"page":"10353-10361","source":"Crossref","is-referenced-by-count":3,"title":["On Probabilistic Generalization of Backdoors in Boolean Satisfiability"],"prefix":"10.1609","volume":"36","author":[{"given":"Alexander","family":"Semenov","sequence":"first","affiliation":[]},{"given":"Artem","family":"Pavlenko","sequence":"additional","affiliation":[]},{"given":"Daniil","family":"Chivilikhin","sequence":"additional","affiliation":[]},{"given":"Stepan","family":"Kochemazov","sequence":"additional","affiliation":[]}],"member":"9382","published-online":{"date-parts":[[2022,6,28]]},"container-title":["Proceedings of the AAAI Conference on Artificial Intelligence"],"original-title":[],"link":[{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/21277\/21026","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/21277\/21026","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,4]],"date-time":"2022-07-04T09:53:43Z","timestamp":1656928423000},"score":1,"resource":{"primary":{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/21277"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,28]]},"references-count":0,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2022,6,30]]}},"URL":"https:\/\/doi.org\/10.1609\/aaai.v36i9.21277","relation":{},"ISSN":["2374-3468","2159-5399"],"issn-type":[{"value":"2374-3468","type":"electronic"},{"value":"2159-5399","type":"print"}],"subject":[],"published":{"date-parts":[[2022,6,28]]}}}