编译满足性问题中的相变现象实验研究

111 浏览量更新于2024-08-27 收藏 749KB PDF 举报

"满足满意度问题中相变的实验分析" 这篇研究论文探讨了在编译满足性问题（satisfiability problems）时出现的相变现象，特别是针对k-满足性问题（k-SAT）转化为可处理语言的过程。相变现象在过去的十年里在复杂组合问题，如SAT问题中受到了广泛的研究。相变是指在问题难度突然增加或减少的现象，通常与问题的可解性阈值相关。作者GAO Jian、WANG Jia Nan和YIN Ming Hao分别来自大连海事大学的信息科学与技术学院以及东北师范大学的计算机科学学院。他们的工作主要集中在通过实证方法研究将k-SAT问题编译到两种可处理语言——有序二元决策图（Ordered Binary Decision Diagram, OBDD）和确定性可分解否定正规形式（Deterministic Decomposable Negation Normal Form, DDNNF）时的相变行为。实验是通过大量测试来完成的，这些测试旨在揭示当问题规模或参数变化时，从不可解到可解状态的转变。OBDD和DDNNF是两种常用于表示和解决逻辑问题的有效数据结构，它们可以帮助理解k-SAT问题在转换过程中的复杂性和效率。相变的实验分析对于理解算法性能和优化策略至关重要，因为它们可以帮助识别问题的难解区间。在实际应用中，例如软件验证、电路设计和人工智能等领域，理解和预测相变可以指导更有效的求解策略，提高解决问题的效率。论文中，作者可能详细分析了实验数据，包括不同k值下的成功编译率、计算时间以及资源消耗等指标。他们可能还讨论了这些相变现象如何随着问题规模的增加而变化，并可能提出了新的理论见解或改进现有算法的建议。这篇研究论文对理解和利用复杂问题中的相变现象提供了深入的实验依据，对于优化问题求解和算法设计具有重要的理论和实践意义。通过这样的研究，我们可以更好地预测和控制在解决大规模逻辑问题时可能出现的困难，从而提高计算效率。

Gao J, et al. Sci China Inf Sci March 2015 Vol. 58 032104:3

instances into OBDD and d-DNNF respectively, which shows that these languages suﬀer the easy–hard–

easy pattern, and the sizes of compilation results increase as the ratio of clauses to variables grows from 0

but decrease when the ratio exceeds a certain point. Also, we observe a phase transition of polynomial–

exponential increment of sizes when compiling instances with very small ratio of #clauses to #variables.

Additionally, we analyze a phase transition phenomenon on prime implicants and point out that average

length of prime implicants is nearly half of the total number of variables around the peak point of the

easy–hard–easy pattern.

2 Background of random k-SAT model

Many academic and real-world problems can be transformed into k-SAT problems and solved by eﬃcient

SAT solvers. However, it is well known that k-SAT is NP-complete for k>2, so designing search

algorithms to solve SAT problems eﬃciently is an essential issue in artiﬁcial intelligence. To evaluate the

eﬃciency of SAT algorithms, Mitchell et al. [30] introduced a model for generating random SAT instances,

which can produce hard instances as it was claimed. Compared with instances derived from industrial

areas, this model can obtain large amount of instances whose size and diﬃculty can be controlled by

parameters. As a result, it has become a canonical benchmark to test various SAT algorithms. Meanwhile,

theoretical analyses on the random k-SAT model have been made [3]. For example, the properties of

phase transitions have been identiﬁed that can be used to analyze average computational complexity.

In the SAT model discussed in [30], there are three parameters k, n,andm that are employed to

generate SAT instances, where k is the length of clauses, n is the number of variables, and m is the

number of clauses. We use a ratio r to represent m/n. Instances are produced by generating m clauses

uniformly and independently, where each clause is generated by selecting k variables without replacement

from n variables and negating each variable with probability 0.5, so all clauses generated are of the same

length.

Empirical and theoretical studies have demonstrated that there are easy–hard–easy patterns when

solving the random k-SAT instances, regardless of the algorithm used. Lots of experiments have shown

that the soluble-to-insoluble phase transition will occur when r is up to a ﬁxed value. For example,

when r is about 4.3 in 3-SAT [30], mean runtimes spent on ﬁnding a solution by SAT algorithms are

often extremely high because the instances generated are in the phase transition region. As r increases

from 0, mean runtimes increase ﬁrst but decrease when r is larger than the value at the transition

point. However, it seems to be diﬃcult to locate exact positions of the transition points in k-SAT by

theoretical proof, as only lower and upper bounds have been found for the positions [3]. On the other

hand, similar phenomenon also exists in counting problems (e.g., #SAT [19] and #CSP [31]). In the

general case, #SAT is #P-complete, so it is considered to be harder than SAT problems, and algorithms

for solving this problem should count the number of solutions in a given SAT instance. Mean runtimes

of several #SAT solvers have been investigated, and the results show that those solvers also suﬀer the

easy–hard–easy pattern, but the hardest regions of those #SAT algorithms are diﬀerent. For instance,

it was reported that an algorithm, called Counting Davis-Putnam [32], reaches its peak runtime when

r =1.2 in the experiments of #3-SAT, but the peak point of another algorithm, called Decomposing

Davis-Putnam [33], occurs when r =1.5.

In the following sections, we will show that the knowledge complication also undergoes the easy–hard–

easy pattern.

3Basicconjecture

Let X

(P ) be the size of the compilation result, where L is the target language to which the SAT instance

P is compiled (we regard the number of nodes as the size approximately, when L is OBDD or d-DNNF).

Deﬁnition 1. Given n, r, k and a target language L, average size E(X

)) is deﬁned as follows:

E(X

)) = (ΣX

))/|P

| (1)

剩余10页未读，继续阅读

weixin_38556668

粉丝: 5
资源: 981

编译满足性问题中的相变现象实验研究

CFX 12相变分析

相变材料步冷过程模拟分析

随机均衡正则恰当(2s,k)-sat问题的相变分析

与无相变时相比，相变传热有哪些不同的换热规律？

固态相变matlab源代码

ABAQUS模拟马氏体相变

comsol 马氏体相变相场

comsol 相变材料

comsol激光加热多孔介质相变

相变在《Micromechanics of Composite Materials》中的介绍

最新资源