OK库：为解决SAT问题引入的整体研究平台

OK库是一个开源数据库，被用于支持广义SAT问题领域的研究和发展，该库可从下述网址获得：http：//www．ok—sat—library．org．。本文中我们讨论了这个数据库的发展历史、开发动机和组成架构，并概述了其当前的状况。文章解释了它与现有其它平台的差别：在我们看来，OK库的方法是“整体性”的，也即OK库不仅包含程序代码，也包括用于处理和评价实验（以及实验结果本身）的研究计划和方法。因此可以把OK库理解为IRE，即集成研究环境（但它并非只是构建一个单独的集成块，而是基于Unix／Linux传统的工具箱）。“广义可满足性问题”被理解为SAT问题向CSP的推广，本文中讨论了其中的基本思路。作为结束，本文阐述了解决高级核心SAT的（我们所认为的）十个基本研究问题。