Abstract
We present an algorithm, CDCL-AMS, for solving Modular Systems consisting of a set of modules where, for each module, we have a simple “black-box” solver. The algorithm is based on the Conflict-Directed Clause Learning algorithm for SAT, and communicates asynchronously with the black-box solvers to accommodate high variability in response latencies.
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
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Eiter, T., Fink, M., Krennwallner, T., Redl, C.: Conflict-driven ASP solving with external sources. Theory Pract. Logic Program. 12(4–5), 659–679 (2012)
Gebser, M., Ostrowski, M., Schaub, T.: Constraint answer set solving. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 235–249. Springer, Heidelberg (2009)
Manthey, N.: Towards Next Generation Sequential and Parallel SAT Solvers. Ph.D. thesis, TU Dresden (2014)
Marques-Silva, J.P., Sakallah, K.A.: Grasp: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)
Mitchell, D.G., Ternovska, E.: A framework for representing and solving NP search problems. In: Veloso, M.M., Kambhampati, S. (eds.) Proceedings The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, 9–13 July, 2005, Pittsburgh, Pennsylvania, USA, pp. 430–435. AAAI Press/The MIT Press (2005)
Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation = lazy clause generation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 544–558. Springer, Heidelberg (2007)
Tasharrofi, S., Ternovska, E.: A semantic account for modularity in multi-language modelling of search problems. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 259–274. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Mitchell, D., Ternovska, E. (2015). Clause-Learning for Modular Systems. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2015. Lecture Notes in Computer Science(), vol 9345. Springer, Cham. https://doi.org/10.1007/978-3-319-23264-5_37
Download citation
DOI: https://doi.org/10.1007/978-3-319-23264-5_37
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23263-8
Online ISBN: 978-3-319-23264-5
eBook Packages: Computer ScienceComputer Science (R0)