Abstract
In this paper, we present a divide-and-conquer SAT solver, MapleAmpharos, that uses a novel propagation-rate (PR) based splitting heuristic. The key idea is that we rank variables based on the ratio of how many propagations they cause during the run of the worker conflict-driven clause-learning solvers to the number of times they are branched on, with the variable that causes the most propagations ranked first. The intuition here is that, in the context of divide-and-conquer solvers, it is most profitable to split on variables that maximize the propagation rate. Our implementation MapleAmpharos uses the AMPHAROS solver as its base. We performed extensive evaluation of MapleAmpharos against other competitive parallel solvers such as Treengeling, Plingeling, Parallel CryptoMiniSat5, and Glucose-Syrup. We show that on the SAT 2016 competition Application benchmark and a set of cryptographic instances, our solver MapleAmpharos is competitive with respect to these top parallel solvers. What is surprising that we obtain this result primarily by modifying the splitting heuristic.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
While the term cube refers to a conjunction of literals, we sometimes use this term to also refer to a sub-problem created by simplifying a formula with a cube.
References
Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 200–213. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_16
Audemard, G., Lagniez, J.-M., Szczepanski, N., Tabary, S.: An adaptive parallel SAT solver. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 30–48. Springer, Cham (2016). doi:10.1007/978-3-319-44953-1_3
Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197–205. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_15
Audemard, G., Simon, L.: Glucose and syrup in the sat 2016. SAT Compet. pp. 40–41 (2016)
Balyo, T., Sanders, P., Sinz, C.: HordeSat: A massively parallel portfolio SAT solver. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 156–172. Springer, Cham (2015). doi:10.1007/978-3-319-24318-4_12
Biere, A.: Yet another local search solver and lingeling and friends entering the sat competition 2014. SAT Compet. 2014(2), 65 (2014)
Biere, A.: Splatz, lingeling, plingeling, treengeling, yalsat entering the sat competition 2016. SAT Compet. 2016, 44 (2016)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)
Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press, Amsterdam (2009)
Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 10 (2008)
Chu, G., Stuckey, P.J., Harwood, A.: Pminisat: a parallelization of minisat 2.0. SAT race (2008)
Fujii, H., Fujimoto, N.: Gpu acceleration of bcp procedure for sat algorithms. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA), The Steering Committee of The World Congress in Computer Science, Computer Engineering and Applied Computing (WorldComp), p. 1 (2012)
Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-Completeness Theory. Oxford University Press on Demand, New York (1995)
Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 252–265. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15396-9_22
Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. J. Satisf. Boolean Model. Comput. 6, 245–262 (2008)
Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34188-5_8
Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: Partitioning SAT instances for distributed solving. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 372–386. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16242-8_27
Hyvärinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 214–227. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_17
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_9
Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. In: 1993 Proceedings of the 2nd Israel Symposium on the Theory and Computing Systems, pp. 128–133. IEEE (1993)
Manthey, N.: Towards next generation sequential and parallel SAT solvers. KI-Künstliche Intelligenz 30(3–4), 339–342 (2016)
Nejati, S., Liang, J.H., Ganesh, V., Gebotys, C., Czarnecki, K.: Adaptive restart and cegar-based solver for inverting cryptographic hash functions. arXiv preprint (2016). arXiv:1608.04720
Nossum, V.: SAT-based preimage attacks on SHA-1. Master’s thesis (2012)
Nossum, V.: Instance generator for encoding preimage, second-preimage, and collision attacks on SHA-1. In: Proceedings of the SAT competition, pp. 119–120 (2013)
Rintanen, J.: Planning and SAT. Handb. Satisf. 185, 483–504 (2009)
Semenov, A., Zaikin, O.: Using Monte Carlo method for searching partitionings of hard variants of boolean satisfiability problem. In: Malyshkin, V. (ed.) PaCT 2015. LNCS, vol. 9251, pp. 222–230. Springer, Cham (2015). doi:10.1007/978-3-319-21909-7_21
Sohanghpurwala, A.A., Hassan, M.W., Athanas, P.: Hardware accelerated SAT solvers a survey. J. Parallel Distrib. Comput. 106, 170–184 (2016)
Soos, M.: The cryptominisat 5 set of solvers at SAT competition 2016. SAT Compet. 2016, 28 (2016)
Tak, P., Heule, M.J.H., Biere, A.: Concurrent cube-and-conquer. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 475–476. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_42
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Nejati, S. et al. (2017). A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-66263-3_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66262-6
Online ISBN: 978-3-319-66263-3
eBook Packages: Computer ScienceComputer Science (R0)