路徑規劃器的安全保證的製作方法

2024-04-16 14:11:05 2

1.本文所描述的主題總體上涉及諸如飛行器的載具的路徑規劃器。更特別地，本文所描述的主題涉及分析路徑規劃器在避開障礙物方面的充分性。


背景技術：

2.動態感測和避開其它移動實體的問題是當今在多個領域(例如，陸地、海面、海面下、以及空中)中計算機控制的載具的路徑規劃的中心挑戰。路徑規劃指定了載具在空間和時間上的配置，並且這樣的規劃然後可以被轉換成使載具致動的命令並且最終在現實中實現。路徑規劃問題的應用包括計算到目的地的路徑，該路徑避免與已知範圍的靜態和動態障礙物的碰撞，並且相對於時間、距離、或風險是最小的。如果系統動態造成完整約束，那麼這本身就是np完全問題。該問題的避開部分是一般規劃問題的實例。對於當前正在開發的許多自主系統來說，規劃避開的保證和驗證是關鍵的技術挑戰。
3.現有的大量工作涉及獲得控制系統的充分性證明。這種證明通常採取包括工廠模型(plant model)和控制器的連續動態的已知代數和數值表示，並且示出在這種模型的界限(confine)內，系統是穩定的、可控的、以及響應的。在混合系統的研究中，這被擴展成包括混合離散自由度，以表示可能存在於可配置的計算機-物理系統中的包括模式切換的現象。
4.在航空航天領域，聯邦航空管理局的飛機避碰系統(federal aviation administration’s aircraft collision avoidance system)acas-x通過基於場景幾何形狀向飛行員發出以可變速率爬升或下降的建議來解決感測和避開問題。使用自動定理證明器在形式上研究了該系統的驗證。然而，該工作是非常有限的，因為acas-x規劃器是極度受約束的，並且僅能夠有小系列的離散建議中的一個，而更現代的規劃器覆蓋了這些驗證技術不是按比例縮放的呈指數規律大的選擇空間。


技術實現要素：

