资源描述：
《Satisfiability Checking满足能力的检验》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、SatisfiabilityChecking:TheoryandApplicationsErikaAbrah´´am(B)andGereonKremerRWTHAachenUniversity,Aachen,Germanyabraham@cs.rwth-aachen.deAbstract.Satisfiabilitycheckingaimstodevelopalgorithmsandtoolsforcheckingthesatisfiabilityofexistentiallyquantifiedlogicalformu-las.
2、BesidespowerfulSATsolversforsolvingpropositionallogicformu-las,sophisticatedSAT-modulo-theories(SMT)solversareavailableforawiderangeoftheories,andareappliedasblack-boxenginesformanytechniquesindifferentareas.Inthispaperwegiveashortintroductiontothetheoreticalfounda
3、tionsofsatisfiabilitychecking,mentionsomeofthemostpopulartools,anddiscussthesuccessfulembeddingofSMTsolversindifferenttechnologies.1IntroductionFirst-order-logicisapowerfulmodellingformalismfrequentlyusedtospecifyproblemsindifferentareaslikeverification,terminationana
4、lysis,testcasegen-eration,controllersynthesis,equivalencechecking,combinatorialtasks,schedul-ing,planning,andproductdesignautomationandoptimisation,justtomentionafewwell-knownexamples.Oncetheproblemisformalised,algorithmsandtheirimplementationsareneededtocheckthev
5、alidityorsatisfiabilityoftheformulas,andincasetheyaresatisfiable,toidentifysatisfyingsolutions.Algorithmstosolvethisproblemarecalleddecisionprocedures.Inmathematicallogic,intheearly20thcenturysomenoveldecisionpro-ceduresweredevelopedforarithmetictheories.Withtheadve
6、ntofcomputersystems,bigeffortsweremadetoprovideautomatedsolutionsinformofprac-ticallyfeasibleimplementationsofdecisionprocedures.Intheareaofsymboliccomputation,thisdevelopmentledtocomputeralgebrasystemssupportingallkindsofscientificcomputations.Anotherlineofresearch
7、,satisfiabilitychecking[10],startedtofocusonthemorespecificaimofcheckingthesatisfiabilityofexistentiallyquantifiedlogicalformulas.ForBooleanpropositionallogic,whichisknowntobeNP-complete,inthelate’90simpressiveprogresswasmadeintheareaofsatisfiabilitychecking,resultingi
8、npowerfulSATsolvers.Thefirstideausedresolutionforquanti-fierelimination[30],butithadseriousproblemswiththeexplosionofthememoryrequirementswithincreasingpr
