基于SAT的路徑規劃系統的設計

蔡莉莎，曾維鵬，吳恒玉

（海南軟件職業技術學院海南瓊海571400）

?

基于SAT的路徑規劃系統的設計

蔡莉莎，曾維鵬，吳恒玉

（海南軟件職業技術學院海南瓊海571400）

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

關鍵詞：可滿足算法；路徑規劃系統；MjnjSAT求解器；控制器

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

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

由于SAT求解技術在知識表達以及計算速度等方面具有明顯優勢，因此基于SAT的規劃方法被使用在移動機器人的路徑規劃系統上［2］。

1　算法的相關知識

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

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

定義3（合取范式CNF）由不同變量組成的析取項，然后將不同的析取項進行合取構成合取范式。

2　基于SAT算法的研究

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

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

圖1　積木世界的移動機器人路徑規劃

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

1）用命題公式表示狀態

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

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

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

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

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

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

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

積木Sg的目標狀態用命題公式表示如下：ON（A，B，Sg）

2）用命題公式表示狀態轉移

要想從初始狀態變為目標狀態則需要在狀態S1執行一個stack（A，B）的動作，執行完該動作后，積木A在積木B的上面。在本算法中使用兩個公式表示動作stack（A，B）。在S1中，機器人抓積木A，積木B在桌面上，積木B上面為空，用命題公式表示為ONTABLE（B，S0）∧CLEAR（B，S1）∧HOLDING（A，S1）。在S2中，機器人將積木A放到積木B上，積木A上面有空，用命題公式表示為ONTABLE（B，S2）∧CLEAR（A，S2）∧ON（A，B，S2）∧HOLDING（A，S1）。需要注意的是S1，S2分別表示的動作執行前及動作執行后的兩個狀態。為了區別一個事實在某一個狀態中成立在另一個狀態中不成立這種情況，需要定義不同的變量以示區別，例如ONTABLE（B，S1），ONTABLE（B，S2），表示的就是兩個不同的變量，可以指派不同的真值。ONTABLE（B，S1）表示在狀態積木B在桌面上的事實成立，而ONTABLE（B，S2）表示在狀態積木B在桌面上的事實成立。

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

3）用命題公式表示規劃問題

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

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

目標狀態的編碼為：ON（A，B，1）。

動作狀態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求解器

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

3　系統設計

本文所設計的路徑規劃系統是基于SAT的路徑規劃系統，系統的設計與實現仍然以圖1的積木世界移動機器人的路徑規劃為例。路徑規劃系統包括規劃器，控制器，機械手3部分構成如圖2所示。

圖2　系統設計框圖

將初始狀態以及目標狀態輸入規劃器中產生一個規劃計劃，將該規劃計劃通過串口通信技術將數據傳輸給基于51單片機的控制器，由51單片機的I/O口控制電機從而控制機械手執行抓取、放下等動作［4］。同時控制器向規劃器返回一個執行狀態以便規劃器進行下一步規劃。

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

4　結束語

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

參考文獻：

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

［2］凌應標.基于SAT的規劃理論與算法研究［D］.廣東：中山大學，2005.

［3］張雷.基于啟發式搜索的最優規劃算法研究［D］.南京：南京大學，2014.

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

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

［6］趙相福，歐陽丹彤.使用SAT求解器產生所有極小沖突部件集［J］.電子學報，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

文獻標識碼：A

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

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

基金項目：2015年海南省高等學校科學研究項目（Hnky2015-76）；2014海南省高等學校科學研究項目（HNKY2014-98）

作者簡介：蔡莉莎（1984—），女，海南海口人，碩士，副教授。研究方向：人工智能、嵌入式技術。