近期，中國(guó)科學(xué)院軟件研究所研究員蔡少偉團(tuán)隊(duì)在邏輯約束求解器研究中取得多項(xiàng)進(jìn)展，并在命題邏輯可滿足性問(wèn)題（SAT）、可滿足性模理論問(wèn)題（SMT）等多項(xiàng)競(jìng)賽中斬獲佳績(jī)。

　　在邏輯約束求解器領(lǐng)域，SAT和SMT是兩個(gè)最重要的邏輯約束問(wèn)題。SAT是命題邏輯上的約束求解問(wèn)題，SMT是一階謂詞邏輯上的約束求解問(wèn)題。它們不僅在自動(dòng)定理證明、軟件工程等學(xué)術(shù)研究中有廣泛應(yīng)用，還是信息安全、集成電路設(shè)計(jì)自動(dòng)化和軟件驗(yàn)證等領(lǐng)域的底層計(jì)算引擎。

　　近日，SAT會(huì)議公布SAT和MaxSAT比賽結(jié)果，F(xiàn)LoC（Federated Logic Conference，國(guó)際聯(lián)合邏輯大會(huì)）的IJCAR（國(guó)際聯(lián)合自動(dòng)推理會(huì)議）會(huì)議宣布SMT 2022比賽結(jié)果。 

　　在SAT比賽中，蔡少偉團(tuán)隊(duì)以明顯優(yōu)勢(shì)獲得主賽道并行組冠軍和NoLimits賽道冠軍；在MaxSAT比賽中，團(tuán)隊(duì)贏得幾乎大滿貫的成績(jī)，在總共6個(gè)賽道中獲得5個(gè)冠軍和1個(gè)亞軍（其中1個(gè)冠軍與華為理論實(shí)驗(yàn)室、東北師范大學(xué)等團(tuán)隊(duì)合作獲得）。

　　在SMT 2022比賽中，蔡少偉團(tuán)隊(duì)研發(fā)的SMT求解器Z3++（基于國(guó)際主流求解器Z3的衍生求解器）在比賽中獲得線性算術(shù)理論和非線性算術(shù)理論的多項(xiàng)第一，并在Model Validation的所有賽道綜合評(píng)分中求解能力領(lǐng)先。其總分獲得FLoC奧林匹克競(jìng)賽頒發(fā)的2塊金牌（大賽共設(shè)6枚金牌2枚銀牌）。這是國(guó)內(nèi)團(tuán)隊(duì)首次在FLoC奧林匹克競(jìng)賽的SMT比賽中取得金牌。FLoC每四年舉辦一次，在數(shù)理邏輯和計(jì)算機(jī)科學(xué)領(lǐng)域有著重要影響。