蔡莉莎，曾維鵬，吳恒玉

（海南軟件職業(yè)技術(shù)學(xué)院海南瓊海571400）

?

基于SAT的路徑規(guī)劃系統(tǒng)的設(shè)計(jì)

蔡莉莎，曾維鵬，吳恒玉

（海南軟件職業(yè)技術(shù)學(xué)院海南瓊海571400）

摘要：本文主要介紹了基于SAT路徑規(guī)劃算法以及路徑規(guī)劃系統(tǒng)的設(shè)計(jì)方案。通過移動機(jī)器人抓取積木為例，介紹了基于SAT路徑規(guī)劃算法包括的規(guī)劃問題的命題表示方法以及如何使用SAT求解器對規(guī)劃命題進(jìn)行求解。該系統(tǒng)較傳統(tǒng)的路徑規(guī)劃系統(tǒng)而言，路徑規(guī)劃解提取速度較快，無需傳感器的反復(fù)檢測初始狀態(tài)及目標(biāo)狀態(tài)，規(guī)劃效率較高。

關(guān)鍵詞：可滿足算法；路徑規(guī)劃系統(tǒng)；MjnjSAT求解器；控制器

隨著人工智能技術(shù)的發(fā)展，在很多惡略環(huán)境下，人們使用移動機(jī)器人取代人類完成一些難度高、危險(xiǎn)系數(shù)大的任務(wù)。然而移動機(jī)器人是否能順利完成任務(wù)取決于其是否能順利抵達(dá)目的地，因此移動機(jī)器人自身需要具有路徑規(guī)劃的功能。

傳統(tǒng)的機(jī)器人路徑規(guī)劃方法都是使用單片機(jī)作為核心器件，機(jī)器人上配備的傳感器對周圍環(huán)境的探測，通過實(shí)時(shí)處理傳感器反饋的信息求得機(jī)器人運(yùn)動的路徑點(diǎn)，從而快速尋求一條安全的運(yùn)動軌線判斷并自動躲避障礙物順利抵達(dá)目的地［1］。傳統(tǒng)方法的缺點(diǎn)是在行走的過程中會出現(xiàn)走“彎路”的現(xiàn)象，搜索效率低。

由于SAT求解技術(shù)在知識表達(dá)以及計(jì)算速度等方面具有明顯優(yōu)勢，因此基于SAT的規(guī)劃方法被使用在移動機(jī)器人的路徑規(guī)劃系統(tǒng)上［2］。

1　算法的相關(guān)知識

定義1（可滿足性問題）判定一個(gè)公式是否存在一組變量使其邏輯命題為真，如果存在說明該邏輯命題為可滿足。

定義2（變量，正變量，反變量）對任意一個(gè)變量p，稱變量p為正變量，‘p為反變量，兩者互補(bǔ)。

定義3（合取范式CNF）由不同變量組成的析取項(xiàng)，然后將不同的析取項(xiàng)進(jìn)行合取構(gòu)成合取范式。

2　基于SAT算法的研究

SAT算法的基本思想是將規(guī)劃問題轉(zhuǎn)換成SAT可滿足性問題，將規(guī)劃任務(wù)構(gòu)造長度N=1的編碼成合取范式（Conjunctjve Norma1 Form，CNF）公式，調(diào)用SAT求解器對該規(guī)劃問題進(jìn)行求解，從SAT求解器返回的賦值中提取規(guī)劃解，如果SAT求解器返回值為SAT，則該規(guī)劃解是規(guī)劃任務(wù)的一個(gè)解。如果SAT求解器返回值為USAT，則表示編碼長度N不足，需要進(jìn)一步構(gòu)造N+1的合取范式［3］。

本文以積木世界的移動機(jī)器人路徑規(guī)劃為例如圖1所示介紹基于SAT路徑規(guī)劃算法。S0，Sg，分別表示積木的初始狀態(tài)以及目標(biāo)狀態(tài)。在初始狀態(tài)S0，積木A，B都在桌面上，機(jī)械手此時(shí)為空閑狀態(tài)。

