Abstract
We present GenC, an efficient and highly-parallel belief revision solver for paramatrized difference operators. GenC uses an AllSAT solver to enumerate the possible models of a formula, and then determines the output of revision through a series of bit comparisons. The result is a system that can calculate the result of revision for formulas with 100 variables and millions of clauses in just seconds; the running times obtained by GenC far surpass existing solvers for belief revision. The system also has many features that are useful for practical problems: it supports both interactive and offline data entry, it allows multiple formats for entering formulas, and it provides output in human-readable format. Most importantly, GenC is able to model revision by any parametrized difference operator, which allows a wide range of practical problems to be easily captured.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alchourrón, C.E., Gärdenfors, P., Makinson, D.: On the logic of theory change: partial meet functions for contraction and revision. J. Symb. Logic 50(2), 510–530 (1985)
Aravanis, T., Peppas, P.: Belief revision in answer set programming. In: Proceedings of the 21st Panhellenic Conference on Informatics (PCI 2017) (2017)
Dalal, M.: Investigations into a theory of knowledge base revision. In: Proceedings of the National Conference on Artificial Intelligence (AAAI), pp. 475–479 (1988)
Delgrande, J.P., Liu, D.H., Schaub, T., Thiele, S.: COBA 2.0: a consistency-based belief change system. In: Mellouli, K. (ed.) ECSQARU 2007. LNCS (LNAI), vol. 4724, pp. 78–90. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75256-1_10
Eiter, T., Gottlob, G.: On the complexity of propositional knowledge base revision, updates and counterfactuals. Artif. Intell. 57(2–3), 227–270 (1992)
Hoos, H., Stützle, T.: SATLIB: an online resource for research on SAT. In: SAT 2000, pp. 283–292 (2000)
Hunter, A., Tsang, E.: GenB: a general solver for AGM revision. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 564–569. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48758-8_40
Hunter, A.: Learning belief revision operators. In: Proceedings of the Canadian Conference on Artificial Intelligence, pp. 239–245 (2018)
Katsuno, H., Mendelzon, A.O.: Propositional knowledge base revision and minimal change. Artif. Intell. 52(2), 263–294 (1992)
Peppas, P., Williams, M.-A.: Kinetic consistency and relevance in belief revision. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 401–414. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48758-8_26
Toda, T., Soh, T.: Implementing efficient all solutions SAT solvers. ACM J. Exp. Algorithmics 21(1), 1.12:1–1.12:44 (2016)
Toda, T., Tsuda, K.: BDD construction for all solutions SAT and efficient caching mechanism. In: Proceedings of the 30th Annual ACM Symposium on Applied Computing, pp. 1880–1886 (2015)
Williams, M.-A.: Applications of belief revision. In: Freitag, B., Decker, H., Kifer, M., Voronkov, A. (eds.) DYNAMICS 1997. LNCS, vol. 1472, pp. 287–316. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055503
Zhuang, Z., Wang, Z., Wang, K., Qi, G.: DL-lite contraction and revision. J. Artif. Intell. Res. (JAIR) 56, 329–378 (2016)
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
Hunter, A., Agapeyev, J. (2019). An Efficient Solver for Parametrized Difference Revision. In: Liu, J., Bailey, J. (eds) AI 2019: Advances in Artificial Intelligence. AI 2019. Lecture Notes in Computer Science(), vol 11919. Springer, Cham. https://doi.org/10.1007/978-3-030-35288-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-35288-2_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-35287-5
Online ISBN: 978-3-030-35288-2
eBook Packages: Computer ScienceComputer Science (R0)