關於約束程式設計的學士論文

概述

身為資訊科學系的大學部學生，我的研究從一個很實際的問題出發：當模擬器累積了大量可能的條件時，要怎麼讓它不再反覆考慮那些已經不可能發生的條件？我為 HydLa 設計並實作了一種方法，利用變數正在變化的方向，把已經失效的條件從搜尋中移除，並加以評估。在作為基準的模型上，模擬的總耗時減少到大約一半。

這項研究是我的設計哲學最早的地基。約束程式設計讓我明白，複雜的結果並不總是需要被直接指定：它們可以從一個經過仔細定義的規則、優先順序與邊界所構成的空間裡生長出來。這樣的思考方式如今支撐著我在 AI 時代從約束出發的設計方式——去設計一個生成系統可以自由行動的條件。

摘要

HydLa 是一種針對混成系統的建模語言；所謂混成系統，是連續變化與離散事件相互作用的系統。基於約束的設計讓這類系統能被簡潔地描述，並以很高的精度加以模擬。代價是：模型一旦變大，模擬器就會持續檢查數量龐大的條件規則，即使其中有些早已無關。

本研究提出在執行過程中動態削減這些守衛約束。只要能辨識出單調的行為——某個值持續朝一個方向變化——模擬器就能判定某些守衛條件在未來永遠不會成立，從而安全地停止檢查它們。在含有大量同類守衛物件的模型中，這個方法尤其有效：實測執行時間降到原本的大約一半。

1. 前言

混成系統同時具備連續的行為與離散的事件。彈跳的小球就是一個簡單的例子：它在空中時，位置與速度連續變化，而撞上平面的那一瞬間構成一個離散事件，改變了它的方向。恆溫器、汽車與機器人，內部都藏著同一種混合，只是後果更為重大。

HydLa 讓建模者以數學與邏輯的約束來描述這類系統，而不必寫出一條唯一的程序序列。它的模擬器 HyLaGI 能進行沒有捨入誤差的符號計算，也能處理取值不確定的參數。然而這樣的表達力帶來了規模上的問題：當一個模型含有許多只在特定條件下才生效的規則時，模擬器必須一再追問，每個條件是否就是下一個將要發生的那個。

2. 模擬中的守衛約束

守衛約束是只在其守衛條件被滿足時才生效的規則。在上面的基準模型裡，每個平面區段都有自己的規則：如果小球的高度降到零，而它的水平位置正落在該區段之內，彈跳規則就適用。因此，平面切得越細，模擬器要檢查的守衛條件也就越多。

實驗把區段數從 10 變化到 200。原有的模擬器變慢的幅度，大致與這個數目的平方成正比。這件事的意義不止於一個玩具範例：更大的模型很可能正是以這種帶守衛的形式，表示大量物體、接觸區域或可能發生的事件。

3. 瓶頸所在

效能剖析顯示，這樣的變慢並沒有平均分布在模擬器各處。當平面被分成 100 個區段時，實測執行時間的 96% 都花在 FindMinTime 上——那是尋找下一個最早可能事件的運算。它在反覆求值每一個候選約束的守衛條件。

這個結果讓最佳化的目標變得具體：在完全不改變被模擬行為的前提下，減少 FindMinTime 必須考慮的守衛條件數量。

4. 守衛約束的削減

設想一個小球沿著階梯逐階彈跳而下。一旦小球越過某一階並繼續向前，那一階就再也影響不到它了。看圖的人會立刻忽略小球身後的階梯；而原有的演算法仍在逐一檢查它們。

困難之處在於證明被丟掉的守衛條件在之後永遠不會再被用到。僅僅因為它此刻為假就移除它，萬一它重新變為真，就可能無聲無息地給出錯誤結果。因此提案使用單調性：判斷某個變數在一段時間區間內，是否保證持續增大或持續減小。

4.1 一致單調性的處理方式

第一種處理方式適用於變數在整個模擬過程中只朝一個方向移動的情形。在分段平面的模型裡，小球的水平位置始終增大。一旦它越過某個區段，該區段的條件就再也不可能被滿足。這個性質可以在模擬之前以模型檢驗的技術加以確立，於是隨著執行的推進，失效的守衛條件可以被安全地移除。

4.2 交替單調性的處理方式

現實中的許多系統並不會永遠朝一個方向變化。一個變數可能先增大，然後轉向，接著減小。因此論文勾勒了第二種處理方式：先假定一個方向，以斷言監視這個假定，並從方向改變的那一點起重新開始削減的邏輯。為某個單調區間移除的守衛條件，會在下一個區間開始時被復原。

5. 實驗結果

我實作了一致單調性這條路線，並以分段平面的模型加以評估。隨著區段數增加，原有演算法與提案演算法的耗時都還是會變長，但提案版本始終做了更少的工作。比較擬合出的曲線，最高次項係數從 1.1463 降到 0.6083；對這個基準而言，模擬的總耗時大約減半。

這並不是說任何 HydLa 模型都會快上一倍。它說明的是這個方法在哪裡有用：含有大量守衛物件、變化方向可被證明，並且守衛條件會在執行過程中永久失效的模型。

6. 結論與未來工作

這項研究表明，讓模擬更有效率的途徑不只是把低階運算做得更快，關於模型本身的知識同樣可以做到。藉由單調性辨識出哪些可能性已經變得不可能，HyLaGI 就能在不改變結果的前提下縮小其有效約束集合。

實際實作並驗證的是一致單調性這一側。論文為後續工作留下了兩個方向：評估針對交替行為的斷言方法，以及利用單調性之外的不變性質，找出更多可以被安全移除的約束。