正则3-可满足性（3-SAT）问题是一个NP难问题，研究正则3-SAT问题解簇结构变化，旨在深入理解该问题的判定难度和可满足性解的分布情况。然而，现有分析模型只研究了接近簇集相变点的几个离散值，在不同约束密度下，缺乏统一的分析模型来描述解簇的结构演变。为了解决这一问题，提出解簇结构相变分析模型（PMSS）。该模型主要思想是采用WalkSAT算法和信息传播算法求得正则3-SAT问题可满足的初始解，再利用随机游走构造该初始解的解簇，并对解簇进行分析。用模块度和社区度量解簇社区结构，用结构熵度量解簇结构复杂性。实验结果表明，PMSS能够准确分析解簇结构演变过程，并且正则3-SAT问题实例的可满足相变点位于13~14，与使用Zchaff求解器得到的相变点一致，进一步验证了PMSS的有效性。

可满足性问题（SAT）是一种NP完全问题，被广泛运用于人工智能和机器学习等研究。恰当可满足性问题（XSAT）是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面，对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题，分析了基础编码和等价编码两种转化方式的公式的部分性质，提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定；其次加入变元所属文字的恰当不可满足计分值，优先处理不易恰当满足的变元；然后使用防重复选择翻转变元的启发式策略减小搜索空间；最后，采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时，相较于ProbSAT，WalkXSAT的变元翻转次数与求解时间显著减少；在求解基础编码转化后的实例中，当实例变元规模大于100时，ProbSAT已失效，而WalkXSAT依然能够在短时间内求解。实验结果表明，所提WalkXSAT精确性高、稳定性强、收敛快。

约束满足问题（CSP）是理论计算机科学领域的组合优化问题，可满足性问题（SAT问题）作为CSP中的一种特殊情形，是理论计算机科学、数理逻辑和人工智能等领域十分关注的热点问题。相变是SAT问题中存在的一种现象，而研究SAT问题的相变现象和相变机制对深入认识SAT问题的难解本质和一般数学现象以及设计更高效的算法求解SAT问题有重要的指导意义。因此，根据近年来国内外学者针对SAT问题的相变现象取得的一些重要研究成果，首先介绍了SAT问题相变的相关知识以及SAT问题的概率分析方法和实例生成模型，其次总结并分析了SAT问题的不可满足相变和可满足相变这两种相变的相变点求解方法和相变阈值，最后展望了SAT问题相变的研究趋势。

已存在的时间戳机制没有解决服务付费问题,即客户在请求时间戳服务机构给他的文档Hash值加盖时间戳时,应该如何向时间戳服务机构支付费用。介绍了已经存在的时间戳机制,基于盲数字签名,提出了一个解决问题的新方案,该方案引入了一个售票实体,解决了服务付费问题,并且基于RSA数字签名,构造了一个完整的时间戳系统。