H-GRASP: advanced GRASP-based hybrid SAT solver
H-GRASP：一种基于GRASP改进的混合SAT解法器*

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.