~pmikkelsen/CDCL-apl

acdfb49f88c2e5f66673b5e73986d0d9b44b12ba — Peter Mikkelsen 1 year, 20 days ago 68178fe master
haha!
1 files changed, 18 insertions(+), 42 deletions(-)

M CDCL.aplf
M CDCL.aplf => CDCL.aplf +18 -42
@@ 1,42 1,18 @@
 r←print CDCL(vs cs);all;c;dbg;ids;l;m;n;new;t;us;⎕IO
 dbg←{print=1:⎕←⍵}
 (⎕IO l new)←0
 ids←⍳≢cs
 all←cs
 t←0 4⍴0 ⍝ the trail of information
 :While vs≠⍥≢t
     :If new
         n←⊃(⍳≢vs)~t[;2]
         l+←1
         cs⍪←n=⍳≢vs
         ids,←¯1 ⍝ the id for this kind of choices
     :EndIf

     :While (~∨⌿us←((,0)≡∪)⍤1⊢cs)∧(≢cs)>n←1⍳⍨+/|cs
         n←⊃⍸|c←n⌷cs                        ⍝ Pick out the clause and variable
         t⍪←(ids[cs⍳c])l n(c[n])       ⍝ Record what we did
         m←,cs[;n]×c[n]                      ⍝ Make a mask..
         cs[⍸m=¯1;n]←0                       ⍝ Simplify clauses
         cs←(~m=1)⌿cs                   ⍝ Remove true clauses
         ids←(~m=1)⌿ids               ⍝ Remove true clauses ids
         dbg'Level ',(⍕l),', setting: ',vs[n]PRETTY c[n]
     :EndWhile

     :If new~⍤⊢←∨⌿us
         :If l=0
             'Not satisfiable'⎕SIGNAL 11
         :EndIf
         c←all⌷⍨⊃us/ids
         :While 1<+⌿l=(t[;2]∊⍸|c)⌿t[;1]
             c←×c+all⌷⍨⊃⌽t[;0]
             t↓⍨←¯1 ⍝ shorten the trail
         :EndWhile
         all⍪←c              ⍝ Add learned clause to clause list
         l←⊃1↓{⍵[⍒⍵]}t[t[;2]⍳⍸|c;1] ⍝ Calculate new level
         t←(l≥t[;1])⌿t              ⍝ shorten trail
         dbg'Backtrack to level ',(⍕l),' with new clause: ',vs SHOW c
         (cs ids)←{(c≢⍤1⊢⍵)∘⌿¨⍵(⍳≢⍵)}×all+⍤1⊢c←t[;3]@(t[;2])⊢0⍴⍨≢vs
     :EndIf
 :EndWhile
 r←t[⍋t[;2];3]
 dbg'Result assignments: ',vs PRETTY r
CDCL←{
     (⎕IO CNT)←0,≢⍉⍵
     CHOOSE←{((l+1)(c⍪<⍀0@(t[;2])⊢CNT⍴1)(i,¯1)@1 4 5)⍣n⊢(t l n a c i)←⍵}
     LEARN←{
         ~∨⌿⊃⌽(t l n a c i u)←⍵:¯1↓⍵
         l=0:'Not satisfiable'⎕SIGNAL 11
         a⍪←x←{×⍵+a⌷⍨⊃⌽((t↓⍨←¯1)⊢t)[;0]}⍣{1=+⌿l=(t[;2]∊⍸|⍺)⌿t[;1]}a⌷⍨⊃u/i
         t⌿⍨←t[;1]≤l←⊃1↓{⍵[⍒⍵]}t[t[;2]⍳⍸|x;1]
         t l 0 a,{(x≢⍤1⊢⍵)∘⌿¨⍵(⍳≢⍵)}×a+⍤1⊢x←t[;3]@(t[;2])⊢CNT⍴0
     }
     UNITPROP←{
         (t l n a c i)←⍵
         ~(~∨⌿u←((,0)≡∪)⍤1⊢c)∧(≢c)>z←1⍳⍨+/|c:⍵,⊂u
         t⍪←(z⌷i)l x(y⌷⍨x←⊃⍸|y←z⌷c)
         ∇ t l 0 a,⌽(~m=1)∘⌿¨i c⊣c[⍸¯1=m←,c[;x]×y[x];x]←0
     }
     {⍵[⍋⍵[;2];3]}⊃(1@2)⍤CHOOSE⍤LEARN⍤UNITPROP⍣{CNT=≢⊃⍺}(0 4⍴0)0 1 ⍵ ⍵(⍳≢⍵)
 }