一种增加了对称破缺的改进子集可满足性算法

• 作者: 于宗光 唐玉兰 张惠国
• 来源期刊: 江苏大学学报（自然科学版）
• 学科: 工学
• 关键词: 基准 布尔函数 现场可编程门阵列 布线算法 对称
• 年，卷（期）: 2010,（3）
• 所属期刊栏目: 电气电子工程
• 页码范围: 318-322
• 分类号: TN79.2
• 字数: 4199字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-7775.2010.03.016

摘要

为了消除子集可满足性算法在布线过程中带来运行时间增加的负面影响,提出了一种新的布线流程.针对子集可满足性算法在求解同时增加额外的变量和字句,而使得对称数量按指数级增长的问题,选用增加静态对称破缺的方法对合取范式(CNF)进行预处理,侦测并破缺其中的对称,从而达到减少搜索路径的目的.用简化图自同构的方法侦测所有对称,在增加合适的对称破缺判定(SBPs)后,限制搜索在空间的非对称领域进行,从而减少了搜索空间,而不影响CNF公式的可满足性.然后把预处理过的CNF送入布尔可满足性(SAT)解法器进行求解.试验结果表明,这种方法可以显著减少运行时间,加速求解过程.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张惠国	江南大学信息工程学院	8	28	4.0	5.0
2	唐玉兰	江南大学信息工程学院	9	27	3.0	5.0
3	于宗光	江南大学信息工程学院	89	354	9.0	14.0