圖1　積木世界的移動機(jī)器人路徑規(guī)劃

為了更好的描述機(jī)器人問題的狀態(tài)描述以及目標(biāo)描述定義以下變量，需要注意的是unstack（A，B）等表示的是變量而不是二目謂詞，使用以下方法定義是為了更好的記憶以及使解的抽取更直觀。

1）用命題公式表示狀態(tài)

①unstack（A，B）：把堆放在積木B上的積木A拾起。在進(jìn)行這個(gè)動作之前，要求機(jī)器人的手為空手，而且積木A的頂上是空的。

②stack（A，B）：把積木A堆放在積木B上。動作之前要求機(jī)械手必須已抓住積木A，而且積木B頂上必須是空的。

③pjckup（A）：從桌面上拾起積木A，并抓住它不放。在動作之前要求機(jī)械手為空手，而且積木A頂上沒有任何東西。

④putdown（A）：把積木A放置到桌面上。要求動作之前機(jī)械手已抓住積木A。

⑤ON（A，B）：積木A在積木B之上。⑥ONTABLE（A）：積木A在桌面上。

⑦CLEAR（A）：積木A頂上沒有任何東西。⑧HOLDING（A）：機(jī)械手正抓住積木A。⑨HANDFREE：機(jī)械手為空手。

積木S0的初始狀態(tài)命題公式表示如下：CLEAR（Ar，S0）∧ONTABLE（Ar，S0）∧CLEAR（B，S0）∧ONTABLE（A，S0）∧HANDFREE（S0）

積木Sg的目標(biāo)狀態(tài)用命題公式表示如下：ON（A，B，Sg）

2）用命題公式表示狀態(tài)轉(zhuǎn)移

要想從初始狀態(tài)變?yōu)槟繕?biāo)狀態(tài)則需要在狀態(tài)S1執(zhí)行一個(gè)stack（A，B）的動作，執(zhí)行完該動作后，積木A在積木B的上面。在本算法中使用兩個(gè)公式表示動作stack（A，B）。在S1中，機(jī)器人抓積木A，積木B在桌面上，積木B上面為空，用命題公式表示為ONTABLE（B，S0）∧CLEAR（B，S1）∧HOLDING（A，S1）。在S2中，機(jī)器人將積木A放到積木B上，積木A上面有空，用命題公式表示為ONTABLE（B，S2）∧CLEAR（A，S2）∧ON（A，B，S2）∧HOLDING（A，S1）。需要注意的是S1，S2分別表示的動作執(zhí)行前及動作執(zhí)行后的兩個(gè)狀態(tài)。為了區(qū)別一個(gè)事實(shí)在某一個(gè)狀態(tài)中成立在另一個(gè)狀態(tài)中不成立這種情況，需要定義不同的變量以示區(qū)別，例如ONTABLE（B，S1），ONTABLE（B，S2），表示的就是兩個(gè)不同的變量，可以指派不同的真值。ONTABLE（B，S1）表示在狀態(tài)積木B在桌面上的事實(shí)成立，而ONTABLE（B，S2）表示在狀態(tài)積木B在桌面上的事實(shí)成立。

因此狀態(tài)從轉(zhuǎn)換成的可以用命題公式如下：ONTABLE（B，S1）∧CLEAR（B，S1）∧HOLDING（A，S1）∧ONTABLE （B，S2）∧CLEAR（A，S2）∧ON（A，B，S2）∧HANDFREE（S2）

3）用命題公式表示規(guī)劃問題

將規(guī)劃任務(wù)構(gòu)造長度N=i的編碼，i表示每一步的狀態(tài)命題和動作命題，初始狀態(tài)用0表示，目標(biāo)狀態(tài)用N表示，因此，j的取值范圍為（0≦i≦N）。對于一個(gè)限定長度的規(guī)劃任務(wù)的編碼由初始狀態(tài)命題公式合取目標(biāo)狀態(tài)命題公式合取從第1步到第N步的動作命題公式。在變量表示中使用步數(shù)值取代狀態(tài)值，例如CLEAR（A，S0）表示為CLEAR（A，0）。

