關於約束型程式設計的畢業論文

概要

模擬器會隨著可能發生的事件增加，而重複檢查更多的條件。那麼，如果可以從進度判斷「這個條件不會再成立」，是否可以安全地停止該檢查呢？我們設計並實現了一種方法，利用值變化的方向作為線索，將不再需要的條件從正在進行的探索中排除，針對混合系統的建模語言 HydLa 進行了實作。

在評價模型中，在不改變模擬結果的情況下，執行時間縮短到約傳統方法的一半。重要的不是將所有計算一律加快，而是利用問題的結構，減少了需要考慮的可能性本身。

在這項研究中學到的限制型程式設計的思維方式，正是目前我的設計哲學的基礎。這種態度不是逐一直接指定結果，而是定義規則、優先順序和界限，並從其範圍內導出成立的解答。

課題——可能性越多，計算就越慢

HydLa是一種用來將連續變化與離散事件相結合的「混合系統」作為數學和邏輯約束來描述的語言。即使不寫出所有程序的順序，也可以通過宣告應該成立的條件來模擬滿足條件的行為。

另一方面，在根據條件才會生效的規則較多的模型中，模擬器會反覆檢查大量候選項。因為已經不再適用、未來也不會成立的條件仍然留在候選中，所以隨著模型的增大，不必要的計算會不斷累積。

題材——連續與離散混合的系統

彈跳的球是混合系統的容易理解的例子。在空中時，位置和速度持續變化，而在接觸地板的瞬間，會發生彈回這種離散的事件。恆溫器、汽車、機器人也不論規模大小，都內含相同的兩種變化。

評估時，使用了讓水平運動的球在被分成多個區塊的面上反彈的模型。每個區塊都有「球如果來到這個範圍就反彈」的條件規則。增加區塊數量雖然可以表達的對象更多，但模擬器需要檢查的條件也會增加。

瓶頸——條件的數量推高計算量

只有在滿足條件時才會生效的規則稱為「帶守護的約束」。在評估模型中，只有當球到達地板且其水平位置位於特定區段內時，該區段的反彈規則才會生效。

將區畫數從10增加到200時，傳統的模擬器大約會隨著區畫數的平方而變慢。對於規模較大的模型，由於物體、接觸區域以及可能發生的事件增加，同樣的問題會變得更大。

調查——處理時間的96%集中在哪裡

測量處理時間時，在區塊數為100的模型中，整體有96%用於FindMinTime。這是從候選項中尋找「下一個發生的最早事件」的處理。因此，所有的守護條件都被反覆評估。

需要改進的地方已經明確。不需要重做整個計算方法，只要安全地減少傳遞給FindMinTime的候選項即可。目標是在不改變模擬結果的前提下，只排除不需要調查的可能性。

方法——安全地解除永遠無法成立的條件

請想像一個沿著階梯彈跳下去的球。如果球越過某一階，並且繼續向前，那麼那一階就無法再影響球。看到圖的人會立即忽略球後面的階。原本的演算法則是一直檢查每一個階。

困難之處在於，證明已被移除的防護之後不會再變得必要的一方。如果只是因為現在是假的就將其移除，那麼當它再次變成真的時候，可能會默默地返回錯誤的結果。因此，提出的方法使用單調性——也就是判斷某個變數在某一時間區間內是否可以保證持續增加或持續減少。

變化的方向沒有改變的情況

第一種對應方法適用於變數在整個模擬過程中單向變動的情況。在將平面分割的模型中，球的水平位置總是增加。一旦越過某個區段，就不會再滿足該區段的條件。由於這種特性可以通過模型檢測技術在模擬之前確認，因此可以在執行過程中安全地移除不再需要的守護條件。

變化的方向在途中改變的情況

現實中的許多系統並不是永遠朝單一方向運行的。變數可能會增加、改變方向，然後減少。因此論文提出了第二種對應方法。首先假設方向，利用斷言來監控這個假設，當方向改變時，從那個時間點重新進行減少的處理。為一個單調區間移除的保護措施，會在下一個區間開始時恢復。

結果——評估模型的執行時間約減半

實現了對均一單調性的應對，並在分割面模型上進行了評估。無論是原始演算法還是提案方法，區域數量增加時所需時間都會增加。然而，提案方法的工作量始終較少。比較擬合的曲線後發現，最高次項的係數從1.1463下降到0.6083，在這個基準測試中，整體模擬所需時間大約減半。

這並不是說所有的 HydLa 模型都會變成兩倍快。所示的是，這種方法有效的地方——擁有許多守護條件的對象，可以證明變化方向，且在執行中守護條件逐漸變得無關的模型。

從這項研究中獲得的視角

在這項研究中所做的不是讓個別的計算一點一點變快。而是利用對系統行為的了解，縮小應該考慮的可能性集合。縮小搜索空間而不改變結果的這種想法，是約束型程式設計的強項。

實現與評估的是，變數持續朝一個方向變動的情況。若變化的方向在途中改變，則僅停留在設計階段，評估則留作今後的課題。還有利用單調性以外的性質，進一步發現不必要的限制的空間。

現在的我，並不是直接設計 AI 的輸出，而是試圖設計 AI 可以探索的條件和邊界，這也是連結到這個經驗的原因。處理複雜結果時，定義什麼不需要考慮，和計算什麼一樣重要。