%0 Journal Article
%T H-GRASP: advanced GRASP-based hybrid SAT solver<br>H-GRASP：一种基于GRASP改进的混合SAT解法器*
%A TANG Yu-lan
%A ZHANG Hui-guo
%A YU Zong-guang
%A CHEN Jian-hui
%A <br>唐玉兰
%A 张惠国
%A 于宗光
%A 陈建慧
%J 计算机应用研究
%D 2010
%I 
%X In order to improve the limitations of GRASP, this paper proposed a new hybrid algorithm (H-GRASP), which could resolve the problem of mixed constraints of pseudo-Boolean (PB) and conjunctive normal from (CNF). The new method adopted the cutting-plane technique to draw inferences among PB constraints and combined it with generic implication graph analysis for conflict-induced learning. Presented a thorough comparison of the new technique against the other two methods-integer linear programming (ILP) and pure SAT-based methods also. Experimental results prove that H-GRASP has significantly reduced running time and sped up, while keeping the overhead of adding it into the problem low.
%K Boolean satisfiability(SAT)
%K cardinality constraint
%K integer linear programming
%K pseudo-Boolean(PB)<br>布尔可满足性
%K 势约束
%K 整数线性规划
%K 伪布尔
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=02C99CF4D82E86F363174A2402C79B2F&yid=140ECF96957D60B2&vid=DB817633AA4F79B9&iid=38B194292C032A66&sid=F90340A344159B2E&eid=65A51D0EBEB846F5&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=23