基于关键文字的求解SAT问题的启发式算法  

A Heuristic Algorithm for Solving the Satisfiability Problem Based on the Key Literal

作　　者：秦永彬[1] 张秋菊[1] 

机构地区：[1]贵州大学计算机科学与信息学院,贵阳550025

出　　处：《计算机与数字工程》2010年第10期1-4,共4页Computer & Digital Engineering

基　　金：国家自然科学基金(编号:60863005);贵州省省长基金(编号:200404);贵州大学自然科学青年基金(编号:2009021)资助

摘　　要：逻辑公式的可满足问题的求解方法是近几年研究的重点,通过对逻辑公式的关键文字和骨干变元集的研究与分析,使用启发式算法寻找公式的关键文字,在公式化简中引入关键文字规则,给出了一种新的求解SAT问题的启发式算法。The solution method of the satisfiability problem of the logic formula is the focus of the study in recently years.Through the study and analysis of the key word and backbone of the logic formula,using the heuristic algorithm to search the key literal of the formula,introducing the rule of the key literal into the simplification of the formula,and giving out a new heuristic algorithm for the satisfiability problem.

关 键 词：关键文字 骨干变元集 可满足(SAT) 启发式算法 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]