arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1304.0145cs.AI
收藏

现实SAT问题中的相变和网络结构

Phase Transition and Network Structure in Realistic SAT Problems

McClintock High School(麦克林托克高中)

Soumya C. Kambhampati, Thomas Liu

摘要:

计算机科学中的一个基本问题是理解特定类别的问题何时从计算上容易变为困难。由于其通用性和应用,布尔可满足性问题(又名SAT)经常被用作研究这个问题的工具。从这些研究的一个信号的结果是,SAT问题的硬度表现出一个戏剧性的容易硬相变相对于问题的约束。然而,过去的研究主要集中在SAT实例使用均匀随机分布,其中所有的约束是独立生成的,问题变量都被认为是同等重要的。不幸的是,大多数实际问题都不满足这些假设。我们的项目旨在更深入地了解实践中出现的SAT问题的难度。我们研究两个关键问题:(i)容易到困难的转变如何随着更现实的分布而变化,这些分布捕获了真实问题的邻域敏感性和富-更富的方面,以及(ii)这些变化能否用SAT问题的子句网络的网络属性(如节点中心性和小世界性)来解释。我们的研究结果,广泛的实证研究和网络分析的基础上,提供了重要的结构和计算的见解现实SAT问题。我们广泛的实证研究表明,SAT实例从现实的分布确实表现出相变,但过渡发生更快(在较低的值的约束)比均匀随机分布的实例。我们发现,这种行为可以解释在其条款的网络属性,如特征向量中心性和小世界性(间接测量的聚类系数和平均节点距离)。

英文摘要:

A fundamental question in Computer Science is understanding when a specific class of problems go from being computationally easy to hard. Because of its generality and applications, the problem of Boolean Satisfiability (aka SAT) is often used as a vehicle for investigating this question. A signal result from these studies is that the hardness of SAT problems exhibits a dramatic easy-to-hard phase transition with respect to the problem constrainedness. Past studies have however focused mostly on SAT instances generated using uniform random distributions, where all constraints are independently generated, and the problem variables are all considered of equal importance. These assumptions are unfortunately not satisfied by most real problems. Our project aims for a deeper understanding of hardness of SAT problems that arise in practice. We study two key questions: (i) How does easy-to-hard transition change with more realistic distributions that capture neighborhood sensitivity and rich-get-richer aspects of real problems and (ii) Can these changes be explained in terms of the network properties (such as node centrality and small-worldness) of the clausal networks of the SAT problems. Our results, based on extensive empirical studies and network analyses, provide important structural and computational insights into realistic SAT problems. Our extensive empirical studies show that SAT instances from realistic distributions do exhibit phase transition, but the transition occurs sooner (at lower values of constrainedness) than the instances from uniform random distribution. We show that this behavior can be explained in terms of their clausal network properties such as eigenvector centrality and small-worldness (measured indirectly in terms of the clustering coefficients and average node distance).

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