简介：InthispaperwestudythesolutionofSATproblemsformulatedasdiscretedecisionanddiscreteconstrainedoptimizationproblems.Constrainedformulationsarebetterthantraditionalunconstrainedformulationsbecauseviolatedconstraintsmayprovideadditionalforcestoleadasearchtowardsasatisfiableassignment.Wesummarizethetheoryofextendedsaddlepointsinpenaltyformulationsforsolvingdiscreteconstrainedoptimizationproblemsandtheassociateddiscretepenaltymethod(DPM).Wethenexaminevariousformulationsoftheobjectivefunction,choicesofneighborhoodinDPM,strategiesforupdatingpenalties,andheuristicsforavoidingtraps.ExperimentalevaluationsonhardbenchmarkinstancespinpointthattrapscontributesignificantlytotheinefficiencyofDPMandforceatrajectorytorepeatedlyvisitthesamesetofornearbypointsintheoriginalvariablespace.Toaddressthisissue,weproposeandstudytwotrap-avoidancestrategies.Thefirststrategyaddsextrapenaltiesonunsatisfiedclausesinsideatrap,leadingtoverylargepenaltiesforunsatisfiedclausesthataretrappedmoreoftenandmakingtheseclausesmorelikelytobesatisfiedinthefuture.Thesecondstrategystoresinformationonpointsvisitedbefore,whetherinsidetrapsornot,andavoidsvisitingpointsthatareclosetopointsvisitedbefore.Itcanbeimplementedbymodifyingthepenaltyfunctioninsuchawaythat,ifatrajectorygetsclosetopointsvisitedbefore,anextrapenaltywilltakeeffectandforcethetrajectorytoanewregion.Itspecializestothefirststrategybecausetrapsarespecialcasesofpointsvisitedbefore.Finally,weshowexperimentalresultsonevaluatingbenchmarksintheDIMACSandSATLIBarchivesandcompareourresultswithexistingresultsonGSAT,WalkSAT,LSDL,andGrasp.TheresultsdemonstratethatDPMwithtrapavoidanceisrobustaswellaseffectiveforsolvinghardSATproblems.