形式化验证是保证硬件系统设计正确性的一种有效的手段,它基于已建立的形式化规格,分析系统的相关特性,以评判系统是否满足期望。命题可满足问题求解是其中重要的分析推理引擎。命题可满足问题(简称为可满足问题或SAT问题)是指,对于一个表示为合取范式(CNF)的命题逻辑公式,是否存在对其所有变量的一个真值赋值使之成立。随着硬件系统规模日益增大,形式化验证过程中产生的SAT问题规模也急剧增长。开放环境下的SAT求解服务,可利用云或网格等提供的弹性计算资源,满足不同规模问题的求解需求,成为一种有效的应对手段。但是,开放计算环境在为用户提供使用便利的同时,未授权访问等问题对用户的数据安全提出了严峻挑战。为解决该问题,本文针对硬件形式化验证中SAT问题的特点,以提高方法的可用性和效能为出发点,系统地研究了在开放计算环境下进行SAT问题求解时,数据隐私保护的若干关键问题,并实现了SAT求解在对偶综合设计中的应用。本文的主要研究内容和创新点如下。1.开放计算环境下基于加噪混淆的SAT求解框架。现有保护SAT问题数据隐私的方法包括基于加密和基于数据分割两类。这些算法都依赖于全空间遍历求解,在效率和实用性方面存在不足。本文通过对SAT问题自身逻辑特点的分析,提出了基于加噪混淆算法的求解方法。该方法通过在原始CNF公式中无缝的混入噪音公式,在隐藏原有的结构信息的同时,保持原有的CNF数据形式和解空间,从而复用已有的SAT求解算法。本文从理论上证明了该算法的正确性并通过仿真实验证明了该算法的高效性。2.结构感知的混淆策略。识别混淆后CNF公式结构的困难程度,是衡量混淆算法有效性的重要指标。本文研究了硬件设计中CNF公式携带的结构信息特征,提出结构感知的加噪策略。该策略将原始公式的结构映射至新的带噪声结构,使得该新结构与原始结构不存在明确对应,从而增大第三方恢复出原始结构的难度。本文从理论上论证了结构感知混淆算法的有效性,并通过大量的仿真实验分析验证了策略对性能的影响。3.解空间投影等价的混淆算法。寻找特定CNF公式的所有解的算法,称为可满足问题遍历(ALL-Solution-SAT,简称为ALLSAT)算法。该算法构成了对上述混淆算法的一个潜在威胁:通过求解出全空间的解,并将在所有解中具有相同唯一赋值的变量作为候选噪音变量,进而从混淆后的公式中识别出原始公式。为了解决该问题,本文研究了解空间投影等价的混淆算法,以打破噪音变量必然是相同单一赋值的断言,以抵御上述基于ALLSAT的攻击。4.解空间加噪的混淆算法。在研究了上述保护输入数据结构信息的算法后,本文进一步研究了隐藏SAT问题求解结果的方法。针对输出信息隐藏,本文提出了解空间上估计的CNF混淆算法。通过在原始公式中混入具有多个解的噪音公式,使得混淆后公式的解空间为原始解空间的上估计,从而实现对原始解的隐藏。由于上估计的CNF混淆算法可能会多次调用SAT求解,其调用的概率取决于真实解与噪音解的比率。本文还讨论了结合投影等价和上估计两种混淆特性,来实现解空间可调制的混淆算法。5.基于可满足问题求解的流控机制迭代特征化算法。特征化流控数据是自动生成流控感知解码器的关键,本文研究了基于可满足问题求解的迭代特征化方法。该算法在每一次迭代中,为每一个尚未被遍历的解A,利用其对应的余因子化简R以满足产生Craig插值的要求。而该插值是A的一个充分扩展。该迭代过程是停机的,且其性能比传统的完全解遍历算法有巨大的提升。综上所述,本文针对形式化验证中的SAT问题,对其数据安全和应用的若干关键问题进行了深入的研究,提出了具有实用性、低开销的解决方案,并通过理论分析和大量的仿真实验验证了所提出算法的有效性和性能,对于促进SAT计算外包服务的实用化有一定的理论意义和应用价值。