5.根據各種示例，提出了一種建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的方法。所述方法包括以下步驟：對以下項進行迭代，直到多個預定停止條件中的停止條件出現為止：從路徑規劃器獲得從起始位置到目的地位置的路徑；將從起始位置到目的地位置的路徑表示為邏輯項析取(disjunction of logical terms)；將該項析取合取(conjoining)成表示先前考慮的從起始位置到目的地位置的路徑的項合取(conjunction of terms)；確定項合取的可滿足性條件；以及對於正的可滿足性條件，將所述多個障礙物中的至少一個對應障礙物添加至路徑規劃器；以及基於該停止條件，提供路徑規劃器的充分性指示，以在規劃從起始位置到目的地位置的路徑中避開障礙物。
6.上述示例的各種可選特徵包括如下。該充分性指示可以是正的，並且所述方法還可以包括以下步驟：載具經過由路徑規劃器生成的路徑。載具可以包括飛行器，並且路徑規
劃器可以在飛行器中實現。所述多個預定停止條件可以包括：包括項合取的可滿足性條件在迭代的某一階段為負的停止條件；以及包括路徑規劃器在迭代的某一階段未能提供路徑的停止條件。所述方法還可以包括以下步驟：將起始位置與目的地位置之間的空間分割成多個局部重疊部分；以及將障礙物表示為所述多個局部重疊部分的子集。該空間可以是三維的，並且各個部分皆可以包括多面體(polytope)。所述邏輯項中的各個項皆可以對應於所述多個局部重疊部分中的部分。所述邏輯項中的各個邏輯項皆可以表示若且唯若對應部分包括障礙物時為真的語句。將從起始位置到目的地位置的路徑表示為邏輯項析取的步驟可以包括：向從起始位置到目的地位置的路徑並且向所述多個局部重疊部分應用成員關係算法(membership algorithm)。確定項合取的可滿足性條件的步驟可以包括：應用增量滿足算法。
7.根據各種示例，提出了一種建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的系統。該系統包括：電子處理器；以及包括指令的電子持久性存儲器，該指令在由電子處理器執行時，將該電子處理器配置成執行包括以下項的操作：對以下項進行迭代，直到多個預定停止條件中的停止條件出現為止：從路徑規劃器獲得從起始位置到目的地位置的路徑；將從起始位置到目的地位置的路徑表示為邏輯項析取；將該項析取合取成表示先前考慮的從起始位置到目的地位置的路徑的項合取；確定項合取的可滿足性條件；以及對於正的可滿足性條件，將所述多個障礙物中的至少一個對應障礙物添加至路徑規劃器；以及基於該停止條件，提供路徑規劃器的充分性指示，以在規劃從起始位置到目的地位置的路徑中避開障礙物。
8.上述示例的各種可選特徵包括如下。該充分性指示可以是正的。載具可以包括飛行器，並且路徑規劃器可以在飛行器中實現。所述多個預定停止條件可以包括：包括項合取的可滿足性條件在迭代的某一階段為負的停止條件；以及包括路徑規劃器在迭代的某一階段未能提供路徑的停止條件。所述操作可以包括：將起始位置與目的地位置之間的空間分割成多個局部重疊部分；以及將障礙物表示為所述多個局部重疊部分的子集。該空間可以是三維的，並且各個部分皆可以包括多面體(polytope)。所述邏輯項中的各個項皆可以對應於所述多個局部重疊部分中的部分。所述邏輯項中的各個邏輯項皆可以表示若且唯若對應部分包括障礙物時為真的語句。將從起始位置到目的地位置的路徑表示為邏輯項析取可以包括：向從起始位置到目的地位置的路徑並且向所述多個局部重疊部分應用成員關係算法。確定項合取的可滿足性條件可以包括應用增量滿足算法。
附圖說明
9.根據下面結合附圖對示例的詳細描述，上述和/或其它方面和優點將變得更明顯且更容易理解，其中：
10.圖1是根據各種示例的航空航天領域中的路徑規劃的示意圖；
11.圖2是建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的系統200的示意圖；
12.圖3是建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的方法的流程圖；以及
13.圖4是適合於實現各種示例的示例硬體的示意圖。
具體實施方式
14.現在，將參照附圖更全面描述示例性方面。然而，本公開的示例可以按許多不同的形式具體實施，而不應視為對本文所闡述的示例進行限制。相反地，提供這些示例，以使本公開透徹和完整，並且向本領域技術人員全面表達所述範圍。在圖中，一些細節可以被簡化和/或繪製成便於理解，而不是維持嚴格的結構準確度、細節、和/或比例。
15.一些示例為路徑規劃器提供避障充分性證明，對於該避障充分性證明，希望將路徑規劃器本身視為任意黑箱。與先前在控制下工作或acas-x不同，不需要關於路徑規劃器如何工作的假設，也不存在對其可以生成的路徑支持的任何限制。這允許驗證複雜的路徑規劃技術，這種複雜路徑規劃技術無法轉化成簡明的代數表示，或者對於該複雜路徑規劃技術，該代數表示將是過大的且計算上難以處理的。
16.一些示例基於路徑規劃器能夠生成的可行路徑表達性來作出關於該路徑規劃器的形式聲明。一些示例將路徑集合的充分性表示成布爾可滿足性問題，以避開已知系列障礙物中的固定數量障礙物的任何組合。一旦這已經完成，布爾可滿足性解算器將證明該問題是不可滿足的，在該情況下，該示例提供了路徑規劃器有關其不能因問題類中的任何障礙物集而失敗的足夠表達的保證，或者將證明該問題在與阻擋所有已知路徑的特定障礙物集相對應的特定變量賦值(assignment)的情況下是可滿足的。然後，可以將該障礙物集反饋到路徑規劃器中，該路徑規劃器將宣告它不能夠解決給定的問題實例(路徑規劃器不足以覆蓋問題類的存在性證明)，或者創建新的路徑，該新的路徑可以被添加至該路徑集中，並且被作為布爾可滿足性問題中的附加合取以供下一次迭代。該處理繼續進行，直到出現所述兩個停止條件中的一個為止，這是由於判定空間是有限的且有界的而得以保證發生的。在許多情況下，該組操作的完成遠快於窮盡的時間上界。
17.示例可以具有許多特徵和優點。一些示例將路徑規劃器的充分性的驗證問題編碼為採用合取正規形式的命題邏輯表達式的布爾可滿足性問題，以生成避開數學上精確的幾何併集中的障礙物的路徑。一些示例在對抗角色中利用路徑規劃器和布爾可滿足性解算器，來指導對路徑規劃器充分性的正或負的證明的高效搜索。特別多，一些示例利用用於布爾可滿足性的算法，該算法被修改成增加在重複查詢的背景下的運行時性能，如由路徑規劃器驗證處理在那些重複查詢具有增量結構時作出的，在該增量結構中，各個連續查詢向表達式添加附加的合取子句(clause)。例如，一些示例利用被修改為增量計算形式的布爾可滿足性算法，來避開在具有對抗約束生成器的應用的背景下的返工。根據一些示例，這種經修改的布爾可滿足性算法極大地增強了示例在處理所關注實際問題方面的運行時間性能和可行性。
18.圖1是根據各種示例的航空航天領域中的路徑規劃的示意圖100。如圖所示，飛行器102包括機載路徑規劃器104，該機載路徑規劃器生成在到達目的地110時避開已知障礙物(諸如動態障礙物108)的路徑(諸如路徑106)。可以將示例用於確定路徑規劃器104是否足夠靈活以避開經定義的有限的任意障礙物集中的障礙物，諸如動態障礙物108。示例可以與任何載具一起使用，作為非限制性示例，包括：飛機、輪船、潛艇、汽車、卡車、工廠機器人、無人駕駛飛機、潛水器和陸地載具、以及自主的或者可以由計算機自主或半自主控制的任何其它載具。示例可以與任何類型的路徑規劃器一起使用，並且無需知道路徑規劃器的內部工作方式。即，可以將示例應用於任何「黑箱」路徑規劃器。
19.圖2是建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的系統200的示意圖。例如，可以使用諸如本文參照圖4示出並描述的硬體來實現系統200。
20.系統200包括幾何分割器202。幾何分割器202在障礙物的離散有限基礎上，將描述可能發生的一組物理場景的問題類分解成可計數的併集，該組物理場景涉及多達固定數量的正在遭遇的指定幾何形狀的障礙物。例如，幾何分割器202可以將空間虛擬地分割成許多局部重疊的空間填充多面體部分。作為非限制性示例，該空間通常可以位於載具的起始位置(例如，載具的目前位置)與載具的目的地位置(例如，最終目的地或者被指定為沿著載具的預期路線更遠的某一位置的目的地)之間，或者位於距載具的設定半徑內。在二維中，通過非限制性示例，可以將這些部分實現為正方形、三角形、矩形、或六邊形。在三維中，作為非限制性示例，可以將這樣的部分實現為四面體、立方體、平行六面體、或二十面體。分割的部分可以局部重疊。例如，這些部分可以重疊，以便確保任何任意定位的障礙物總是完全位於至少一個部分內。因此，可以選擇所述部分的重疊的面積(對於二維)或體積(對於三維)，以包圍典型障礙物的外形(對於二維)或整體(對於三維)。根據與問題中的其它約束的交互的相關性，可以在絕對位置或相對位置中指定障礙物。
21.原始問題類可以是按照由幾何分割器202轉換成離散覆蓋的連續語句來指定的。例如，問題類可以指定障礙物的最大數量以及障礙物可以位於其中的體積(在三維中)或面積(在二維中)。一個示例問題類是語句「在遠處的距離d1與d2之間檢測到多達n個飛機，各個飛機皆佔據具有半徑r和高度z的圓柱形體積」。注意，在該示例中，問題類包括針對實數的語句(在遠處的距離d1與d2之間的任何位置)，而幾何分割器202的輸出將是離散的(一些多面體的重疊網格)，使得保證不是分割障礙物的成員的路徑不是原始(連續)問題類中的任何障礙物集的成員。例如，輸出可以使得對於原始(連續)問題類中的每一個障礙物集，存在等數量分割的成員集合，使得被包含在原始(連續)問題的障礙物中的任何點被包含在最終所得(離散)問題的分割成員中的一個分割成員中。這意味著對於任何路徑集合(對於其來說，不存在(恰當數量的)分割成員的單個選擇，使得集合中的每一個路徑與所選擇的分割成員中的至少一個分割成員相交)，在原始連續問題類中無法存在同時與該集合中的各個路徑相交的障礙物集。因此，導致問題的離散版本的不可行性是對原始連續問題的不可行性的充分保證。
22.總而言之，幾何分割器202將起始位置與目的地位置之間的載具操作的連續空間減小到離散空間，其中，可以利用重疊分割中的各種障礙物所處的部分來標識該障礙物。
23.系統200還包括路徑規劃器204。路徑規劃器204可以是任意的路徑規劃器，該路徑規劃器能夠考慮起始位置、目的地位置、以及要避開的障礙物集的特徵化，並且能夠在它們周圍創建至少一個路徑(軌線)，或者宣告該問題在路徑規劃器204的搜索空間和界限內是不可行的。路徑規劃器204可以是基於代數的和/或利用根據各種非限制性示例的移動性曲線圖。路徑規劃器可以包括諸如本文參照圖4示出並描述的硬體或者以該硬體來實現。可以將路徑規劃器204部署在載具上或者可以部署在不同的位置。
24.系統200還包括成員關係解釋器206。成員關係解釋器206接受例如由路徑規劃器204生成的路徑和例如由幾何分割器202生成的分割來作為輸入。成員關係解釋器206輸出分割的、路徑影響到的部分的離散併集。成員關係解釋器206可以利用多種技術中的任一技
術來執行成員關係確定，作為非限制性示例，可以是顯式比較(例如，多面體障礙物的半空間不等性測試)或者其它幾何方法(例如，k-d樹、voronoi圖等)。
25.系統200還包括增量sat解算器208。增量sat解算器208確定在分割中是否存在經受諸如最大數量的障礙物的約束的障礙物集，其將阻擋所有已知路徑(例如，對於所有已知路徑包含成員關係解釋器206的輸出的至少一個成員)。這將幾何碰撞問題簡化成特定命題邏輯公式的代表性布爾可滿足性問題。增量sat解算器208然後使用布爾可滿足性技術(諸如回溯或衝突驅動搜索(例如，davis-putnam-logemann-loveland算法))來確定特定命題邏輯公式是否可滿足。即，增量sat解算器208確定特定命題邏輯公式是否不滿足，或者是否存在滿足該特定命題邏輯公式的與可允許障礙物相對應的命題變量賦值。它的滿意表示路徑被與命題變量賦值相對應的障礙物集所阻擋，而它的不滿意表示路徑規劃器204能夠在這些障礙物周圍進行路線選擇。
26.雖然可以將標準命題邏輯可滿足性算法用於增量sat解算器208，但是一些示例利用對增量查詢特別高效的標準sat解算器的修改。即，在建立路徑規劃器問題的充分性的背景下，其中，重複的sat查詢將利用順序添加的附加路徑來進行，一些示例包括標準sat算法的修改，以支持對命題邏輯公式中的子句集的增量添加，而不需要重建任何可滿足性樹卷展(rollout)。這可以通過注意到以下內容來實現：由於已知不可行或不確定的樹節點(對應於命題邏輯變量賦值)(相應地)保持不可行或不確定，而至多有一個開放節點指定命題邏輯變量賦值集，該命題邏輯變量賦值集滿足可以被直接檢查和處理為在附加子句上進一步迭代的起始點的問題。
27.系統202提供可以被用於執行迭代方法的要素。簡要地，根據各種示例，幾何分割器202定義了在其上進行驗證是可能的空間，然後，路徑規劃器204和增量sat解算器208是迭代中的錨點，其創建附加的子句並證明(或反證)路徑規劃器204的充分性。路徑規劃器204的執行負責擴大增量sat解算器208必須滿足的子句集，而增量sat解算器208的執行負責為路徑規劃器204指定路徑規劃問題，以在由幾何分割器202創建的類內求解。現在參照圖3詳細描述這些和其它動作。
28.圖3是建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的方法300的流程圖。方法300可以由如本文參照圖2示出並且描述的系統200來實現，例如，使用如本文參照圖4示出並描述的硬體400。方法300的動作可以以啟用操作的任何順序來執行。
29.在302，方法300可以開始。方法300可以繼續迭代動作308、310、312、314、以及316，直到在304處出現多個預定停止條件中的一個停止條件為止。下面進一步描述示例停止條件。如果停止條件出現，則控制轉到306。否則，如果停止條件未出現，則控制轉到308。
30.在308，方法300嘗試從路徑規劃器(諸如路徑規劃器204)獲得從起始位置到目的地位置的路徑。路徑規劃器可以接受起始位置、結束位置、以及可能障礙物的描述(例如，問題類)，並且生成從起始位置到結束位置的路徑，該路徑或者避開障礙物或者聲明不可能有路徑。作為非限制性示例，起始位置可以是行程的起始位置，或者可以是行程期間載具的當前位置。目的地位置可以是行程結束的最終位置，或者可以是沿著行程比載具的目前位置更遠的某一點處的位置。在方法300的第一次迭代，作為約束提供給路徑規劃器的障礙物集可以是空的；即，路徑規劃器在第一次迭代中可以不考慮障礙物。第一迭代之後的每次迭代
皆可以向路徑規劃器添加零個或更多個附加障礙物作為約束，如下面參照314和316所描述的。例如，可以將該路徑保存在電子存儲器中和/或存儲在永久存儲器中。如果對於給定的迭代，路徑規劃器無法在障礙物周圍進行路線選擇，則控制轉到304。否則，控制轉到310。
31.在310，方法300將從起始位置到目的地位置的路徑表示為邏輯項析取。根據一些示例，方法300可以首先將幾何分割器(例如，幾何分割器202)應用於通常在起始位置與目的地位置之間的空間，以獲得局部重疊部分的分割。根據這樣的示例，方法300然後可以將成員關係解釋器(例如，成員關係解釋器206)應用於在308處獲得的關於局部重疊部分的分割的路徑。成員關係解釋器輸出該分割中的與路徑相交的部分的標識。作為非限制性示例，標識可以是與分割中的所述部分的用於某一列舉的相應部分相對應的數字的形式。作為非限制性示例，可以有數百、數千、數萬、數十萬、或者數百萬個部分與特定路徑相交。
32.方法300然後將該分割中的與路徑相交的各個部分表示為命題變量，例如，字面值(literal)。如果命題變量為真，則認為對應部分被某一障礙物阻擋；如果命題變量為假，則對應部分被認為是可行進的。作為非限制性的例示性示例，如果從起始位置到目的地位置的路徑與部分x、y以及z相交，則可以將對應的邏輯項析取例如表示為x∨y∨z，其中，部分x對應於命題變量x，部分y對應於命題變量y，以及部分z對應於命題變量z。可以將該命題變量合取「x∨y∨z」解釋為「x或y或z」。如果部分x、y或z中的任一者被阻擋，則對應的命題變量x、y或z被考慮為真。因此，若且唯若x或y或z中的至少一個為真時，析取x∨y∨z為真，這出現在若且唯若部分x、y以及z中的至少一個被阻擋時。
33.在312，方法300將來自310的項析取合取成表示先前考慮的從起始位置到目的地位置的路徑的項析取的合取。例如，對於方法300的第一次迭代，可能不存在先前考慮的路徑，在該情況下，310的動作包括保留來自310的項析取。作為另一示例，對於第一次迭代之後的迭代，可能存在根據先前迭代的來自動作310的先前考慮的路徑，以及對應的項析取，在該情況下，來自目前迭代的析取被合取成表示先前考慮的從起始位置到目的地位置的路徑的項析取的合取。在符號方面，每次迭代i》1可以生成項合取，表示為其中，各個x
i，j
(其中，j為1至ni)皆是表示分割中的、根據方法300的第i次迭代與在308處獲得的路徑相交的部分的命題變量，並且ni表示合取中的項數量(對應於來自相應路徑中的分割的部分數量)。然後，在每次迭代i，將根據該迭代的項析取φi合取至根據先前迭代的析取φ
i-1
，φ
i-2
，...，φ2，φ1，舉例來說，如可以將該項合取存儲在動態或持久性存儲器中。
34.在314，方法300確定項合取ψi的可滿足性條件，例如，「可滿足的」或「不可滿足的」。根據一些示例，方法300可以將布爾解算器(舉例來說，如本文參照圖2示出並描述的增量sat解算器208)應用於項合取ψi。布爾解算器可以接受約束的描述作為輸入，諸如最大障礙物數。然後，布爾解算器確定對項合取ψi中的、與諸如最大障礙物數的約束一致的命題變量集賦值真值(true)是否滿足項合取ψi。
35.例如，利用增量sat解算器，諸如增量sat解算器208，可以通過使用針對ψ
i-1
的過去可滿足性結果(和/或表示命題變量真值賦值的對應的過去可滿足性樹)並且例如使用回溯或衝突驅動搜索(諸如davis-putnam-logemann-loveland算法)確定φi的可滿足性，來實現ψi＝ψ
i-1
∧φi的可滿足性確定。以這種方式，增量sat解算器使用根據過去迭代的結果來加速目前迭代中的可滿足性確定。
36.對於314處的負的可滿足性條件，控制返回到304。
37.對於314處的正的可滿足性條件，控制轉到316。在316，方法300將所述多個障礙物中的至少一個對應障礙物作為約束添加至路徑規劃器。更詳細地，如上參照310所述，若且唯若對合取的命題變量進行true/false的某一賦值滿足該合取時，針對該合取的正的可滿足性結果出現。在這種賦值中被賦值為真值的命題變量對應於分割中的以下部分：這些部分然後在316處作為附加約束被提供給路徑規劃器。然後控制返回到304。
38.在304，方法確定是否出現了多個停止條件中的一個停止條件。根據一些示例，兩個預定停止條件是可能的，其中，第一停止條件指示路徑規劃器足夠靈活以在原始問題類中描述的障礙物周圍進行路線選擇，而第二停止條件指示路徑規劃器不能夠在障礙物周圍進行路線選擇。第一停止條件(其指示路徑規劃器足夠靈活以在障礙物作為進行路線選擇)可以在迭代的某一階段i，當項合取ψi的可滿足性條件為負(即，不可滿足)時出現。第二停止條件(其指示路徑規劃器不能夠圍繞由原始問題描述約束的障礙物進行路線選擇)可以在迭代的某一階段i，當路徑規劃器在308未能提供路徑時出現。
39.例如，在障礙物數有限的情況下，保證出現上述兩個停止條件中的一個停止條件。方法300的迭代可以導致在310處創建與一個新的障礙物配置相對應的至少一個新的項析取，並且例如在障礙物數有限時，存在數量有界的此類選擇。在實踐中，方法300已經顯示出與自然的窮盡界限相比終止得快得多，這是因為路徑規劃器與sat解算器之間的交互的對手性質在日益具有挑戰性的情形下，隨著sat解算器學習避開路徑規劃器可以解決什麼而得到鍛鍊。
40.對於障礙物數是無限的或者其出現的量是無界的問題類，方法300仍可以產生有效結果，但是其可能無法在形式上保證導致如本文所描述的停止條件。在這樣的情況下，例如，根據無界空間的起源，可以將字面值遲鈍地讀出成員關係，因為它們是通過路徑規劃器的執行隱式地找到的，而不是試圖顯式地分配或預聲明字面值。例如，方法300可以在固定的預定次數的迭代之後終止這樣的問題類。
41.在316，方法300基於在304處確定的停止條件，提供路徑規劃器的充分性指示，以在規劃從起始位置到目的地位置的路徑中避開障礙物。例如，對於上述第一停止條件，方法300可以輸出路徑規劃器足以在規劃從起始位置到目的地位置的路徑中避開障礙物的指示。作為另一示例，對於上述第二停止條件，方法300可以輸出路徑規劃器不足以在規劃從起始位置到目的地位置的路徑中避開障礙物的指示。方法300可以多種方式中的任一方式輸出所述指示，諸如在計算機監視器上顯示該指示。
42.圖4是適合於實現各種示例的示例硬體400的示意圖。硬體400包括載具402，該載具可以是任何類型的計算機可控制的載具。載具402使用路徑規劃器410，該路徑規劃器可以位於載具402上或遠離載具402。
43.路徑規劃器410可以被實現為臺式計算機、膝上型計算機中的任一種，可以被併入一個或更多個伺服器、集群、或其它計算機或硬體資源中，或者可以使用基於雲的資源來實現。路徑規劃器410包括易失性存儲器416和持久性存儲器418，其中的持久性存儲器可以存儲計算機可讀指令，該指令在由電子處理器412執行時，配置如本文示出並描述的路徑規劃器410。
44.路徑規劃器410包括網絡接口414，該網絡接口經由網絡430將路徑規劃器410以通信方式聯接至計算機420。網絡430可以包括一個或更多個計算機網絡，並且可以包括網際網路或其部分。根據一些示例，將路徑規劃器410直接聯接至計算機420。根據一些示例，路徑規劃器410和計算機420是在同一計算機上實現的。
45.計算機420包括易失性存儲器426和持久性存儲器428，其中的持久性存儲器可以存儲計算機可讀指令，該指令在由電子處理器422執行時，將計算機420配置成，至少部分地執行本文所公開的方法(舉例來說，如本文參照圖3示出並描述的方法300)。計算機420包括網絡接口424，該網絡接口經由網絡430將計算機420以通信方式聯接至路徑規劃器410。硬體400的其它配置也是可能的。針對所公開的示例的變型例、修改例、以及用例是多種多樣的。
46.例如，可以將一些示例用作多步驟路徑規劃處理的一部分，其中，第一步驟生成一束(bundle)高分集路徑，並且第二步驟從該束中選擇或導出路徑。這可以通過結合使用路徑規劃器和sat解算器來實現，以指導對經受恰當約束的路徑規劃器的表現空間的高效探索。
47.作為另一示例，可以將一些示例用作構建操縱的查找表的部分。特別多，當sat解算器返回結果「不滿意」時，與相應的命題邏輯合取公式隱式地關聯的路徑集合構成足夠的基礎，使得它們中的至少一個可以被用於避開問題類中的任何場景。然後，可以將路徑明確地持久存留至存儲器(例如，硬碟)，並且在載具操作時用作基於查找的策略的部分，例如，用於避免衝突。
48.條款1：一種建立路徑規劃器(104)的充分性以在規劃從起始位置到目的地(110)位置的路徑中避開多個障礙物的方法(300)，所述方法包括以下步驟：對以下項進行迭代，直到多個預定停止條件中的停止條件出現為止：從所述路徑規劃器獲得從所述起始位置到所述目的地位置的路徑；將從所述起始位置到所述目的地位置的所述路徑表示為邏輯項析取；將所述項析取合取成表示先前考慮的從所述起始位置到所述目的地位置的路徑的項合取；確定所述項合取的可滿足性條件；以及對於正的可滿足性條件，將所述多個障礙物中的至少一個對應障礙物添加至所述路徑規劃器；以及基於所述停止條件，提供所述路徑規劃器的充分性指示，以在規劃從所述起始位置到所述目的地位置的路徑中避開所述障礙物。
49.條款2：根據條款1所述的方法，其中，所述充分性指示是正的，所述方法還包括以下步驟：載具經過由所述路徑規劃器生成的路徑。
50.條款3：根據條款2所述的方法，其中，所述載具包括飛行器，並且其中，所述路徑規劃器是在所述飛行器中實現的。
51.條款4：根據條款1至3中的任一條款所述的方法，其中，所述多個預定停止條件包括：包括所述項合取的所述可滿足性條件在所述迭代的某一階段為負的停止條件；以及包括所述路徑規劃器在所述迭代的某一階段未能提供路徑的停止條件。
52.條款5：根據條款1至4中的任一條款所述的方法，所述方法還包括以下步驟：將所述起始位置與所述目的地位置之間的空間分割成多個局部重疊部分；以及將所述障礙物表示為所述多個局部重疊部分的子集。
53.條款6：根據條款5所述的方法，其中，所述空間是三維的，並且其中，各個部分皆包括多面體。
54.條款7：根據條款5或6所述的方法，其中，所述邏輯項中的各個項皆對應於所述多個局部重疊部分中的部分。
55.條款8：根據條款7所述的方法，其中，所述邏輯項中的各個邏輯項皆表示若且唯若對應部分包括障礙物時為真的語句。
56.條款9：根據條款5至8中的任一條款所述的方法，其中，將從所述起始位置到所述目的地位置的所述路徑表示為所述邏輯項析取的步驟包括：向從所述起始位置到所述目的地位置的所述路徑並且向所述多個局部重疊部分應用成員關係算法。
57.條款10：根據條款1至9中的任一條款所述的方法，其中，確定所述項合取的可滿足性條件的步驟包括：應用增量滿足算法。
58.條款11：一種用於建立路徑規劃器的充分性以在規劃從起始位置到目的地位置的路徑中避開多個障礙物的系統，所述系統包括：電子處理器；以及包括指令的電子持久性存儲器，所述指令在由所述電子處理器執行時，將所述電子處理器配置成執行包括以下項的操作：對以下項進行迭代，直到多個預定停止條件中的停止條件出現為止：從所述路徑規劃器獲得從所述起始位置到所述目的地位置的路徑；將從所述起始位置到所述目的地位置的所述路徑表示為邏輯項析取；將所述項析取合取成表示先前考慮的從所述起始位置到所述目的地位置的路徑的項合取；確定所述項合取的可滿足性條件；以及對於正的可滿足性條件，將所述多個障礙物中的至少一個對應障礙物添加至所述路徑規劃器；以及基於所述停止條件，提供所述路徑規劃器的充分性指示，以在規劃從所述起始位置到所述目的地位置的路徑中避開所述障礙物。
59.條款12：根據條款11所述的系統，其中，所述充分性指示是正的。
60.條款13：根據條款11所述的系統，其中，所述載具包括飛行器，並且其中，所述路徑規劃器是在所述飛行器中實現的。
61.條款14：根據條款11至13中的任一條款所述的系統，其中，所述多個預定停止條件包括：包括所述項合取的所述可滿足性條件在所述迭代的某一階段為負的停止條件；以及包括所述路徑規劃器在所述迭代的某一階段未能提供路徑的停止條件。
62.條款15：根據條款11至14中的任一條款所述的系統，其中，所述操作還包括：將所述起始位置與所述目的地位置之間的空間分割成多個局部重疊部分；以及將所述障礙物表示為所述多個局部重疊部分的子集。
63.條款16：根據條款15所述的系統，其中，所述空間是三維的，並且其中，各個部分皆包括多面體。
64.條款17：根據條款15或16所述的系統，其中，所述邏輯項中的各個項皆對應於所述多個局部重疊部分中的部分。
65.條款18：根據條款17所述的系統，其中，所述邏輯項中的各個邏輯項皆表示若且唯若對應部分包括障礙物時為真的語句。
66.條款19：根據條款15至18中的任一條款所述的系統，其中，將從所述起始位置到所述目的地位置的所述路徑表示為所述邏輯項析取的步驟包括：向從所述起始位置到所述目的地位置的所述路徑並且向所述多個局部重疊部分應用成員關係算法。
67.條款20.根據條款11至19中的任一條款所述的系統，其中，確定所述項合取的可滿足性條件的步驟包括：應用增量滿足算法。
68.雖然出於清楚和理解的目的，已經通過例示和示例的方式相當詳細地描述了前述公開內容，但是通過閱讀本公開，本領域普通技術人員將清楚，在不脫離本公開的真實範圍的情況下，可以進行形式和細節上的各種改變，並且可以在所附權利要求的範圍內加以實踐。例如，所有方法、系統、和/或組成部分或其其它方面可以各種組合來加以使用。本文所引用的所有專利、專利申請、網站、其它出版物或文獻等出於所有目的通過引用它們的全部內容而併入，其程度如同將各個單獨項明確且單獨地指示為通過引用而併入的那樣。