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.