增量式可满足性问题的解搜索方法、系统及计算机设备

本发明提供一种增量式可满足性问题的解搜索方法、系统及计算机设备，该方法包括：将两个时序逻辑电路在各时钟周期形成的Miter电路分别映射为一个合取范式，选取指定时钟周期对应的合取范式为基础合取范式，后续时钟周期对应的合取范式为增量合取范式，计算增量合取范式相对基础合取范式的增量子句；将基础合取范式的满足解作为基础解，对增量合取范式进行解搜索时，根据待求解的增量合取范式相对基础合取范式的增量子句将基础解中除了与增量子句相关的解变量以外的其他解变量设置为固定不可翻转状态，对可翻转解变量进行变量翻转构造SLS算法的初始解，使得当应用SLS求解增量式可满足性问题时，不必重新完全构造问题，降低求解时间与开销。