p_tan's blog

勉強日記です。ツッコミ大歓迎

簡易DPLLアルゴリズムによるSAT Solver

F#

そろそろ関数型言語もやっとかないとね、ということでF#でプログラミングしてみる。

参考文献

SAT Solver

  • ちょっと前に「P=NP証明か？」とか話題になったね。
  • DPLLアルゴリズム
    • DPLLアルゴリズム - Wikipedia
    • 真偽値の確定する論理変数を考慮しつつバックトラック法でしらみ潰しに真偽値の割り当てを探索する

F#で実装

  • 1リテラル規則のみを使用
    • だからまぁ早くはない
  • 論理変数は整数で表現
  • 否定(not)は単項マイナスで表現
  • 節(clause)はint list、論理式はint list list でそれぞれ表現
/// リテラルvに真を割り当てる
let assign (F : int list list) (v:int) =
    F |> List.filter (List.forall ((<>) v))
      |> List.map (List.filter ((<>) -v))

/// 1リテラル規則を適用
let rec apply_unit_rule (F: int list list) =
    match F |> List.tryFind (fun cl -> cl.Length  = 1)  with
    | Some v -> apply_unit_rule (assign F v.Head)
    | None -> F
    
/// DPLL(1リテラル規則のみ)
let rec DPLL (F : int list list) = 
    match apply_unit_rule F with
    | [] -> true
    | newF when List.exists List.isEmpty newF -> false
    | newF ->
        let v = newF.Head.Head
        DPLL (assign newF v) || DPLL (assign newF -v)

// 充足可能な時
let SatFormula = [ [ -1; 2 ];
                   [ 1; -2 ] ]
printfn "%A, %A"  "SatFormula" (DPLL SatFormula)
// 充足不能な時
let UnsatFormula = [ [ 1; 2 ];
                     [ 1; -2 ];
                     [ -1; 2 ];
                     [ -1; -2 ] ]
printfn "%A, %A"  "UnsatFormula" (DPLL UnsatFormula)

↓実行結果

"SatFormula", true
"UnsatFormula", false

こんなに短く書けるF#超楽しい。

SATに関してその他もろもろ