2024年5月9日发(作者：)

JournalonSatisfiability,BooleanModelingandComputation2(2006)165-189

Pueblo:AHybridPseudo-BooleanSATSolver

ah

ElectricalEngineeringandComputerScienceDepartment,

UniversityofMichigan,AnnArbor,MI

hsheini@

karem@

Abstract

ThispaperintroducesanewhybridmethodforefficientlyintegratingPseudo-Boolean

(PB)constraintsintogenericSATsolversinordertosolvePBsatisfiabilityandoptimiza-

evethis,weadoptthecutting-planetechniquetodrawinferences

amongPBconstraintsandcombineitwithgenericimplicationgraphanalysisforconflict-

eaturesofourapproachincludealight-weightandefficienthybrid

learningandbackjumpingstrategyforanalyzingPBconstraintsandCNFclausesinorder

tosimultaneouslylearnbothaCNFclauseandaPBconstraintwithminimumoverhead

ltechniquesforhandlingtheoriginal

l,ourmethodbenefitssignificantlyfrom

thepruningpowerofthelearnedPBconstraints,whilekeepingtheoverheadofadding

paper,wealsoaddresstwoothermethodsforsolving

PBproblems,namelyIntegerLinearProgramming(ILP)andpre-processingtoCNFSAT,

mental

comp-

tionally,weprovidedetailsoftheMiniSAT-basedimplementationofoursolverPuebloto

enablethereadertoconstructasimilarone.

Keywords:satisfiability,SATsolver,pseudo-Boolean,inference-basedlearning

SubmittedOctober2005;revisedMarch2006;publishedMarch2006

uction

RecentadvancesinalgorithmsforBooleanSatisfiability(SAT)haveledtoasignificant

rgedesignandanalysis

problemsfromthefieldofElectronicDesignAutomation(EDA)arenowroutinelycastas

SATinstances(withmillionsofCNFclausesandtensofthousandsofvariables)andquickly

solvedusingthesepowerfulsolvers.

ModernSATsolversforsystemsofBooleanconstraintsinConjunctiveNormalForm

(CNF)arebasedontheDLLbacktracksearchprocedureofDavis,Logemann,andLove-

land[11]augmentedwithpowerfulconflict-basedlearning[28]andefficientwatched-literal

schemes[29]forBooleanconstraintpropagation(BCP).Whileprovingtobequiteversatile

forawiderangeofapplications,CNFconstraintsarenotalwaysthemosteffi

closely-relatedlinear0-1inequalitiesknownasPseudo-Boolean(PB)constraintshavebeen

widelyusedtoefficientlyencodemanyproblemsrangingfromlogicsynthesis[1]andverifi-

cation[5]tonumerousOperationsResearchapplications[4].Additionally,PBconstraints

areincreasinglyusedtorepresentobjectivefunctionsinoptimizationapplications,suchas

c

2006DelftUniversityofTechnologyandtheauthors.