4月11日马菲菲讲座:Satisfiability Checking and Model Counting for Propositional Logic and SMT

Title: Satisfiability Checking and Model Counting for Propositional Logic and SMT

 

马菲菲 中科院软件所 副研究员

 

时间:4月11日下午3:00-6:00

地点:北京大学第一教学楼304

 

Abstract:

Propositional Logic has been recognized as one of the corner stones of reasoning in philosophy and mathematics.  The propositional satisfiability (SAT) is a classical NPC problem which has been extensively investigated.  In recent years, Satisfiability Modulo Theories (SMT) has become a hot research topic in automated reasoning.  SMT is a decision problem, i.e., deciding the satisfiability of logical formulas with respect to combinations of background theories. SMT can be regarded as an extension to SAT, and is much more expressive than SAT. Tremendous progresses have been made in the solving techniques for SAT and SMT. However, in many applications, it is desirable to count the number of models of these formulas.  In this talk, I will introduce some techniques in solving and model counting for SAT and SMT.


发布时间:2017-04-10 09:45:28
联系我们      关于本站      版权所有© 2009-2017  北京大学哲学系逻辑、语言与认知研究中心      地址:北京大学人文学苑二号楼