付江龍 楊 陽 陳素軍 趙天驕

(1.河北建筑工程學(xué)院，河北 張家口 075000;2.河北科技大學(xué)，河北 石家莊 050000)

可滿足性問題的約束求解器應(yīng)用淺析

付江龍1楊 陽1陳素軍1趙天驕2

(1.河北建筑工程學(xué)院，河北 張家口 075000;2.河北科技大學(xué)，河北 石家莊 050000)

約束求解問題涉及廣泛，解決約束求解問題的一個(gè)重要方法就是SMT理論.本文介紹了兩種利用SMT理論設(shè)計(jì)的約束求解器，分析了其求解原理和主要應(yīng)用，并對以上兩種約束求解器的優(yōu)缺點(diǎn)進(jìn)行探討.約束求解器的研究為解決相對應(yīng)的約束求解問題提供了思路和方法.

約束求解；YICES；HySat

0 引 言

約束問題的求解涉及到計(jì)算機(jī)科學(xué)，醫(yī)學(xué)以及生物學(xué)等很多方面.約束問題可以形式化為一個(gè)三元組：變量V，變量的域D以及約束C.變量的域D是變量可取值的集合，變量Vi只能在它的域Di中進(jìn)行取值；約束C描述了變量V之間必須滿足的關(guān)系.求解約束問題就是在各變量的域D中找到一個(gè)或所有的值S使得各變量之間滿足約束C.

SMT[1]是可滿足性的按模計(jì)算理論.一個(gè)SMT求解器可以判定并求解某些理論衍生出的復(fù)雜公式的可滿足性.SMT工具與SAT工具都是用來解決命題邏輯滿足問題.但不同的是，SAT工具僅僅能解決只包含布爾變量的邏輯命題，而SMT可以解決更為廣泛的命題邏輯問題，這些命題邏輯中可以包含整數(shù)變量，實(shí)數(shù)類型的變量等.這一優(yōu)點(diǎn)可以為有界模型檢測提供了方便，即無需將模型變量都編碼成布爾型變量，只需將得到的含有整數(shù)變量或者實(shí)數(shù)變量的邏輯命題交給SMT工具求解即可[2].

1 約束求解的內(nèi)涵

根據(jù)待解決問題的復(fù)雜程度和命題邏輯，可以把待處理的公式分為線性約束公式和非線性約束公式.其中，線性約束即可理解為一次線性方程約束，而非線性約束可以理解為高次方程約束.約束求解器的主要用途就是求解約束方程或者布爾約束，判斷其可滿足性并求出相對應(yīng)的解，一些約束求解器還可以提供滿足公式的模型.

當(dāng)前很多研究課題把約束求解器作為研究的輔助工具.主要利用約束求解器的兩個(gè)特點(diǎn)，第一可以證明公式的可滿足性，第二約束求解器計(jì)算正確率高且效率高.根據(jù)調(diào)查和研究，國內(nèi)外的涉及到公式求解的課題主要有以下幾個(gè)方面[3]：

1)利用約束求解器，進(jìn)行模型的求解和證明，包括使用SMT求解器，計(jì)算當(dāng)前約束的子類型化并利用一階理論以及類型檢測算法，消除動(dòng)態(tài)測試以及靜態(tài)測試發(fā)現(xiàn)的錯(cuò)誤.

2)利用約束求解器，自動(dòng)分析線索性混成系統(tǒng)的狀態(tài)，并實(shí)現(xiàn)對混成系統(tǒng)有限模型測試的證明引擎.

3)基于約束求解器對時(shí)間自動(dòng)機(jī)的有界模型進(jìn)行檢測.

4)解決非線性的約束問題.

5)解決高度集成的系統(tǒng)問題.

2 主要約束求解器以及其主要應(yīng)用分析

2.1 YICES

2.1.1 YICES求解器原理

YICES[4]是一個(gè)效率高的SMT求解器，它與頻繁使用在軟件和硬件建模的一級理論有著密切的聯(lián)系，這些理論包括算法，未被解釋的功能，位向量，數(shù)組，遞歸數(shù)據(jù)類型等等.除了純粹的解決SMT問題，YICES也可以解決加權(quán)的MAX-SMT問題，計(jì)算不可滿足的核心以及構(gòu)建模型.YICES是用于SAL模型檢測運(yùn)行環(huán)境的主要決定程序，并且它正被集成到PVS理論的證明中.

