×

zbMATH — the first resource for mathematics

The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17). (English) Zbl 07099220
Summary: After a break of about five years, in 2016 the classical QBFEVAL has been revived. QBFEVAL is a competitive evaluation of solvers for quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over the propositional variables. Due to the enormous interest in QBFEVAL’16, more recently, QBFEVAL’17 was organized. Both competitions were affiliated to the respective editions of the International Conference on Theory and Applications of Satisfiability Testing (SAT’16 and SAT’17), the major conference in research on SAT and related areas. In this paper we report about the 2016 and 2017 competitive evaluations of QBF solvers (QBFEVAL’16 and QBFEVAL’17), the two most recent events in a series of competitions established with the aim of assessing the advancements in reasoning about QBFs. This report gives an overview of the setup of these two events, on their participants and on the results of the experiments that were performed for evaluating the participating systems.

MSC:
68T Artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Balyo, T.; Biere, A.; Iser, M.; Sinz, C.; Race, S. A.T., SAT Race 2015, Artif. Intell., 241, 45-65, (2016) · Zbl 1392.68381
[2] Balyo, T.; Heule, M. J.H.; Järvisalo, M., SAT competition 2016: recent developments, (Proc. of the Thirty-First AAAI Conference on Artificial Intelligence. Proc. of the Thirty-First AAAI Conference on Artificial Intelligence, AAAI’17, (2017), AAAI Press), 5061-5063
[3] Cok, D. R.; Déharbe, D.; Weber, T., The 2014 SMT competition, J. Satisf. Boolean Model. Comput., 9, 207-242, (2014)
[4] Marin, P.; Narizzano, M.; Pulina, L.; Tacchella, A.; Giunchiglia, E., Twelve years of QBF evaluations: QSAT is pspace-hard and it shows, Fundam. Inform., 149, 1-2, 133-158, (2016) · Zbl 1373.68380
[5] Pulina, L., The ninth QBF solvers evaluation - preliminary report, (Proc. of the 4th International Workshop on Quantified Boolean Formulas. Proc. of the 4th International Workshop on Quantified Boolean Formulas, QBF’16. Proc. of the 4th International Workshop on Quantified Boolean Formulas. Proc. of the 4th International Workshop on Quantified Boolean Formulas, QBF’16, CEUR Workshop Proc., CEUR-WS.org, vol. 1719, (2016)), 1-13
[6] Janota, M.; Jordan, C.; Klieber, W.; Lonsing, F.; Seidl, M.; Van Gelder, A., The QBFGallery 2014: the QBF competition at the FLoC olympic games, J. Satisf. Boolean Model. Comput., 9, 187-206, (2016)
[7] Lonsing, F.; Seidl, M.; Gelder, A. V., The QBF gallery: behind the scenes, Artif. Intell., 237, 92-114, (2016) · Zbl 1357.68209
[8] Stump, A.; Sutcliffe, G.; Tinelli, C., StarExec: a cross-community infrastructure for logic solving, (Proc. of the 7th International Joint Conference on Automated Reasoning. Proc. of the 7th International Joint Conference on Automated Reasoning, IJCAR’14. Proc. of the 7th International Joint Conference on Automated Reasoning. Proc. of the 7th International Joint Conference on Automated Reasoning, IJCAR’14, Lecture Notes in Computer Science, vol. 8562, (2014), Springer), 367-373 · Zbl 06348250
[9] Diptarama; Narisawa, K.; Shinohara, A., Extension of generalized tic-tac-toe: p stones for one move, IPSJ J., 55, 2344-2352, (2014)
[10] Amendola, G.; Ricca, F.; Truszczynski, M., Generating hard random Boolean formulas and disjunctive logic programs, (Proceedings of the 26th International Joint Conference on Artificial Intelligence, (2017), AAAI Press), 532-538
[11] Slivovsky, F.; Szeider, S., Soundness of Q-resolution with dependency schemes, Theor. Comput. Sci., 612, 83-101, (2016) · Zbl 1332.68204
[12] Peschiera, C.; Pulina, L.; Tacchella, A.; Bubeck, U.; Kullmann, O.; Lynce, I., The seventh QBF solvers evaluation (QBFEVAL’10), (Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10, Lecture Notes in Computer Science, vol. 6175, (2010), Springer: Springer Berlin Heidelberg), 237-250 · Zbl 1306.68173
[13] Brummayer, R.; Lonsing, F.; Biere, A., Automated testing and debugging of SAT and QBF solvers, (Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10, Lecture Notes in Computer Science, vol. 6175, (2010), Springer), 44-57 · Zbl 1306.68155
[14] Chen, H.; Interian, Y., A model for generating random quantified Boolean formulas, (Proc. of 19th International Joint Conference on Artificial Intelligence. Proc. of 19th International Joint Conference on Artificial Intelligence, IJCAI’05, (2005)), 66-71
[15] Rousseeuw, P. J., Silhouettes: a graphical aid to the interpretation and validation of cluster analysis, J. Comput. Appl. Math., 20, 53-65, (1987) · Zbl 0636.62059
[16] Hall, M.; Frank, E.; Holmes, G.; Pfahringer, B.; Reutemann, P.; Witten, I. H., The weka data mining software: an update, ACM SIGKDD Explor. Newsl., 11, 1, 10-18, (2009)
[17] Pigorsch, F.; Scholl, C., Exploiting structure in an AIG based QBF solver, (Design, Automation and Test in Europe. Design, Automation and Test in Europe, DATE’09, (2009), IEEE), 1596-1601
[18] Scholl, C.; Pigorsch, F., The QBF solver AIGSolve, (Proc. of the 4th Int. Workshop on Quantified Boolean Formulas. Proc. of the 4th Int. Workshop on Quantified Boolean Formulas, QBF 2016. Proc. of the 4th Int. Workshop on Quantified Boolean Formulas. Proc. of the 4th Int. Workshop on Quantified Boolean Formulas, QBF 2016, CEUR Workshop Proc., CEUR-WS.org, vol. 1719, (2016)), 55-62
[19] Pigorsch, F.; Scholl, C., An AIG-based QBF-solver using SAT for preprocessing, (Proc. of the 47th International Conference on Design Automation Conference. Proc. of the 47th International Conference on Design Automation Conference, DAC’10, (2010), IEEE), 170-175
[20] Gent, I.; Giunchiglia, E.; Narizzano, M.; Rowley, A.; Tacchella, A., Watched data structures for QBF solvers, (Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing. Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing, SAT’03. Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing. Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing, SAT’03, Lecture Notes in Computer Science, vol. 2919, (2003), Springer Verlag), 25-36 · Zbl 1204.68195
[21] Giunchiglia, E.; Narizzano, M.; Tacchella, A., Clause-term resolution and learning in quantified Boolean logic satisfiability, Artif. Intell. Res., 26, 371-416, (2006) · Zbl 1183.68475
[22] Gomes, C. P.; Selman, B.; Kautz, H., Boosting combinatorial search through randomization, (Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference. Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI’98/IAAI’98, vol. 98, (1998), AAAI Press / The MIT Press), 431-437
[23] Pipatsrisawat, K.; Darwiche, A., A lightweight component caching scheme for satisfiability solvers, (Proc. of the 10th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT’07. Proc. of the 10th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT’07, Lecture Notes in Computer Science, vol. 4501, (2007), Springer), 294-299
[24] Zhang, L.; Malik, S., Conflict driven learning in a quantified Boolean satisfiability solver, (Proc. of the International Conference on Computer Aided Design. Proc. of the International Conference on Computer Aided Design, ICCAD’02, (2002), ACM / IEEE Computer Society), 442-449
[25] Zhang, L.; Madigan, C. F.; Moskewicz, M. W.; Malik, S., Efficient conflict driven learning in a Boolean satisfiability solver, (Proc. of the International Conference on Computer-Aided Design. Proc. of the International Conference on Computer-Aided Design, ICCAD’01, (2001)), 279-285
[26] Giunchiglia, E.; Marin, P.; Narizzano, M., sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning, (Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10, Lecture Notes in Computer Science, vol. 6175, (2010), Springer), 85-98 · Zbl 1306.68157
[27] Pulina, L.; Tacchella, A., A self-adaptive multi-engine solver for quantified Boolean formulas, Constraints, 14, 1, 80-116, (2009) · Zbl 1183.68589
[28] Janota, M.; Marques-Silva, J., Abstraction-based algorithm for 2QBF, (Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing, SAT’11. Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing, SAT’11, Lecture Notes in Computer Science, vol. 6695, (2011), Springer), 230-244 · Zbl 1330.68115
[29] Biere, A.; Lonsing, F.; Seidl, M., Blocked clause elimination for QBF, (Bjørner, N.; Sofronie-Stokkermans, V., Proc. of the 23rd International Conference on Automated Deduction. Proc. of the 23rd International Conference on Automated Deduction, CADE’11. Proc. of the 23rd International Conference on Automated Deduction. Proc. of the 23rd International Conference on Automated Deduction, CADE’11, Lecture Notes in Computer Science, vol. 6803, (2011), Springer), 101-115 · Zbl 1341.68181
[30] Eiter, T.; Gottlob, G., On the computational cost of disjunctive logic programming: propositional case, Ann. Math. Artif. Intell., 15, 3-4, 289-323, (1995) · Zbl 0858.68016
[31] Rabe, M. N.; Seshia, S. A., Incremental determinization, (Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT’16. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT’16, Lecture Notes in Computer Science, vol. 9710, (2016), Springer), 375-392 · Zbl 06623523
[32] Rabe, M. N.; Tentrup, L., CAQE: a certifying QBF solver, (Proc. of the 15th Conference on Formal Methods in Computer-Aided Design. Proc. of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD’15, (2015)), 136-143
[33] Narizzano, M.; Peschiera, C.; Pulina, L.; Tacchella, A., Evaluating and certifying QBFs: a comparison of state-of-the-art tools, AI Commun., 22, 4, 191-210, (2009) · Zbl 1186.68440
[34] Lonsing, F.; Biere, A., DepQBF: a dependency-aware QBF solver, JSAT, 7, 2-3, 71-76, (2010)
[35] Letz, R., Lemma and model caching in decision procedures for quantified Boolean formulas, (Proc. of the International Conference on Automated Reasoning With Analytic Tableaux and Related Methods. Proc. of the International Conference on Automated Reasoning With Analytic Tableaux and Related Methods, TABLEAUX’02. Proc. of the International Conference on Automated Reasoning With Analytic Tableaux and Related Methods. Proc. of the International Conference on Automated Reasoning With Analytic Tableaux and Related Methods, TABLEAUX’02, Lecture Notes in Computer Science, vol. 2381, (2002), Springer), 160-175 · Zbl 1015.68173
[36] Zhang, L.; Malik, S., Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation, (Proc. of the Eighth International Conference on Principles and Practice of Constraint Programming. Proc. of the Eighth International Conference on Principles and Practice of Constraint Programming, CP’02. Proc. of the Eighth International Conference on Principles and Practice of Constraint Programming. Proc. of the Eighth International Conference on Principles and Practice of Constraint Programming, CP’02, Lecture Notes in Computer Science, vol. 2470, (2002)), 200-215
[37] Lonsing, F.; Bacchus, F.; Biere, A.; Egly, U.; Seidl, M., Enhancing search-based QBF solving by dynamic blocked clause elimination, (Proc. of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’15. Proc. of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’15, Lecture Notes in Computer Science, vol. 9450, (2015), Springer), 418-433 · Zbl 06528797
[38] Lonsing, F.; Egly, U., Depqbf 6.0: a search-based QBF solver beyond traditional QCDCL, (Proc. of the 26th International Conference on Automated Deduction. Proc. of the 26th International Conference on Automated Deduction, CADE 26. Proc. of the 26th International Conference on Automated Deduction. Proc. of the 26th International Conference on Automated Deduction, CADE 26, Lecture Notes in Computer Science, vol. 10395, (2017), Springer), 371-384 · Zbl 06778415
[39] Niemetz, A.; Preiner, M.; Lonsing, F.; Seidl, M.; Biere, A., Resolution-based certificate extraction for QBF, (Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’12. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’12, Lecture Notes in Computer Science, vol. 7317, (2012)), 430-435
[40] Charwat, G.; Woltran, S., DynQBF: a dynamic programming-based QBF solver, (2016)
[41] Klieber, W.; Sapra, S.; Gao, S.; Clarke, E., A non-prenex, non-clausal QBF solver with game-state learning, (Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT’10, Lecture Notes in Computer Science, vol. 6175, (2010), Springer), 128-142 · Zbl 1306.68161
[42] Balyo, T.; Lonsing HordeQBF, F., A modular and massively parallel QBF solver, (Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT’16. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT’16, Lecture Notes in Computer Science, vol. 9710, (2016), Springer), 531-538 · Zbl 06623533
[43] Balyo, T.; Sanders, P.; Sinz HordeSat, C., A massively parallel portfolio SAT solver, (Proc. of the 18th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 18th International Conference on Theory and Applications of Satisfiability Testing, SAT’15. Proc. of the 18th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 18th International Conference on Theory and Applications of Satisfiability Testing, SAT’15, Lecture Notes in Computer Science, vol. 9340, (2015), Springer), 156-172 · Zbl 06512571
[44] Wimmer, R.; Reimer, S.; Marin, P.; Becker, B., HQSpre-an effective preprocessor for QBF and DQBF, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2017), Springer), 373-390
[45] Bloem, R.; Braud-Santoni, N.; Hadzic, V., QBF solving by counterexample-guided expansion, CoRR
[46] Korovin, K., Inst-gen - a modular approach to instantiation-based automated reasoning, (Programming Logics - Essays in Memory of Harald Ganzinger. Programming Logics - Essays in Memory of Harald Ganzinger, Lecture Notes in Computer Science, vol. 7797, (2013), Springer), 239-270 · Zbl 1385.68038
[47] Seidl, M.; Lonsing, F.; Biere, A., qbf2epr: a tool for generating EPR formulas from QBF, (Proc. of the Third Workshop on Practical Aspects of Automated Reasoning. Proc. of the Third Workshop on Practical Aspects of Automated Reasoning, PAAR’12. Proc. of the Third Workshop on Practical Aspects of Automated Reasoning. Proc. of the Third Workshop on Practical Aspects of Automated Reasoning, PAAR’12, EPiC Series in Computing, EasyChair, vol. 21, (2012)), 139-148
[48] Jordan, C.; Kaiser, L.; Lonsing, F.; Seidl, M., MPIDepQBF: towards parallel QBF solving without knowledge sharing, (Proc. of the 17th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 17th International Conference on Theory and Applications of Satisfiability Testing, SAT’14. Proc. of the 17th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 17th International Conference on Theory and Applications of Satisfiability Testing, SAT’14, Lecture Notes in Computer Science, vol. 8561, (2014), Springer), 430-437 · Zbl 1423.68455
[49] Van Gelder, A., Primal and dual encoding from applications into quantified Boolean formulas, (Proc. of the 19th International Conference on Principles and Practice of Constraint Programming. Proc. of the 19th International Conference on Principles and Practice of Constraint Programming, CP’13. Proc. of the 19th International Conference on Principles and Practice of Constraint Programming. Proc. of the 19th International Conference on Principles and Practice of Constraint Programming, CP’13, Lecture Notes in Computer Science, vol. 8124, (2013), Springer), 694-707
[50] Tu, K.; Hsu, T.; Jiang, J. R., QELL: QBF reasoning with extended clause learning and levelized SAT solving, (Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’15. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’15, Lecture Notes in Computer Science, vol. 9340, (2015), Springer), 343-359 · Zbl 06512584
[51] Janota, M.; Marques-Silva, J., Solving QBF by clause selection, (Proc. of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Proc. of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI’15, (2015), AAAI Press), 325-331
[52] Janhunen, T.; Tasharrofi, S.; Ternovska SAT-TO-SAT, E., Declarative extension of SAT solvers with new propagators, (Proc. of the Thirtieth AAAI Conference on Artificial Intelligence. Proc. of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI’16, (2016), AAAI Press), 978-984
[53] Bogaerts, B.; Janhunen, T.; Tasharrofi, S., Solving QBF instances with nested SAT solvers, (Proc. of the 2016 AAAI Beyond NP Workshop. Proc. of the 2016 AAAI Beyond NP Workshop, AAAI Workshops, vol. WS-16-05, (2016), AAAI Press), 307-313
[54] Lonsing, F.; Biere, A., Failed literal detection for QBF, (Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing, SAT’11. Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 14th International Conference on Theory and Applications of Satisfiability Testing, SAT’11, Lecture Notes in Computer Science, vol. 6695, (2011), Springer), 259-272 · Zbl 1330.68118
[55] Devriendt, J.; Bogaerts, B.; Bruynooghe BreakIDGlucose, M., On the importance of row symmetry in SAT, (Proc. 4th International Workshop on the Cross-Fertilization Between CSP and SAT, (2014)), 1-17
[56] Tentrup, L., Non-prenex QBF solving using abstraction, (Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT’16. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT’16, Lecture Notes in Computer Science, vol. 9710, (2016), Springer), 393-401 · Zbl 06623524
[57] Peitl, T.; Slivovsky, F.; Szeider, S., Dependency learning for QBF, (Proc. of the 20th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 20th International Conference on Theory and Applications of Satisfiability Testing, SAT’17. Proc. of the 20th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 20th International Conference on Theory and Applications of Satisfiability Testing, SAT’17, Lecture Notes in Computer Science, vol. 10491, (2017), Springer), 298-313 · Zbl 06807233
[58] Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E., Solving QBF with counterexample guided refinement, (Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’12. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proc. of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT’12, Lecture Notes in Computer Science, vol. 7317, (2012), Springer), 114-128 · Zbl 1273.68178
[59] Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E., Solving QBF with counterexample guided refinement, Artif. Intell., 234, 1-25, (2016) · Zbl 1351.68254
[60] Pulina, L.; Tacchella, A., A structural approach to reasoning with quantified Boolean formulas, (Proc. of the 21st International Joint Conference on Artificial Intelligence. Proc. of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, (2009)), 596-602
[61] Narizzano, M.; Pulina, L.; Tacchella, A., The QBFEVAL web portal, (Proc. of the 10th European Conference on Logics in Artificial Intelligence. Proc. of the 10th European Conference on Logics in Artificial Intelligence, JELIA’06. Proc. of the 10th European Conference on Logics in Artificial Intelligence. Proc. of the 10th European Conference on Logics in Artificial Intelligence, JELIA’06, Lecture Notes in Computer Science, vol. 4160, (2006), Springer Verlag), 494-497
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.