由于本文所舉的例子僅需一步即可完成積木A抓取放到積木B上，因此限定計(jì)劃長度N=1。初始狀態(tài)的編碼為：CLEAR（A，0）∧ONTABLE（A，0）∧CLEAR（B，0）∧ONTABLE（A，0）

目標(biāo)狀態(tài)的編碼為：ON（A，B，1）。

動作狀態(tài)MOVE1，MOVE2編碼分別為：

MOVE（A，Tab1e，B，0）?CLEAR（A，0）∧ON（A，B，1）∧CLEAR（B，0）∧┑ONTABLE（A，Tab1e，1）

MOVE（A，Tab1e，A，0）?CLEAR（A，0）∧ON（B，A，1）∧CLEAR（B，0）∧┑ON（B，Tab1e，1）

4）SAT求解器

判斷一個(gè)命題公式是否可滿足實(shí)際上是一個(gè)NP問題，近幾年來大量學(xué)者在研究SAT求解器的研究與改進(jìn)，使得SAT求解速度不斷提高。因此路徑規(guī)劃領(lǐng)域、電路故障診斷領(lǐng)域也不斷引入SAT求解器對命題公式的求解。將以上所構(gòu)建的命題轉(zhuǎn)換成合取范式的形式輸入SAT求解器中進(jìn)行規(guī)劃解的求解，如果SAT求解器輸出SAT則表明該步規(guī)劃命題存在規(guī)劃解，規(guī)劃成功，如果SAT求解器輸出USAT，則需要增加步數(shù)構(gòu)建N+1的規(guī)劃命題。

3　系統(tǒng)設(shè)計(jì)

本文所設(shè)計(jì)的路徑規(guī)劃系統(tǒng)是基于SAT的路徑規(guī)劃系統(tǒng)，系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)仍然以圖1的積木世界移動機(jī)器人的路徑規(guī)劃為例。路徑規(guī)劃系統(tǒng)包括規(guī)劃器，控制器，機(jī)械手3部分構(gòu)成如圖2所示。

圖2　系統(tǒng)設(shè)計(jì)框圖

將初始狀態(tài)以及目標(biāo)狀態(tài)輸入規(guī)劃器中產(chǎn)生一個(gè)規(guī)劃計(jì)劃，將該規(guī)劃計(jì)劃通過串口通信技術(shù)將數(shù)據(jù)傳輸給基于51單片機(jī)的控制器，由51單片機(jī)的I/O口控制電機(jī)從而控制機(jī)械手執(zhí)行抓取、放下等動作［4］。同時(shí)控制器向規(guī)劃器返回一個(gè)執(zhí)行狀態(tài)以便規(guī)劃器進(jìn)行下一步規(guī)劃。

根據(jù)基于SAT的路徑規(guī)劃系統(tǒng)的設(shè)計(jì)思路，該路徑規(guī)劃系統(tǒng)的規(guī)劃器由編譯器、簡化器、求解器及解碼器構(gòu)成。首先將路徑的規(guī)劃問題轉(zhuǎn)換成SAT問題，把初始狀態(tài)、目標(biāo)動作及規(guī)劃長度輸入編譯器產(chǎn)生一個(gè)命題邏輯公式，然后將命題邏輯公式中的子句、運(yùn)算符號、文字描述等轉(zhuǎn)換成合取范式的形式即CNF。將該CNF公式輸入MjnjSAT求解器中，通過求解器求解判斷該公式是否可滿足，規(guī)劃解是否存在。如果求解器求解的結(jié)果是不可滿足，則編譯器需要通過增加規(guī)劃長度產(chǎn)生新的編碼執(zhí)行以上過程。如果求解器求解的結(jié)果為可滿足，則將求解器輸出的滿足賦值輸入解碼器中，將其翻譯成可被控制器語言執(zhí)行的規(guī)劃解符號［5］。

4　結(jié)束語

