一句话：提出 PSMT 问题与 Prob-MCSAT 算法，将概率分布引入 SMT 求解，使解呈现合理的分布趋势。
SMT 求解器广泛用于程序验证、分析与测试生成，但其确定性算法对同一公式每次运行都输出相同解，且在实际实例中解往往难以理解。为让求解器给出更合理的解，本文把 SMT 求解与概率结合，定义了新问题 PSMT：在满足约束的前提下要求变量服从某一分布。作者基于主流 SMT 求解算法 MCSAT 定义了「约束下的分布」，并据此提出 Prob-MCSAT 算法，在 MCSAT 框架中为变量引入概率。可视化示例表明，由此得到的赋值会依据概率形成清晰的趋势。
SMT (Satisfiability Modulo Theories) has been widely used in program verification, analysis, and test generation. But sometimes, SMT solver outputs incomprehensible solutions, especially for practical instances. Besides, due to the design of the deterministic algorithms, for a given formula, the result of each run is the same. In this paper, we concentrate on combining SMT solving with probability, which will instruct the SMT solver to give some plausible solutions. We define a special problem: PSMT, which allows solving an SMT instance with variables conforming to a certain distribution. We define distribution under constraint for PSMT, which is based on MCSAT (Model Constructing Satisfiability), a mainstream SMT-solving algorithm. We propose the Prob-MCSAT algorithm, which combines the MCSAT algorithm and introduces the probability to variables. The visualized examples show that the resulting assignments will form a clear trend based on Prob-SMT.
@inproceedings{JiaHMCLHMZ23,
title = {PSMT: Satisfiability Modulo Theories Meets Probability Distribution},
author = {Fuqi Jia and Rui Han and Xutong Ma and Baoquan Cui and Minghao Liu and Pei Huang and Feifei Ma and Jian Zhang},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00183}
}