Local Search for Solving Satisfiability of Polynomial Formulas
科研大讨论系列报告
报告题目(Title)：Local Search for Solving Satisfiability of Polynomial Formulas
报告人(Speaker)：夏壁灿 教授 (北京大学)
地点(Place)：后主楼1124
时间(Time)：2023年6月2日(周五), 11：00-12：00
邀请人(Inviter)：郭来刚
报告摘要
Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combinations of polynomial equations and inequalities with integer coefficients and real variables. In this talk, we introduce a local search algorithm for a special subclass of SMT(NRA), where all constraints are strict inequalities. Experiments show the algorithm is competitive with state-of-the-art SMT solvers, and performs particularly well on those formulas with high-degree polynomials.
主讲人简介
夏壁灿，北京大学数学科学学院教授，中国工业与应用数学学会常务理事，中国数学会计算机数学专委会副主任。曾担任北京大学数学科学学院副院长，北京大学数学科学学院信息科学系主任。担任 Mathematics in Computer Science、系统科学与数学等多个权威期刊编委，主持或参与多个国家重大项目。研究兴趣包括：符号计算，程序与混成系统验证，自动定理证明。
