Open Access
Subscription or Fee Access
Decomposing Hard SAT Instances with Metaheuristic Optimization
Abstract
In the article, within the framework of the Boolean Satisfiability problem (SAT), the problem of estimating the hardness of specific Boolean formulas w.r.t. a specific complete SAT solving algorithm is considered. Based on the well-known Strong Backdoor Set (SBS) concept,
we introduce the notion of decomposition hardness (d-hardness). If B is an arbitrary subset of the set of variables occurring in a SAT formula C, and A is an arbitrary complete SAT solver , then the d-hardness expresses an estimate of the hardness of C w.r.t. A and B.
We show that the d-hardness of C w.r.t. a particular B can be expressed in terms of the expected value of a special random variable associated with A, B, and C. For its computational evaluation, algorithms based on the Monte Carlo method can be used. The problem
of finding B with the minimum value of d-hardness is formulated as an optimization problem for a pseudo-Boolean function whose values are calculated as a result of a probabilistic experiment. To minimize this function, we use evolutionary algorithms. In the experimental
part, we demonstrate the applicability of the concept of d-hardness and the methods of its estimation to solving hard unsatisfiable SAT instances.
Keywords
Disclaimer/Regarding indexing issue:
We have provided the online access of all issues and papers to the indexing agencies (as given on journal web site). It’s depend on indexing agencies when, how and what manner they can index or not. Hence, we like to inform that on the basis of earlier indexing, we can’t predict the today or future indexing policy of third party (i.e. indexing agencies) as they have right to discontinue any journal at any time without prior information to the journal. So, please neither sends any question nor expects any answer from us on the behalf of third party i.e. indexing agencies.Hence, we will not issue any certificate or letter for indexing issue. Our role is just to provide the online access to them. So we do properly this and one can visit indexing agencies website to get the authentic information. Also: DOI is paid service which provided by a third party. We never mentioned that we go for this for our any journal. However, journal have no objection if author go directly for this paid DOI service.