判定過程：SAT與SMT求解算法（第2版）

Daniel Kroening是牛津大學計算機科學系的教授，他的興趣包括自動驗證、軟件工程和編程語言。

Ofer Strichman是以色列理工學院工業工程與管理學院的教授，他的研究興趣包括軟件和硬件的形式化驗證，以及一階邏輯片段的決策程序。

目錄

第1版序

第2版序

前言

第1章簡介和基本概念1

11形式推理的兩種方法2

111基於推演的證明3

112基於枚舉的證明4

113推演與枚舉5

12基本定義5

13範式及其屬性7

14理論視角14

141我們求解的問題17

142如何介紹理論18

15表達能力vs可判定性18

16邏輯公式的布爾結構20

17邏輯作為建模語言21

18習題23

19詞匯表24

第2章命題邏輯的判定過程25

21命題邏輯25

22SAT求解器27

221SAT求解的歷史27

222CDCL框架29

223布爾約束傳播和蘊含圖30

224學習子句與歸結法36

225決策啟發式39

226歸結圖和不可滿足核42

227增量式可滿足性問題43

228從SAT到CSP44

229SAT求解器：總結46

23習題47

231預熱練習47

232命題邏輯48

233建模48

234復雜度49

235CDCLSAT求解50

236相關問題51

24文獻註釋51

25詞匯表55

第3章從命題邏輯到無量詞理論56

31引言56

32DPLL(T)概述58

33形式化表達60

34理論傳播和DPLL(T)框架64

341理論傳播蘊含64

342性能，性……66

343返回蘊含賦值而非子句67

344生成強引理68

345即刻傳播68

35習題69

36文獻註釋70

37詞匯表72

第4章帶未解釋函數的等式邏輯73

41引言73

411復雜度和表達能力73412布爾變量74

413消除常數：一個化簡技術74

42未解釋函數74

421未解釋函數的使用75

422一個例子：證明程序的等價性76

43通過等價閉包判定等式和未解釋函數的合取公式80

44函數一致性不足以完成證明82

45未解釋函數的兩個應用例子84

451證明電路的等價性84

452通過翻譯驗證來驗證編譯過程86

46習題87

47文獻註釋89

48詞匯表90

第5章線性算術91

51引言91

52單純形法93

521範式93

522單純形法基礎94

523帶上下界的單純形法96

524增量式問題99

53分支限界方法100

54Fourier–Motzkin消元106

541等式約束106

542變量消除106

543復雜度109

55Omega測試109

551問題描述109

552等式約束110

553不等式約束113

56預處理118

561線性系統的預處理118

562整數線性系統的預處理119

57差分邏輯120

571引言120

572一個差分邏輯判定過程122

58習題123

581熱身練習123

582單純形法123

583整數線性系統124

584Omega測試124

585差分邏輯125

59文獻註釋126

510詞匯表127

第6章位向量128

61位向量算術128

611語法128

612符號130

613語義131

62位向量算術的平展判定方法136

621轉換骨架136

622算術運算137

63增量位平展140

631有些運算是難的140

632基於未解釋函數進行抽象142

64定點算術142

641語義142

642平展144

65習題145

651語義145

652位向量算術的位級別變量145

653使用線性算術求解器146

66文獻註釋148

67詞匯表149

第7章數組151

71引言151

711語法152

712語義153

72消除數組項154

73數組理論片段的歸約算法155

731數組屬性155

732歸約算法157

74惰性編碼過程159

741基於DPLL(T)的增量編碼159

742讀覆寫公理的惰性實例化159

743外延規則的惰性實例化162

75習題164

76文獻註釋165

77詞匯表166

第8章指針邏輯167

81引言167

811指針及其應用167

812動態內存分配169

813帶指針程序分析169

82一個簡單的指針邏輯171

821語法171

822語義173

823內存模型的公理化174

824增加結構類型175

83堆分配的數據結構建模176

831鏈表176

832樹178

84一個判定過程180

841應用語義轉換180

842純變量182

843內存劃分183

85基於規則的判定過程185

851鏈接型數據結構的可達性謂詞185

852判定可達性謂詞公式187

86習題190

861指針公式190

862可達性謂詞191

87文獻註釋192

88詞匯表194

第9章量化公式196

91引言196

911例子：量化布爾公式198

912例子：量化析取線性算術199

92量詞消去200

921前束範式200

922量詞消去算法202

923量化布爾公式的量詞消去203

924量化析取線性算術的量詞消去206

93基於搜索的QBF算法207

94有效命題化邏輯210

95一般量化212

96習題219

961熱身練習219

962QBF220

963EPR222

964一般量化222

97文獻註釋222

98詞匯表224

第10章判定理論組合公式225

101引言225

102預備知識225

103Nelson–Oppen過程227

1031凸理論的組合227

1032非凸理論的組合231

1033Nelson–Oppen過程的正確性證明233

104習題237

105文獻註釋238

106詞匯表240

第11章命題邏輯編碼241

111惰性編碼vs積極編碼241

112從未解釋函數到等式邏輯241

1121Ackermann歸約242

1122Bryant歸約245

113等式圖249

114化簡公式252

115基於圖的命題邏輯歸約255

116等式和小值域實例化258

1161一些簡單的界259

1162基於圖的域分配261

1163域分配算法262

1164可靠性證明265

1165總結268

117Ackermann歸約vsBryant歸約268

118習題270

1181歸約271

1182域分配272

119文獻註釋273

1110詞匯表275

第12章判定過程在軟件工程和計算生物上的應用277

121引言277

122有界程序分析279

1221檢查單一路徑的可行性279

1222檢查有界程序中所有路徑的可行性283

123無界程序分析285

1231使用非確定賦值的過近似285

1232過估計可能太粗糙287

1233循環不變式290

1234利用循環不變式對抽象進行細化292

124SMT方法在生物學中的應用294

1241DNA計算294

1242基因調控網絡296

125習題298

1251熱身練習298

1252有界符號模擬298

1253程序的過近似300

126文獻註釋301

ASMT-LIB：簡介304

A1SMT庫與標準304

A2SMT-LIB文件接口305

A21命題邏輯306

A22算術307

A23位向量算術308

A24數組309

A25等式理論和未解釋函數309

B判定過程的C++庫311

B1簡介311

B2圖和樹312

B3解析314

B31一階邏輯語法314

B32問題的文件格式316

B33存儲標識符的類317

B34解析樹317

B4CNF和SAT319

B41產生CNF319

B42解析命題骨架320

B5一個惰性判定過程模板321

參考文獻323