publication . Preprint . 2010

Heuristics in Conflict Resolution

Drescher, Christian; Gebser, Martin; Kaufmann, Benjamin; Schaub, Torsten;
Open Access English
  • Published: 11 May 2010
Modern solvers for Boolean Satisfiability (SAT) and Answer Set Programming (ASP) are based on sophisticated Boolean constraint solving techniques. In both areas, conflict-driven learning and related techniques constitute key features whose application is enabled by conflict analysis. Although various conflict analysis schemes have been proposed, implemented, and studied both theoretically and practically in the SAT area, the heuristic aspects involved in conflict analysis have not yet received much attention. Assuming a fixed conflict analysis scheme, we address the open question of how to identify "good'' reasons for conflicts, and we investigate several heuris...
free text keywords: Computer Science - Artificial Intelligence, Computer Science - Logic in Computer Science
Download from
27 references, page 1 of 2

Baral, C.; Brewka, G.; and Schlipf, J., eds. 2007. Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07). Springer-Verlag.

Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.

Bayardo, R., and Schrag, R. 1997. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI'97), 203-208. AAAI Press/MIT Press.

Beame, P.; Kautz, H.; and Sabharwal, A. 2004. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research 22:319-351.

Clark, K. 1978. Negation as failure. In Gallaire, H., and Minker, J., eds., Logic and Data Bases, 293-322. Plenum Press.

Dechter, R. 2003. Constraint Processing. Morgan Kaufmann Publishers. [OpenAIRE]

Dershowitz, N.; Hanna, Z.; and Nadel, A. 2005. A clausebased heuristic for SAT solvers. In Bacchus, F., and Walsh, T., eds., Proceedings of the Eigth International Conference on Theory and Applications of Satisfiability Testing (SAT'05), 46-60. Springer-Verlag.

Ee´n, N., and So¨rensson, N. 2003. An extensible SATsolver. In Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03), 502-518.

Erdem, E., and Lifschitz, V. 2003. Tight logic programs. Theory and Practice of Logic Programming 3(4-5):499- 518. [OpenAIRE]

Fages, F. 1994. Consistency of Clark's completion and the existence of stable models. Journal of Methods of Logic in Computer Science 1:51-60.

Gebser, M.; Kaufmann, B.; Neumann, A.; and Schaub, T. 2007a. clasp: A conflict-driven answer set solver. In Baral et al. (2007), 260-265. [OpenAIRE]

Gebser, M.; Kaufmann, B.; Neumann, A.; and Schaub, T. 2007b. Conflict-driven answer set enumeration. In Baral et al. (2007), 136-148.

Gebser, M.; Kaufmann, B.; Neumann, A.; and Schaub, T. 2007c. Conflict-driven answer set solving. In Veloso, M., ed., Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), 386-392. [OpenAIRE]

Gebser, M.; Liu, L.; Namasivayam, G.; Neumann, A.; Schaub, T.; and Truszczyn´ski, M. 2007d. The first answer set programming system competition. In Baral et al. (2007), 3-17.

Giunchiglia, E.; Lierler, Y.; and Maratea, M. 2006. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning 36(4):345-377. [OpenAIRE]

27 references, page 1 of 2
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue