Abstract
In statistical relational learning, one is concerned with inferring the most likely explanation (or world) that satisfies a given set of weighted constraints. The weight of a constraint signifies our confidence in the constraint, and the most likely world that explains a set of constraints is simply a satisfying assignment that maximizes the weights of satisfied constraints. The relational learning community has developed specialized solvers (e.g., Alchemy and Tuffy) for such weighted constraints independently of the work on SMT solvers in the verification community. In this paper, we show how to leverage SMT solvers to significantly improve the performance of relational solvers.
Constraints associated with a weight of 1 (or 0) are called axioms because they must be satisfied (or violated) by the final assignment. Axioms can create difficulties for relational solvers. We isolate the burden of axioms to SMT solvers and only lazily pass information back to the relational solver. This information can either be a subset of the axioms, or even generalized axioms (similar to predicate generalization in verification).
We implemented our algorithm in a tool called Soft-Cegar that out-performs state-of-the-art relational solvers Tuffy and Alchemy over four real-world applications. We hope this work opens the door for further collaboration between relational learning and SMT solvers.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Principles of Programming Languages (POPL 2002), pp. 1–3 (2002)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast. STTT: International Journal on Software Tools for Technology Transfer 9(5-6), 505–525 (2007)
Bilenko, M., Mooney, R.: Adaptive duplicate detection using learnable string similarity measures. In: Knowledge Discovery and Data Mining (KDD 2003), pp. 39–48 (2003)
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer (2007)
Braz, R., Amir, E., Roth, D.: Lifted first-order probabilistic inference. In: International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 1319–1325 (2005)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
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)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Kautz, H., Selman, B., Jiang, Y.: A general stochastic approach to solving problems with hard and soft constraints. In: Gu, D., Du, J., Pardalos, P. (eds.) The Satisfiability Problem: Theory and Applications, pp. 573–586. AMS (1997)
Kiddon, C., Domingos, P.: Coarse-to-fine inference and learning for first-order probabilistic models. In: National Conference on Artificial Intelligence, AAAI 2011 (2011)
Kok, S., Domingos, P.: Learning the structure of Markov logic networks. In: International Conference on Machine Learning (ICML 2005), pp. 441–448 (2005)
Kok, S., Sumner, M., Richardson, M., Singla, P., Poon, H., Lowd, D., Domingos, P.: The Alchemy system for statistical relational AI. Technical report, University of Washington (2007), http://alchemy.cs.washington.edu
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
Mihalkova, L., Mooney, R.: Bottom-up learning of Markov logic network structure. In: International Conference on Machine Learning (ICML 2007), pp. 625–632 (2007)
Milch, B., Zettlemoyer, L.S., Kersting, K., Haimes, M., Kaelbling, L.P.: Lifted probabilistic inference with counting formulas. In: National Conference on Artificial Intelligence (AAAI 2008), pp. 1062–1068 (2008)
Niu, F., Re, C., Doan, A., Shavlik, J.: Tuffy: Scaling up statistical inference in Markov logic networks using an RDBMS. In: International Conference on Very Large Data Bases, VLDB 2011 (2011)
Poole, D.: First-order probabilistic inference. In: International Joint Conference on Artificial Intelligence (IJCAI 2003), pp. 985–991 (2003)
Poon, H., Domingos, P.: Joint inference in information extraction. In: National Conference on Artificial Intelligence (AAAI 2007), pp. 913–918 (2007)
Poon, H., Domingos, P., Sumner, M.: A general method for reducing the complexity of relational inference and its application to mcmc. In: National Conference on Artificial Intelligence, AAAI 2008 (2008)
Richardson, M., Domingos, P.: Markov logic networks. Machine Learning 62, 107–136 (2006)
Riedel, S.: Cutting plane map inference for Markov logic. In: Statistical Relational Learning, SRL 2009 (2009)
Silberschatz, A., Korth, H., Sudarshan, S.: Database Systems Concepts, 5th edn. McGraw-Hill, Inc. (2006)
Singla, P., Domingos, P.: Entity resolution with Markov logic. In: International Conference on Data Mining (ICDM 2006), pp. 572–582 (2006)
Singla, P., Domingos, P.: Memory-efficient inference in relational domains. In: National Conference on Artificial Intelligence (AAAI 2006), pp. 488–493 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaganty, A., Lal, A., Nori, A.V., Rajamani, S.K. (2013). Combining Relational Learning with SMT Solvers Using CEGAR. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)