This project explores connections between computational logic and polyhedral combinatorics through the paradigm of Quantified Polyhedral programming. Quantified Polyhedral programming encompasses Quantified Linear Programming (QLP) and Quantified Integer Programming (QIP); both the programming paradigms are extremely useful in modeling environment-dependent actions in real-time scheduling problems. Quantified Integer Programs can also be used to formally verify the correctness of programs through the mechanism of Abstract Interpretation. This project aims to provide a framework in which traditional notions of duality and convexity can be extended to the 2-person game setting. For instance, a typical optimization problem is defined by an optimization function and a convex set, called the domain of feasibility. In real-world applications, such as robot navigation, the domain is not fixed but varies continuously as a consequence of events initiated by the environment. Thus, the concept of optimality needs to be defined in a 2-person setting.
On a broader front, the investigator plans to significantly advance the state-of-the-art in Quantified Polyhedral Programming through a combination of innovative research and the integration of research themes into graduate and undergraduate education. This work will have the added benefit of increasing the participation of women and under-represented minorities in computer science research.
This award is co-funded by West Virginia EPSCoR.
Project Outcomes: Quantified Linear Programming (QLP) is the problem of checkingwhether a linear system is satisfiable with respect to a given quantifierstring that specifies which variables are existentially quantified and which are universally quantified. Hence, quantified linear programming is a (non-trivial)generalization of linear programming. Accordingly, a quantified linear program consists of a set of linear inequalities and a corresponding quantifier string, in which a bounded region of values is also specified for each universally quantified variable.The problem that arises by extending the quantification of variables to implications of two linear systemsis called Quantified Linear Implication (QLI). Alternatively, QLI can be viewed as extending the notion of inclusion of two linear systems to arbitrary quantifiers.Several interesting variants of these problems arise when the universally quantifiedvariables are partially bounded or unbounded, namely the partially bounded and the unbounded QLP (PQLP and UQLP, respectively),and the partially bounded and the unbounded QLI (PQLI and UQLI, respectively). Any QLP can be viewed as a 2-person game. Such a game includes an existential player X, who chooses values for the existentially quantified variables, and a universal player Y, who chooses values for the universally quantifiedvariables. X and Y make their choices according to theorder of the variables in the quantifier string. If, at the end, the instantiatedlinear system in the QLP is true, then X wins the game (i.e., X has a winning strategy). Otherwise, Y wins the game (i.e., Y has a winning strategy). Similarly, we proposed 2-person game semantics for QLIs: An existential player X and a universal player Y also choose their moves according to the order of the variables in thequantifier string.The goals of the players are the following: X selects the values of the existentially quantified variables so asto violate the constraints in the Left-Hand Side (LHS) or to satisfy the constraints in the Right-Hand Side (RHS) of theimplication. On the other hand, Y selects the values ofthe universally quantified variables so as to satisfy the constraints of the LHS and at the same time to violate the constraints of the RHS of the implication. X wins the game (i.e., has a winning strategy)if at the end of the game the instantiated implication in the QLI is true. Otherwise, Y wins the game (i.e., has a winning strategy). Using these 2-person game semantics as well as results and procedures from polyhedral theory and computational logic, our research established several important results for QLPs and QLIs and their variants. More specifically, we showed that the generic QLI problem is PSPACE-complete. Note that QLPs have been shown to be in PSPACE though their hardness has not been established.Moreover, with respect to each class of the polynomial hierarchy (PH), we showed that there exists some instantiation to the QLI frameworkthat is complete for this class.This is interesting with respect to the fact that QLIs cover the {f PH} using only continuous (and not discrete) variables,thus providing a continuous analogue of the way Quantified Boolean Formulas cover PH. Furthermore, we established the computational complexities of all classes of QLIs with 0 and 1 quantifier alternations, and of several interesting classes of $2$ quantifier alternations.The latter describe variants of the problem of entailment of polyhedral sets of parameterized linear constraints. Further, we proved that all partially bounded and unbounded variants of QLPs and QLIs are in P. The intellectual merit of this proposal is rooted in the fact that the research that was undertaken with respect tothe above-mentioned problems required combining fundamentally new ideas from multi-disciplinary fields,such as combinatorial algorithms, computational logic, and linear programming theory and techniques. The problems that were addressed are variations of classical problems, such as linear programming and the first-order theory of linear arithmetic, that have been researched fordecades by the computer science, the operations research, and the mathematics community. Furthermore, efficient decision algorithms have been devised for all polynomially solvable classes that were examined. The broader impact of this project is multidimensional. It served to significantly advance learning and discovery in analysis, algorithms, and implementations,which also resulted in writingand publishing high quality papers. The PI, the postdoctoral associates, and the graduate students that worked for this projecthad the opportunity to publish high quality papers in various journals (e.g., TCS, AMAI) and international conferences. Moreover, this project effectively integrated education and research to train undergraduate and graduate students and to promote a thriving and active computer science program at West Virginia University. The courses taught by the PI have improved students’ abilities to conduct research and communicatethe results to their peers. The PI has also mentored several undergraduate students, graduate students, and postdocs. Further, the project facilitated the development of collaborative relationships with research laboratories and other academic institutions,thereby enhancing the local research infrastructure.
