Perrin Bignoli, Grad Student, RPI


Perrin Bignoli, Grad Student, RPI

Sage 4101

February 13, 2008 12:00 PM - 12:45 PM



In the Human-Level Intelligence Lab, we endeavor to discover ways to make computers capable of solving problems that are beyond the current scope of automation. One valuable tool for automated problem solving is model checking. This paper aims to extend the abilities of existing model checking routines and, in turn, cognitive architectures by developing a system to support inference about time and change. Since time is involved with problems across many domains, reasoning about it is required for the advancement of AI, as well as the creation of more powerful models of human cognition. We decided to implement model-checking with satisfiability testing (SAT). SAT has been used effectively in many inference, planning and constraint satisfaction tasks. However, since SAT constraints are defined over atomic propositions, domains with state variables that change over time can lead to extremely large search spaces. This poses both memory- and time-efficiency problems for existing SAT algorithms. In this paper, we propose to address these problems by introducing a language that encodes the temporal intervals over which relations occur and an integrated system that satisfies constraints formulated in this language. Temporal intervals are presented as a compressed method of encoding time that results in significantly smaller search spaces. However, intervals cannot be used efficiently without significant modifications to traditional SAT algorithms. Using the Polyscheme cognitive architecture, we created a system that integrates a DPLL-like SAT-solving algorithm with a rule matcher in order to support intervals by allowing new constraints and objects to be lazily instantiated throughout inference. Our system also includes constraint graphs to compactly store information about temporal and identity relationships between objects. In addition, a memory retrieval subsystem was utilized to guide inference towards minimal models in common sense reasoning problems involving time and change. We performed two sets of evaluations to isolate the contributions of the system's individual components. These tests demonstrate that both the ability to add new objects during inference and the use of smart memory retrieval result in a significant increase in performance over pure satisfiability algorithms alone and offer solutions to some problems on a larger scale than what was possible before. Also, we show that memory retrieval is able to improve the speed and scope of inference in addition to simple recall.


Add to calendar