High Performance Model Construction

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

Two software systems, SATO (SAtisfiability Test Optimized) and SEM (a System for Enumerating Models), developed with the NSF support, have been widely and successfully used for solving many problems often considered a challenge for automated reasoning systems. SATO and SEM were used to solve over a hundred cases of of previously open problems in algebras and logics. The proposed research will further increase the reasoning power of SATO and SEM. A new experimental software system called HOTTER (a Humble OTTER) will be fine-tuned for the high-performance first-order satisfiability testing. The main objective of this research is to develop high performance model generation techniques. These software systems will be serve as an environment for experimenting and developing these techniques, and will be available to the public. Many computational problems from a variety of fields, i.e., software and hardware verification, circuit design verification, scheduling and planning, can be reformulated as a model generation problems. Instead of creating special-purpose software for these problems, an alternative and competitive approach is to write the problems in a model-generation language and then submit the problems to a model generator optimized to this language. Another objective of this research is to support this approach by designing a general-purpose language for model generation, and implementing it with SATO, SEM, and HOTTER as its components. The language will provide an easy-to-use model generator for people in various fields.