Abstract
A portfolio approach has become a widespread method for parallelizing SAT solvers. In comparison with a divide-and-conquer approach, an important feature of the portfolio approach is that there is no need to conduct load-balancing for workers. Instead of load-balancing, the portfolio makes a diversification of workers by differentiating their search parameters. However, it is difficult to achieve effective diversification in a massively parallel environment because the number of combinations of the search parameters is limited. Thus, many overlaps of the search spaces between the workers can occur in such an environment. In order to prevent these overlaps, we propose a novel diversification method, called block branching, for the portfolio approach. Preliminary experimental results show that our approach works well, even in a small parallel setting (sixteen processes), and shows potential for a massively parallel environment.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)
Bordeaux, L., Hamadi, Y., Samulowitz, H.: Experiments with massively parallel constraint solving. In: Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI’09, pp. 443–448 (2009)
Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of the 15th National/10th Conference on Artificial Intelligence, AAAI’98/IAAI’98, pp. 431–437 (1998)
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)
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6(4), 245–262 (2009)
Marques-Silva, J.: Practical applications of boolean satisfiability. In: Proceedings of Workshop on Discrete Event Systems, WODES’08, pp. 74–80 (2008)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC’01, pp. 530–535 (2001)
Sonobe, T., Inaba, M.: Counter implication restart for parallel SAT solvers. In: Hamadi, Y., Schoenauer, M. (eds.) LION 2012. LNCS, vol. 7219, pp. 485–490. Springer, Heidelberg (2012)
Sonobe, T., Inaba M.: Division and alternation of decision variables. In: Pragmatics of SAT 2012 (2012)
Sonobe, T., Inaba, M., Nagai, A.: Counter implication restart. In: Pragmatics of SAT 2011 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sonobe, T., Inaba, M. (2013). Portfolio with Block Branching for Parallel SAT Solvers. In: Nicosia, G., Pardalos, P. (eds) Learning and Intelligent Optimization. LION 2013. Lecture Notes in Computer Science(), vol 7997. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-44973-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-44973-4_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-44972-7
Online ISBN: 978-3-642-44973-4
eBook Packages: Computer ScienceComputer Science (R0)