High Performance Model Construction

在NSF的支持下开发的两个软件系统，SATO(可满足性测试优化)和SEM(模型枚举系统)，已经被广泛并成功地用于解决许多通常被认为是自动推理系统的挑战的问题。用佐藤和扫描电子显微镜解决了一百多个以前在代数和逻辑中未解决的问题。提出的研究将进一步提高佐藤和结构方程的推理能力。一种新的实验软件系统Hotter(一种Humble Otter)将进行微调，以进行高性能的一阶可满足性测试。本研究的主要目的是开发高性能的模型生成技术。这些软件系统将作为试验和开发这些技术的环境，并将向公众开放。许多来自各种领域的计算问题，即软硬件验证、电路设计验证、调度和规划，都可以转化为模型生成问题。与为这些问题创建专用软件不同，另一种竞争的方法是用模型生成语言编写问题，然后将问题提交给针对该语言进行优化的模型生成器。这项研究的另一个目标是通过设计一种通用的模型生成语言来支持这种方法，并以Sato、SEM和Hotter作为其组件来实现它。该语言将为各个领域的人们提供一个易于使用的模型生成器。

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.