~pmikkelsen/CDCL-apl

68178fedba9de5da96ccc0be1e7ade28f15ad510 — Peter Mikkelsen 1 year, 17 days ago 4ae1902
shorten names (i am just trolling now)
1 files changed, 25 insertions(+), 27 deletions(-)

M CDCL.aplf
M CDCL.aplf => CDCL.aplf +25 -27
@@ 1,44 1,42 @@
 r←print CDCL(Vars Clauses);AllClauses;ClauseIds;DISPLAY;Extra;ExtraIds;MakeChoice;NewTrail;UNSAT;c;l;m;n;t;⎕IO
 DISPLAY←{print=1:⎕←⍵}
 UNSAT←((,0)≡∪)⍤1

 (⎕IO l MakeChoice)←0
 ClauseIds←⍳≢Clauses
 AllClauses←Clauses
 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 Vars≠⍥≢t
     :If MakeChoice
         n←⊃(⍳≢Vars)~t[;2]
 :While vs≠⍥≢t
     :If new
         n←⊃(⍳≢vs)~t[;2]
         l+←1
         Clauses⍪←n=⍳≢Vars
         ClauseIds,←¯1 ⍝ the id for this kind of choices
         cs⍪←n=⍳≢vs
         ids,←¯1 ⍝ the id for this kind of choices
     :EndIf

     :While (~∨⌿UNSAT Clauses)∧(≢Clauses)>n←1⍳⍨+/|Clauses
         n←⊃⍸|c←n⌷Clauses                         ⍝ Pick out the clause and variable
         t⍪←(ClauseIds[Clauses⍳c])l n(c[n])       ⍝ Record what we did
         m←,Clauses[;n]×c[n]                      ⍝ Make a mask..
         Clauses[⍸m=¯1;n]←0                       ⍝ Simplify clauses
         Clauses←(~m=1)⌿Clauses                   ⍝ Remove true clauses
         ClauseIds←(~m=1)⌿ClauseIds               ⍝ Remove true clauses ids
         DISPLAY'Level ',(⍕l),', setting: ',Vars[n]PRETTY c[n]
     :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 MakeChoice~⍤⊢←∨⌿UNSAT Clauses
     :If new~⍤⊢←∨⌿us
         :If l=0
             'Not satisfiable'⎕SIGNAL 11
         :EndIf
         c←AllClauses⌷⍨⊃(UNSAT Clauses)/ClauseIds
         c←all⌷⍨⊃us/ids
         :While 1<+⌿l=(t[;2]∊⍸|c)⌿t[;1]
             c←×c+AllClauses⌷⍨⊃⌽t[;0]
             c←×c+all⌷⍨⊃⌽t[;0]
             t↓⍨←¯1 ⍝ shorten the trail
         :EndWhile
         AllClauses⍪←c              ⍝ Add learned clause to clause list
         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
         DISPLAY'Backtrack to level ',(⍕l),' with new clause: ',Vars SHOW c
         (Clauses ClauseIds)←{(c≢⍤1⊢⍵)∘⌿¨⍵(⍳≢⍵)}×AllClauses+⍤1⊢c←t[;3]@(t[;2])⊢0⍴⍨≢Vars
         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]
 DISPLAY'Result assignments: ',Vars PRETTY r
 dbg'Result assignments: ',vs PRETTY r