SatisfiabilityandItsApplications1ShaoweiCai(蔡少伟)2020.2.11中国科学院软件研究所个人简介研究领域:逻辑推理与搜索教育经历：•2012.7-2014.7Griffith大学IIIS研究所（应用数学）博士•2008.9-2012.7北京大学计算机软件与理论专业博士•2004.9-2008.7华南理工大学计算机科学与技术专业本科工作经历：•2017.9-至今中国科学院软件研究所计算机科学国家重点实验室研究员•2014.7-2017.9中国科学院软件研究所计算机科学国家重点实验室副研究员2个人简介•发表论文60+篇，其中CCFA类30+篇，ArtificialIntelligence6篇•中国科学院大学岗位教授•中科院青促会信息与管理分会会长•(S)PC:AAAI2015-2020(CCFA)，IJCAI2015-2020(CCFA)•FrontiersofComputerScience（FCS）青年编委3个人简介•逻辑推理与搜索是人工智能领域的两个基础方法，且有密切联系。•主要研究成果：•处理局部搜索循环问题的通用策略•命题逻辑可满足性求解•基于推理与搜索的大规模组合优化4Outline⚫Satisfiability⚫ConfigurationCheckingforSAT⚫AdvancingConflictDrivenClauseLearning(CDCL)⚫CombinatorialOptimizationbyReasoningandSearch⚫SatisfiabilityModuloTheories(SMT)Solving5Outline⚫Satisfiability⚫ConfigurationCheckingforSAT⚫AdvancingConflictDrivenClauseLearning(CDCL)⚫CombinatorialOptimizationbyReasoningandSearch⚫IncrementalSatisfiabilityModuloTheories(SMT)Solving6Satisfiability•Logic,especiallyFirstorderlogic,isthelanguageofmathematics,andistheformallanguagetodescribeourworld.•Logicisthebasisofmathematicalreasoningandautomatedreasoning.•Acorestudyoflogicconcernsthesatisfiabilityoflogicalformulas,whichhaswideapplicationsinartificialintelligenceaswellasmanyareasofcomputerscience.Satisfiability:Givenalogicalformulaφ,testwhetherthereisanassignmenttothevariablesthatmakesφtrue.7Satisfiability8SatisfiabilitySatisfiabilityFindingasolutionCheckingvaliditySATReasoningTheoremproving,Systemverification,Knowledgerepresentation,Decisionprocedure,Agents,…ConstraintsScheduling,Resourceallocation,Logistics,HardwaredesignSoftwareEngineering,…9PropositionalSatisfiability(SAT)•AsetofBooleanvariables:𝑥1,𝑥2,…𝑥𝑛•Literals:𝑥1,¬𝑥1,𝑥2,¬𝑥2,…𝑥𝑛,¬𝑥𝑛•Clauses:𝑥1∨...