YICES既作為發(fā)一個(gè)單獨(dú)的工具，又是一個(gè)庫.在它的基本應(yīng)用中，它可以從一個(gè)文件中讀取一個(gè)公式并判斷這個(gè)公式是否是具有可滿足性.如果這個(gè)公式具有可滿足性，YICES也可以選擇輸出一個(gè)模型.對于一些具有半決定能力的公式，例如含有量詞的公式，如果YICES不能說明這個(gè)公式是具有不可滿足行，它將會(huì)返回一個(gè)“unknown”.

YICES還可以用于更加交互式的模式中.YICES包含一個(gè)內(nèi)部的邏輯規(guī)則，即一個(gè)聲明和斷言的集合，并且還提供了一些命令來用于通過增加和刪除這些斷言、檢測當(dāng)前斷言集合的可滿足性、回溯等方法來操控這些規(guī)則.

YICES有它自己的輸入語言，在實(shí)現(xiàn)了SMT-LIB理論的同時(shí)支持遞歸數(shù)據(jù)類型，如元組、記錄和拉姆達(dá)表達(dá)式.這個(gè)語言還可以比SMT-LIB更加復(fù)雜，因?yàn)樗梢匀我獾鼗旌细鞣N理論.這個(gè)語言還提供了一些命令用于給出全部YICES函數(shù)的路徑，包括模型構(gòu)建，MAX-SMT，以及對邏輯規(guī)則的操作.

除了純粹解決SMT問題外，YICES還包含了一個(gè)MAX-SMT解算機(jī).用戶可以給斷言分配數(shù)值權(quán)重，并且要求YICES搜索滿足要求的權(quán)重分配.

2.1.2 YICES當(dāng)前的主要應(yīng)用：

1)邊界模型檢測

YICES通常作為SAT解算機(jī)進(jìn)行有限狀態(tài)機(jī)邊界模型檢測，它也是一個(gè)對于SAL無限狀態(tài)機(jī)邊界模型檢測的默認(rèn)SMT解算機(jī).

2)理論證明

YICES可以自動(dòng)實(shí)現(xiàn)大量的交互式的理論證明.

3)集成學(xué)習(xí)和推理

作為CALO系統(tǒng)的一部分，YICES是一個(gè)概率一致性模塊的主要組件.CALO是學(xué)習(xí)和組織的認(rèn)知助手[5](Cognitive Assistant that Learns and Organizes).這是一個(gè)基于學(xué)習(xí)和推理算法的系統(tǒng)，旨在通過與用于交互來學(xué)習(xí)任務(wù)，適應(yīng)用戶的參數(shù)選擇，并且?guī)椭麄冏詣?dòng)地為任務(wù)規(guī)定路徑.

2.2 HySat

2.2.1 HySat求解器原理

HySat[6]提供了一個(gè)處理程序，可以用來進(jìn)行混成自動(dòng)機(jī)的處理，是一個(gè)高效的約束求解器.

HySat的目標(biāo)的是自動(dòng)探索一個(gè)線性混成系統(tǒng)的狀態(tài)分析，并使用二分邏輯以及真值變量定位計(jì)算可滿足性問題.在解決線性混成自動(dòng)機(jī)的過程中，布爾變量代表了狀態(tài)組件的連續(xù)性.

2.2.2 HySat求解過程

HYSAT利用回溯搜索來減少搜索空間直到剩下一個(gè)足夠充足又足夠小的搜索空間，這個(gè)空間中的數(shù)據(jù)，要滿足公式中的各種限制條件.

就像一個(gè)普通的SAT求解器，HYSAT操作，通過交替地使用兩個(gè)步驟：

1)任意選擇一個(gè)變量，分裂開它的當(dāng)前的間隔并臨時(shí)丟棄在搜索中或高或低的部分.求解器將忽略被丟棄的部分求解出結(jié)果.

