Abstract
This work considers the MACE-style approach to finite model finding for (multi-sorted) first-order logic. This existing approach iteratively assumes increasing domain sizes and encodes the corresponding model existence problem as a SAT problem. The original MACE tool and its successors have considered techniques for avoiding introducing symmetries in the resulting SAT problem, but this has never been the focus of the previous work and has not received concentrated attention. In this work we formalise the symmetry avoiding problem, characterise the notion of a sound symmetry breaking heuristic, propose a number of such heuristics and evaluate them experimentally with an implementation in the Vampire theorem prover. Our results demonstrate that these new heuristics improve performance on a number of benchmarks taken from SMT-LIB and TPTP. Finally, we show that direct symmetry breaking techniques could be used to improve finite model finding, but that their cost means that symmetry avoidance is still the preferable approach.
This work was supported by EPSRC Grant EP/P03408X/1. Martin Suda was supported by the ERC Consolidator grant AI4REASON 649043.
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
Notes
- 1.
An alternative to encoding the problem into SAT is to target the EUF logic and use an SMT solver instead. This approach has been explored by Vakili and Day [21].
- 2.
This means that for every function symbol f of arity a we have \(M(f)(\mathsf {d}_1,\ldots ,\mathsf {d}_a)=\mathsf {d}\) if and only if \(M_\sigma (f)(\sigma (\mathsf {d}_1),\ldots ,\sigma (\mathsf {d}_a))=\sigma (\mathsf {d})\) and for every predicate symbol p of arity b we have \(M(p)(\mathsf {d}_1,\ldots ,\mathsf {d}_b)\) if and only if \(M_\sigma (p)(\sigma (\mathsf {d}_1),\ldots ,\sigma (\mathsf {d}_b))\).
- 3.
Recall that a \( DC \)-interpretation can be identified by the set of principal atoms true in it.
- 4.
- 5.
We necessarily have \(k \le m\) and \(k < m\) implies \(M(p_i) = M(p_j)\) for some \(i \ne j\).
- 6.
Speculating what this value could be if we proceed anyway is an interesting direction for further research not covered in this paper.
- 7.
In particular, \(p_1\) must be a constant.
- 8.
- 9.
- 10.
Some combinations are not sensible. For example, randomising the ordering of principal terms means that any ordering of function symbols will be ignored.
References
Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: efficient symmetry-breaking for Boolean satisfiability. In: Proceedings of the 40th Design Automation Conference, DAC 2003, Anaheim, CA, USA, 2–6 June 2003, pp. 836–839 (2003)
Audemard, G., Henocque, L.: The eXtended least number heuristic. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 427–442. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_35
Claessen, K., Lillieström, A.: Automated inference of finite unsatisfiability. J. Autom. Reason. 47(2), 111–132 (2011)
Claessen, K., Sörensson, N.: New techniques that improve MACE-style model finding. In: CADE-19 Workshop: Model Computation - Principles, Algorithms and Applications (2003)
Darga, P.T., Katebi, H., Liffiton, M., Markov, I.L., Sakallah, K.: Saucy. http://vlsicad.eecs.umich.edu/BK/SAUCY
Darga, P T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for CNF. In: Proceedings of the 41st Design Automation Conference, DAC 2004, San Diego, CA, USA, 7–11 June 2004, pp. 530–534. ACM (2004)
Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104–122. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_8
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). https://doi.org/10.1007/978-3-540-24605-3_37
Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer set solving in practice. In: Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, San Rafael (2012)
Gent, I.P., Petrie, K.E., Puget, J.: Symmetry in constraint programming. In: Handbook of Constraint Programming, pp. 329–376 (2006)
SAT Competitions: SAT Competition 2009: Benchmark Submission Guidelines. https://www.satcompetition.org/2009/format-benchmarks2009.html
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1
Mccune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problems. Technical report, Argonne National Laboratory (1994)
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning (in 2 volumes), pp. 335–367 (2001)
Reger, G., Suda, M., Voronkov, A.: The challenges of evaluating a new feature in vampire. In: Proceedings of the 1st and 2nd Vampire Workshops. EPiC Series in Computing, vol. 38, pp. 70–74. EasyChair (2016)
Reger, G., Suda, M., Voronkov, A.: Finding finite models in multi-sorted first-order logic. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 323–341. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_20
Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: GCAI 2016, 2nd Global Conference on Artificial Intelligence. EPiC Series in Computing, vol. 41, pp. 11–23. EasyChair (2016)
Sakallah, K.A.: Symmetry and satisfiability. In: Handbook of Satisfiability, pp. 289–338 (2009)
Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https://www.starexec.org
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)
Vakili, A., Day, N.A.: Finite model finding using the logic of equality with uninterpreted functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 677–693. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_41
Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI 1995, pp. 298–303 (1995)
Zhang, J., Zhang, H.: System description generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308–312. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61511-3_96
Acknowledgement
We thank the anonymous reviewers for critically reading the paper and suggesting substantial improvements.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Reger, G., Riener, M., Suda, M. (2019). Symmetry Avoidance in MACE-Style Finite Model Finding. In: Herzig, A., Popescu, A. (eds) Frontiers of Combining Systems. FroCoS 2019. Lecture Notes in Computer Science(), vol 11715. Springer, Cham. https://doi.org/10.1007/978-3-030-29007-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-29007-8_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29006-1
Online ISBN: 978-3-030-29007-8
eBook Packages: Computer ScienceComputer Science (R0)