軟件所博士生提出一種圖神經網絡模型實現 MaxSAT問題求解優化
文章來源: | 發布時間:2023-03-13 | 【打印】 【關閉】
軟件所計算機科學國家重點實驗室的博士生劉明昊,針對人工智能和理論計算機科學中的基礎問題之一——最大可滿足性問題(MaxSAT),提出了一種基于圖神經網絡的深度學習系統,在求解大規模的困難MaxSAT實例時可以快速獲得更高質量的解。該研究成果以“Can Graph Neural Networks Learn to Solve the MaxSAT Problem?”為題發表在人工智能領域國際頂級會議AAAI 2023的學生摘要軌道,并榮獲大會最佳學生摘要提名獎(Honorable Mention)。
最大可滿足性問題即給定一個命題邏輯公式,要求找到滿足最多數量布爾約束的解。該問題在理論計算機科學、知識推理、電子設計自動化和組合優化等領域都有著重要的應用。傳統的MaxSAT求解算法主要基于人工設計的高效啟發式搜索策略,難以有效遷移到不同分布的問題實例上。該研究創新性地提出了一種圖神經網絡模型,能夠從小規模的簡單實例中學習出有效的解生成策略,并成功泛化到同分布的較大規模實例上。實驗結果表明,該模型在兩種不同分布的實例集上均能夠學習至收斂,在包含1600個變量的困難測試實例上相較于最先進的傳統算法可以產生更優的解,且求解階段用時顯著低于傳統算法。該研究揭示了將深度學習與符號推理兩類人工智能方法進行更深入結合的巨大價值。
論文主要內容
獲獎證書