2)求解結(jié)果是由一個(gè)推理過程得到的.在推理過程中，這個(gè)求解器提供一系列推理規(guī)則，瀏覽所有的先前的結(jié)果.

假設(shè)，例如，輸入的公式包含單一的約束x*y=8并且初始狀態(tài)x∈[2,4]and y∈[2,4].這個(gè)求解器決定分離這個(gè)x的間隔通過設(shè)定其低的邊界為x≥3.在推倒階段，求解器將會(huì)減少那個(gè)約束空間，由于增加x的下界，這個(gè)y的上界可以減小到8/3，因?yàn)檫@個(gè)約束是x*y=8，在斷言y≤8/3后，因此將搜索空間減小到[3,4]×[2,8/3],求解器會(huì)繼續(xù)進(jìn)行下一次的推理.推理可能也對一個(gè)沖突妥協(xié)，則就需要回溯了.

為了強(qiáng)制終止算法，求解器之恩能夠選擇一個(gè)變量x來裂開，如果這個(gè)x-x的寬度超過一定的閾值ε，就可以調(diào)用最小分裂寬度.另外如果它對已經(jīng)存在的邊界僅僅產(chǎn)生了一個(gè)相對較小的過程，求解器還丟棄一個(gè)推理邊界.

這些用來強(qiáng)制終止算法的措施，有一些結(jié)果是非常重要的：

1)如果HySat得到終止unsatisfiable并終止，這個(gè)公式是不符合滿足性的.

2)如果這個(gè)求解器得到“candidate solution box found”并終止，這個(gè)說明對于給定的ε and δ，這個(gè)求解器對于框內(nèi)的結(jié)果不能檢測到任何沖突.它不意味著結(jié)果包含著一個(gè)路徑.你將在這個(gè)界限內(nèi)或附近找到這在大多數(shù)情況下的一個(gè)解決方案

3 結(jié)束語

以上提到的求解器，對于約束求解問題各有優(yōu)點(diǎn)和不足.YICES僅限于解決線性約束求解問題，但其求解比較高效，求解性能良好，而且提供了編程接口，可直接利用java編程使用其接口.HySat可以解決非線性的約束求解問題，但其不提供對外接口，不能嵌入到程序中，其主要作為單獨(dú)工具應(yīng)用于理論驗(yàn)證，規(guī)劃求解等方面.

[1]何炎祥.基于SMT求解器的路徑敏感程序驗(yàn)證[J].軟件學(xué)報(bào),2012,23(10)

[2]李婧.SMT求解器理論組合技術(shù)研究[J].計(jì)算機(jī)工程與科學(xué),2011,33(10)

[3]張永剛.求解約束滿足問題的改進(jìn)蟻群優(yōu)化算法[J].通信學(xué)報(bào),2015,36(5)

[4]金繼偉.SMT求解技術(shù)簡述[J].計(jì)算機(jī)科學(xué)與探索,2015,(7)

[5]羅文杰.CALO研究進(jìn)展分析[J].計(jì)算機(jī)研究與發(fā)展,2006,43(z1)

[6]Christian Herde.Analysis of Hybrid Systems using HySAT[A].Third International Conference on Systems[C].2008

Analysis on the Application of Constraint Solver for Satisfactory Problem

FUJiang-long1,YANGYang1,CHENSu-jun1,ZHAOTian-jiao2

(1.Hebei University of Architecture，Zhangjiakou,075000,China;2.Hebei University of Science and Technology,Shijiazhuang,050000,China)

Constraint solving involves a wide range of problems,and the most important method to solve the problem is SMT theory.This paper introduces two kinds of constraint solvers which are designed by using SMT theory,analyzes the principle and the main application of the constraint solvers,and discusses the advantages and disadvantages of the above two kinds of constraint solvers.The research of the constraint solver provides ideas and methods for solving the corresponding constraint solving problem.

constraint solver;YICES;HySat

2016-12-03

2013年河北省教育廳青年基金項(xiàng)目(QN20131148)；河北省科技計(jì)劃項(xiàng)目(16236004D-8)

付江龍(1988-)，男，碩士，助教.

10.3969/j.issn.1008-4185.2017.02.032

TP 3

A