Colloquium: Transitions Systems for Describing Combinatorial Search Procedures

Dr. Yulia Lierer, Postdoctoral Fellow, Department of Computer Science, University of Kentucky

Host: Professor M. Truszczynski

Venue: 112 Raymond Blg (Civil Engineering) 

Abstract:

 Nieuwenhuis, Oliveras, and Tinelli (2006) introduced a transition system for modeling algorithms underlying Satisfiability solvers. In the talk we we show how transition systems can also be used for describing solvers developed for other propositional formalisms such as logic programming under answer set semantics and the ID-logic.

 Davis-Putnam-Logemann-Loveland (DPLL) is a classical example of a combinatorial search procedure that exhaustively searches the problem space to generate the solutions. DPLL generates satisfying assignments for propositional formulas. Most modern Satisfiability solvers are based on variations of the DPLL. Usually these variations are presented with the use of pseudocode. Nieuwenhuis, Oliveras, and Tinelli proposed an alternative approach to describing DPLL by means of a transition system. The transition system describes what "states of computation" are, and which transitions between states are allowed. In this way, it defines a directed graph such that every execution of the DPLL procedure corresponds to a path in this graph. Such an abstract way of presenting DPLL simplifies the analysis of its correctness and facilitates formal reasoning about its properties. Instead of reasoning about pseudocode constructs, we can reason about properties of a graph. For instance, by proving that the graph corresponding to a version of DPLL is acyclic we demonstrate that the algorithm always terminates. On the other hand, by checking that every terminal state corresponds to a solution we establish the correctness of the algorithm. Answer set programming is a popular knowledge representation and reasoning formalism based on answer set semantics of logic programs. It turns out that transition systems are also well-suited to describe algorithms underlying search procedures of answer set solvers, e.g., SMODELS and SUP. Propositional ID-logic is another knowledge representation formalism whose search procedures may be described by DPLL-like transition systems. The analysis of algorithms of answer set solvers and ID-logic solvers in terms of transition systems contributes to clarifying computational principles of these knowledge representation formalisms and possibly to the development of new systems.

 Overall transition systems constitute a clear and uniform framework for describing combinatorial search procedures. Such uniform approach provides the means for studying the relations between algorithms designed for reasoning with different logic languages, e.g., propositional logic, logic programming under answer set semantics, ID-logic, in precise mathematical terms. For instance, for a large class of logic programs, called tight, the graph representing SMODELS is closely related to the graph representing the application of DPLL to the ''completion'' of the program.

Short Bio:

Dr. Yuliya Lierler is a Computing Innovation Fellow Postdoc at the Computer Science Department at the University of Kentucky. Her research interests are in the field of artificial intelligence, especially in the areas of knowledge representation, automated reasoning, declarative problem solving, and natural language understanding. She completed her Ph.D. in Computer Science at the University of Texas at Austin earlier this year. Her dissertation bridged two traditionally separate fields: answer set programming and propositional satisfiability.

Speaker's personal page