目前比較經(jīng)典的路徑規(guī)劃算法包括柵格法，拓?fù)浞?，可視圖法，遺傳算法，圖規(guī)劃算法、SAT可滿足性算法等。早期由于SAT問題一直被人們定性為NP問題，所以極少人將規(guī)劃問題轉(zhuǎn)換成SAT問題。但由于上世紀(jì)90年代，可滿足算法的研究有了重大突破，因此很多研究人員試圖將規(guī)劃問題轉(zhuǎn)換成SAT問題，也取得的了一定的研究成果。而且由于一年一度的求解器大賽的舉行使得SAT求解器求解速率的不斷提高，規(guī)劃解的提取速度原來越快，使得規(guī)劃效率不斷提高。本文主要介紹了基于SAT路徑規(guī)劃算法，以積木抓取為例介紹了如何將規(guī)劃問題轉(zhuǎn)換成SAT問題，通過改變動作狀態(tài)描述方式以及限定規(guī)劃長度解決情景演算存在的異常模型以及情景無限的問題。通過將初始狀態(tài)、目標(biāo)狀態(tài)、動作轉(zhuǎn)變狀態(tài)合取得到CNF。利用MjnjSAT求解器對該CNF進(jìn)行求解規(guī)劃解。控制器通過規(guī)劃器所發(fā)送的規(guī)劃解控制機(jī)械手執(zhí)行相應(yīng)動作包括抓取、放下等。通過實(shí)驗(yàn)表明，該系統(tǒng)規(guī)劃效率較高，邏輯命題推導(dǎo)過程簡單，而且更改規(guī)劃任務(wù)只需更改推理內(nèi)核即可，移植性較強(qiáng)［6］。

參考文獻(xiàn)：

［1］吳忻生，郭丙華，胡躍明.基于傳感器的非完整移動機(jī)器人運(yùn)動規(guī)劃［J］.控制理論與應(yīng)用，2002，19（6）：945-948.

［2］凌應(yīng)標(biāo).基于SAT的規(guī)劃理論與算法研究［D］.廣東：中山大學(xué)，2005.

［3］張雷.基于啟發(fā)式搜索的最優(yōu)規(guī)劃算法研究［D］.南京：南京大學(xué)，2014.

［4］姚佳.智能小車的避障及路徑規(guī)劃［D］.南京：東南大學(xué)，2005.

［5］潘云霞.智能車的尋跡規(guī)劃研究［D］.廣東：中山大學(xué)，2014.

［6］趙相福，歐陽丹彤.使用SAT求解器產(chǎn)生所有極小沖突部件集［J］.電子學(xué)報(bào)，2009，37（4）：804-810.

Deslgn of Path Plannlng system based on SAT

CAI Lj-sha，ZENG Wej-peng，WU Heng-yu
（Hainan Software Profession Institute，Qionghai 571400，China）

Abstract:Thjs paper descrjbes SAT path p1annjng a1gorjthm and the desjgn path p1annjng system. By examp1e of mobj1e robot craw1 B1ocks descrjbes SAT path p1annjng a1gorjthm，jnc1udjng proposjtjon representatjon of p1annjng jssues and how to use the SAT so1ver to so1ve the p1annjng proposjtjons. The system js compared wjth the tradjtjona1 path p1annjng system，extractjon path p1annjng so1utjons faster，effjcjency of p1an more hjgher.

Key words:satjsfjabj1jty a1gorjthm；path p1annjng system；MjnjSAT so1vers；contro11er

中圖分類號：TN02

文獻(xiàn)標(biāo)識碼：A

文章編號：1674-6236（2016）07-0011-02

收稿日期：2015-10-12稿件編號：201510062

基金項(xiàng)目：2015年海南省高等學(xué)?？茖W(xué)研究項(xiàng)目（Hnky2015-76）；2014海南省高等學(xué)?？茖W(xué)研究項(xiàng)目（HNKY2014-98）

作者簡介：蔡莉莎（1984—），女，海南?？谌耍T士，副教授。研究方向：人工智能、嵌入式技術(shù)。