zbMATH — the first resource for mathematics

Decomposing SAT instances with pseudo backbones. (English) Zbl 1453.68170
Hu, Bin (ed.) et al., Evolutionary computation in combinatorial optimization. 17th European conference, EvoCOP 2017, Amsterdam, The Netherlands, April 19–21, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10197, 75-90 (2017).
Summary: Two major search paradigms have been proposed for SAT solving: Systematic Search (SS) and Stochastic Local Search (SLS). In SAT competitions, while SLS solvers are effective on uniform random instances, SS solvers dominate SLS solvers on application instances with internal structures. One important structural property is decomposability. SS solvers have long been exploited the decomposability of application instances with success. We conjecture that SLS solvers can be improved by exploiting decomposability of application instances, and propose the first step toward exploiting decomposability with SLS solvers using pseudo backbones. We then propose two SAT-specific optimizations that lead to better decomposition than on general pseudo Boolean optimization problems. Our empirical study suggests that pseudo backbones can vastly simplify SAT instances, which further results in decomposing the instances into thousands of connected components. This decomposition serves as a key stepping stone for applying the powerful recombination operator, partition crossover, to the SAT domain. Moreover, we establish a priori analysis for identifying problem instances with potential decomposability using visualization of MAXSAT instances and treewidth.
For the entire collection see [Zbl 1360.68014].
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68R07 Computational aspects of satisfiability
90C59 Approximation methods and heuristics in mathematical programming
Full Text: DOI
[1] Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151-158. ACM (1971)
[2] Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7-34 (2001) · Zbl 0985.68038
[3] Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2), 73-106 (2003) · Zbl 1069.68119
[4] Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell. 224, 103-118 (2015) · Zbl 1344.68205
[5] Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502-518. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_37 · Zbl 1204.68191
[6] Tompkins, D.A.D., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306-320. Springer, Heidelberg (2005). doi:10.1007/11527695_24 · Zbl 1122.68620
[7] The International SAT Competitions Webpage. http://www.satcompetition.org/
[8] Amir, E., McIlraith, S.: Partition-based logical reasoning for first-order and propositional theories. Artif. Intell. 162(1), 49-88 (2005) · Zbl 1132.68672
[9] Prestwich, S.D.: CNF encodings. Handb. Satisfiability 185, 75-97 (2009)
[10] Ansótegui, C., Giráldez-Cru, J., Levy, J., Simon, L.: Using community structure to detect relevant learnt clauses. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 238-254. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_18 · Zbl 06512577
[11] Bjesse, P., Kukula, J., Damiano, R., Stanion, T., Zhu, Y.: Guiding SAT diagnosis with tree decompositions. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 315-329. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_24 · Zbl 1204.68104
[12] Huang, J., Darwiche, A.: A structure-based variable ordering heuristic for SAT. In: IJCAI, vol. 3, pp. 1167-1172 (2003)
[13] Monnet, A., Villemaire, R.: Scalable formula decomposition for propositional satisfiability. In: Proceedings of the Third C* Conference on Computer Science and Software Engineering, pp. 43-52. ACM (2010)
[14] Whitley, D., Hains, D., Howe, A.: Tunneling between optima: partition crossover for the traveling salesman problem. In: Proceedings of the 11th Annual Conference on Genetic and Evolutionary Computation, pp. 915-922. ACM (2009)
[15] Tinós, R., Whitley, D., Chicano, F.: Partition crossover for pseudo-boolean optimization. In: Proceedings of the 2015 ACM Conference on Foundations of Genetic Algorithms XIII, pp. 137-149. ACM (2015) · Zbl 1361.68209
[16] Ochoa, G., Chicano, F., Tinós, R., Whitley, D.: Tunnelling crossover networks. In: Proceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation, GECCO 2015, pp. 449-456. ACM, New York (2015)
[17] Lin, S.: Computer solutions of the traveling salesman problem. Bell Syst. Tech. J. 44(10), 2245-2269 (1965) · Zbl 0136.14705
[18] Tinós, R., Whitley, D., Ochoa, G.: Generalized asymmetric partition crossover (GAPX) for the asymmetric TSP. In: Proceedings of the 2014 Annual Conference on Genetic and Evolutionary Computation, pp. 501-508. ACM (2014)
[19] Kauffman, S., Levin, S.: Towards a general theory of adaptive walks on rugged landscapes. J. Theor. Biol. 128(1), 11-45 (1987)
[20] Zhang, W.: Configuration landscape analysis and backbone guided local search: part i: satisfiability and maximum satisfiability. Artif. Intell. 158, 1-26 (2004) · Zbl 1085.68678
[21] Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic ‘phase transitions’. Nature 400(6740), 133-137 (1999) · Zbl 1369.68244
[22] Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett. 8(3), 121-123 (1979) · Zbl 0398.68042
[23] Robertson, N., Seymour, P.D.: Graph minors. II. Algorithmic aspects of tree-width. J. Algorithms 7(3), 309-322 (1986) · Zbl 0611.05017
[24] Bodlaender, H.L.: Dynamic programming on graphs with bounded treewidth. In: Lepistö, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol. 317, pp. 105-118. Springer, Heidelberg (1988). doi:10.1007/3-540-19488-6_110 · Zbl 0649.68039
[25] Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM J. Algebraic Discret. Methods 8(2), 277-284 (1987) · Zbl 0611.05022
[26] Bodlaender, H.L.: Discovering treewidth. In: Vojtáš, P., Bieliková, M., Charron-Bost, B., Sýkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 1-16. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30577-4_1
[27] Kroc, L., Sabharwal, A., Gomes, C.P., Selman, B.: Integrating systematic and local search paradigms: a new strategy for MaxSAT. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 544-551. Morgan Kaufmann Publishers Inc., San Francisco (2009)
[28] Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 121-133. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72788-0_15 · Zbl 1214.68362
[29] Gaspers, S., Szeider, S.: Strong backdoors to bounded treewidth SAT. In: 2013 IEEE 54th Annual Symposium on Foundations of Computer Science (FOCS), pp. 489-498. IEEE (2013)
[30] Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61-75. Springer, Heidelberg (2005). doi:10.1007/11499107_5 · Zbl 1128.68463
[31] Sinz, C.: Visualizing SAT instances and runs of the DPLL algorithm. J. Autom. Reason. 39(2), 219-243 (2007) · Zbl 1129.68502
[32] Fruchterman, T.M., Reingold, E.M.: Graph drawing by force-directed placement. Softw.: Pract. Exp. 21(11), 129-1164 (1991)
[33] Frank, J.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.