Learning Local Search Heuristics for Boolean Satisfiability
Abstract
GNN (select variable) + local search algorithm.
RL，初始X，GNN結合sofetmax作為policy 函數(shù)，選擇p最大的variable翻轉，每個Trajectory有一個reward（找到使得fai為真的reward為1），訓練參數(shù)。
SAT problem: 屬于[決定性問題]，也是第一個被證明屬于[NP完全]
命題邏輯公式，也稱為布爾表達式，由變量，運算符AND（連接，也用∧表示），OR（分離，∨）， NOT （否定，?）和括號構成。如果通過為其變量分配適當?shù)倪壿嬛担碩RUE，F(xiàn)ALSE）可以使公式為TRUE，則稱該公式是可滿足的.
子句（Clause）就是每個人的愿望清單，eg,x1∨?x2
文字（Literal）就是一個愿望 eg, x1,?x2..
命題變元（Variable）x的真假值
Introduction
we focus on stochastic local search (SLS) and propose a learnable algorithm with a variable selection heuristic computed by a graph neural network。用強化學習訓練一組solver，針對不同類別的啟發(fā)式算法。
Background
boolean formula：n個variable，m個clause（wish list， 由 ∨連接literals的式子），
CNF formula is the conjunction (∧) of all clauses
φ(X) : n個{0/1} ->{0/1}, input為n個bool變量，output是0/1，最后的真假值。
local search: start with a random initial candidate solution - > iteratively re?ne it
Select Variable x,flip (0->1 or 1->0)
Select Variable:
1）walkSAT
randomly selects a clause unsatis?ed by the current assignment 使得最少的previously satis?ed clauses becoming unsatis?e
2）This work:
employs a graph neural network to select a variable. 可以選任意，不一定要在unsatisfied clauses里面選。
with some probability randomly select a variable from a randomly selected unsatis?ed clause.
GNN : maps each node to a vector space, embedding by iteratively updating the representation of the node based on its neighbors.
Model
graphical representation for CNF formulas:
Factor graph（因子圖）：
undirected bipartite graph （二分圖，一邊variable，一邊clause(∨連接)） +
two types of edge: positive (x)and negative(?x) polarities (正負極)
input of the mode:
formula φ + an assignment X
image.png
achitecture of GNN -> policy part of RL
image.png
Training
MDP represented as a tuple (S_D,A,T,R,γ) ,learning a good heuristic is equivalent to ?nding an optimal policy π, max accumulated reward R
訓練policy network中的參數(shù)，ie找到最好的Π使得每次找到合適的action a （意義為：翻轉X_a）
S_D: a set of states (s = (φ,X) ),
A: maps states to available actions A(s) = {1,...,n}
T: SD ×{1,...,n}→SD mapping from a state-action pair to the next state T(s,a) = T((φ,X),a) = (φ,Flip(X,a))
R : SD →{0,1}is the reward function, sR(s) = R((φ,X)) = φ(X), only 1 when the assignment satisfies folmula
γ ∈ (0,1] is the discount factor.
Policy is the function ρθ(φ,X) which returns an action(variable index) a ～ πθ(φ,X)
where πθ is the policy network, learn θ
image.png
Data
A problem distribution D：we sample a formula φ ～ D，generate multiple trajectories for the same formula with several different initial assignments X.
Curriculum Learning： training is performed on a sequence of problems of increasing dif?culty.
the policy learned for easier problems should at least partially generalize to more dif?cult problems,
Experiments
baseline：WalkSAT.
imporve：
model-based algorithms such as Monte Carlo tree search [12] can provide critical improvements. As a step towards practicality, it is also important to incorporate the suite of heuristics in an algorithm portfolio. In this work, we have achieved promising results for learning heuristics, and we hope that this helps pave the way for automated algorithm design.
Words and Phrases
runs for T iterations
makes it viable to 使它可行
a number of avenues for improvement 許多改進方法
omitted for brevity, 為了簡潔起見
implement == achieve, realize, implement
Solid and dashed edges correspond respectively to 實線和虛線分別對應。。。
concretely具體的
opt == select
iteratively re?ne it
迭代地完善它
explicitly == clearly ==demonstratively 明確的
Lately... In a more recent work...
On another front ~~~ on the other hand
from scratch
從頭開始
incorporate A in B
在B中引入A
generic == common;general
Recently there has been a surge of interest in applying machine learning to combinatorial optimization
（a surge of 激增）
manually-designed, requiring signi?cant insight into the problem
insight: 慧眼 manually-designed (手動設計)
abbreviated SAT 縮寫為SAT
is referred to 被稱為
refer to 參考/指
SAT is the canonical NP-complete problem 典型的
a plethora of problems 大量的問題
arising from A 由A產(chǎn)生
algorithms that require fewer, although costlier, steps to arrive at a solution.
更少step，但是更貴
