Solving Quantified Algebraic Constraints

点击翻译按钮获取中文摘要

Proposal #0097976Hong, HoonNorth Carolina State UThe long term objective of this research is to develop mathematical theories, algorithms, and software libraries/packages for efficiently solving quantified algebraic constraints (quantified boolean expressions of polynomial equations/inequalities over real numbers), which can handle large real life problems. This particular project will focus on moderate size inputs (up to about 10 variables). There are still many interesting real life problems of moderate sizes.The potential impact is as follows. Many important and difficult problems in mathematics, scientific, engineering and industry can be reduced to that of solving quantified algebraic constraints. Thus the availability of efficient algorithms/softwares for solving quantified algebraic constraint will have a broad impact on science and industry.The specific approaches are as follows.- Allow approximate solutions.The subject of quantifier constraint solving arose originally as a problem in logic. Naturally, obtaining "exact" solution has been the goal of the previous research efforts. In order to obtain exact solutions, most calculations have been carried out symbolically, suffering from enormous intermediate computation swelling. Further, they had to deal with all the singular/degenerate cases, which are often very expensive computationally to analyze. However, in most real-life problems, approximate solutions are acceptable. In fact, often, there are many uncertain coefficients in constraints, and thus it is even meaningless to try to find exact solutions. Hence, we will allow approximate solutions. During this project period, we will pursue two particular ideas in this direction: "approximate quantification" and "box approximation" of solution sets. Our preliminary investigations suggest that these are very promising ideas/directions.- Utilize the structure of constraints.So far, the constraints have been treated as "flat" objects. For example, the polynomials arising in the constraints have been viewed as "atomic" objects. However, constraints in real life problems usually have intrinsic structures that arise naturally from the structures in the underlying laws/components or from the way how the those laws/components are combined. Thus, we will utilize the structures of given constraints. During this project period, we will study ways to utilize two particular structures: "convexity" of bounded quantifiers and "composition" structure of polynomials. Again, our preliminary investigations suggest that these are very promising ideas/directions.The results will be implemented in a software library and freely distributed on the web, in order to facilitate their application to moderate size real life problems by the scientific and engineering communities.