EAGER: Robust Reasoning using a Geometric Approach to SAT and PSAT

University Of Utah, Salt Lake City UT

Investigators

Abstract

The overarching goal of this EAGER project is to develop efficient and reliable methods for autonomous agents to produce plans for their safe operation in complex situations. For example, the development of large-scale unmanned aircraft system operation in urban areas for package delivery depends on such a capability. The fundamental issue is to determine if there is a viable solution in a specific situation; at the present time the complexity of this problem is too high to guarantee that a solution can be found. The team of researchers is developing a lower complexity approach with wide application in artificial intelligence. The project engages student researchers from underrepresented groups in computer science, and the research results are integrated into the classroom through courses like artificial intelligence, theory of computation, and autonomous agent systems. The project provides a new approach to agent planning at the cognitive level. The basic innovation is to convert the satisfiability problem into a geometric setting; in particular, the models of an n-variable logical sentence are viewed as the corners of an n-D hypercube, and interior points assign probabilities to the variables. Each conjunct in the conjunctive normal form sentence reduces the convex feasible solution region. Any non-empty feasible region indicates the existence of a solution to the probabilistic satisfiability problem and can also be probed with linear programming methods in polynomial time to seek an answer to the satisfiability problem. Particular approaches to be explored include: (1) modifications to the interior point method using barrier methods, (2) finding linear programming solutions in a non-Euclidean geometry, (3) applying random rotations to the feasible region to allow coordinate projects to determine if there is a solution, and (4) using Markov Chain Monte Carlo to get a point near a corner. Applications include probabilistic satisfiability inference, reinforcement policy optimization for autonomous agents, and probabilistic temporal logic. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.