Abstract
In many real-life computational search problems, one is not only interested in finding a solution, but also in maintaining a solution under varying circumstances. For example, in the area of network configuration, an initial configuration of a computer network needs to be obtained, but also a new configuration when one of the machines in the network breaks down. Currently, most such revision problems are solved manually, or with highly specialized software.
A recent declarative approach to solve (hard) computational search problems involving a lot of domain knowledge, is by finite model generation. Here, the domain knowledge is specified as a logic theory T, and models of T correspond to solutions of the problem. In this paper, we extend this approach to solve revision problems. In particular, our method allows to use the same theory to describe the search problem and the revision problem, and applies techniques from current model generators to find revised solutions.
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
Preview
Unable to display preview. Download preview PDF.
References
Brain, M., Watson, R., De Vos, M.: An interactive approach to answer set programming. In: Answer Set Programming. CEUR Workshop Proceedings, vol. 142 (2005), CEUR-WS.org
Cadoli, M., Ianni, G., Palopoli, L., Schaerf, A., Vasile, D.: NP-SPEC: an executable specification language for solving all problems in NP. Computer Languages 26(2-4), 165–195 (2000)
De Cat, B.: Ontwikkeling van algoritmes voor modelrevisie, met toepassingen in treinplanning en netwerkconfiguratie. Master’s thesis, Katholieke Universiteit Leuven, Leuven, Belgium (June 2009) (in Dutch)
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)
Enderton, H.B.: A Mathematical Introduction To Logic. Academic Press, London (1972)
Fox, M., Gerevini, A., Long, D., Serina, I.: Plan stability: Replanning versus plan repair. In: Long, D., Smith, S.F., Borrajo, D., McCluskey, L. (eds.) ICAPS, pp. 212–221. AAAI, Menlo Park (2006)
Li, C.M., Manyà , F., Planes, J.: New inference rules for max-sat. J. Artif. Intell. Res. (JAIR) 30, 321–359 (2007)
Marek, V.W., Truszczyński, M.: Stable models and an alternative logic programming paradigm. In: Apt, K.R., Marek, V.W., Truszczyński, M., Warren, D.S. (eds.) The Logic Programming Paradigm: a 25-Year Perspective, pp. 375–398. Springer, Heidelberg (1999)
Mariën, M., Wittocx, J., Denecker, M., Bruynooghe, M.: SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 211–224. Springer, Heidelberg (2008)
Mitchell, D.G.: A SAT solver primer. Bulletin of the European Association for Theoretical Computer Science 85, 112–132 (2005)
Mitchell, D.G., Ternovska, E., Hach, F., Mohebali, R.: Model expansion as a framework for modelling and solving search problems. Technical Report TR 2006-24, Simon Fraser University, Canada (2006)
Niemelä, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25(3-4), 241–273 (1999)
Patterson, M., Liu, Y., Ternovska, E., Gupta, A.: Grounding for model expansion in k-guarded formulas with inductive definitions. In: Veloso, M.M. (ed.) IJCAI, pp. 161–166 (2007)
Perri, S., Scarcello, F., Catalano, G., Leone, N.: Enhancing DLV instantiator by backjumping techniques. Annals of Mathematics and Artificial Intelligence 51(2-4), 195–228 (2007)
Pipatsrisawat, K., Darwiche, A.: Clone: Solving Weighted Max-SAT in a Reduced Search Space. In: Orgun, M.A., Thornton, J. (eds.) AI 2007. LNCS (LNAI), vol. 4830, pp. 223–233. Springer, Heidelberg (2007)
Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pp. 521–532 (1995)
Wittocx, J., Mariën, M., Denecker, M.: GidL: A grounder for FO + . In: Pagnucco, M., Thielscher, M. (eds.) NMR, pp. 189–198. University of New South Wales (2008)
Wittocx, J., Mariën, M., Denecker, M.: The idp system: a model expansion system for an extension of classical logic. In: Denecker, M. (ed.) LaSh, pp. 153–165 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wittocx, J., De Cat, B., Denecker, M. (2011). Towards Computing Revised Models for FO Theories. In: Abreu, S., Seipel, D. (eds) Applications of Declarative Programming and Knowledge Management. INAP 2009. Lecture Notes in Computer Science(), vol 6547. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20589-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-20589-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20588-0
Online ISBN: 978-3-642-20589-7
eBook Packages: Computer ScienceComputer Science (R0)