Penalty Formulations and Trap-Avoidance Strategies for Solving Hard Satisfiability Problems  

作　　者：BenjaminW.Wah ZheWu 

机构地区：[1]DepartmentofElectricalandComputerEngineering,UniversityofIllinois,Urbana,IL61801,U.S.A. [2]OracleCorporation,OneOracleDrive,Nashua,NH03062,U.S.A.

出　　处：《Journal of Computer Science & Technology》2005年第1期3-17,共15页计算机科学技术学报（英文版）

基　　金：美国自然科学基金

摘　　要：In this paper we study the solution of SAT problems formulated as discretedecision and discrete constrained optimization problems. Constrained formulations are better thantraditional unconstrained formulations because violated constraints may provide additional forces tolead a search towards a satisfiable assignment. We summarize the theory of extended saddle pointsin penalty formulations for solving discrete constrained optimization problems and the associateddiscrete penalty method (DPM). We then examine various formulations of the objective function,choices of neighborhood in DPM, strategies for updating penalties, and heuristics for avoidingtraps. Experimental evaluations on hard benchmark instances pinpoint that traps contributesignificantly to the inefficiency of DPM and force a trajectory to repeatedly visit the same set ofor nearby points in the original variable space. To address this issue, we propose and study twotrap-avoidance strategies. The first strategy adds extra penalties on unsatisfied clauses inside atrap, leading to very large penalties for unsatisfied clauses that are trapped more often and makingthese clauses more likely to be satisfied in the future. The second strategy stores information onpoints visited before, whether inside traps or not, and avoids visiting points that are close topoints visited before. It can be implemented by modifying the penalty function in such a way that,if a trajectory gets close to points visited before, an extra penalty will take effect and force thetrajectory to a new region. It specializes to the first strategy because traps are special cases ofpoints visited before. Finally, we show experimental results on evaluating benchmarks in the DIMACSand SATLIB archives and compare our results with existing results on GSAT, WalkSAT, LSDL, andGrasp. The results demonstrate that DPM with trap avoidance is robust as well as effective forsolving hard SAT problems.In this paper we study the solution of SAT problems formulated as discretedecision and discrete constrained optimization problems. Constrained formulations are better thantraditional unconstrained formulations because violated constraints may provide additional forces tolead a search towards a satisfiable assignment. We summarize the theory of extended saddle pointsin penalty formulations for solving discrete constrained optimization problems and the associateddiscrete penalty method (DPM). We then examine various formulations of the objective function,choices of neighborhood in DPM, strategies for updating penalties, and heuristics for avoidingtraps. Experimental evaluations on hard benchmark instances pinpoint that traps contributesignificantly to the inefficiency of DPM and force a trajectory to repeatedly visit the same set ofor nearby points in the original variable space. To address this issue, we propose and study twotrap-avoidance strategies. The first strategy adds extra penalties on unsatisfied clauses inside atrap, leading to very large penalties for unsatisfied clauses that are trapped more often and makingthese clauses more likely to be satisfied in the future. The second strategy stores information onpoints visited before, whether inside traps or not, and avoids visiting points that are close topoints visited before. It can be implemented by modifying the penalty function in such a way that,if a trajectory gets close to points visited before, an extra penalty will take effect and force thetrajectory to a new region. It specializes to the first strategy because traps are special cases ofpoints visited before. Finally, we show experimental results on evaluating benchmarks in the DIMACSand SATLIB archives and compare our results with existing results on GSAT, WalkSAT, LSDL, andGrasp. The results demonstrate that DPM with trap avoidance is robust as well as effective forsolving hard SAT problems.

关 键 词：knowledge representation and reasoning techniques of algorithms constraintsatisfaction boolean satisfiability penalty formulation saddle point SEARCH 

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