~pmikkelsen/CDCL-apl

4ae19028aaf072e94379378daf5146e05b7a56bc — Peter Mikkelsen 1 year, 25 days ago 2b8c636
shorten :D
1 files changed, 27 insertions(+), 62 deletions(-)

M CDCL.aplf
M CDCL.aplf => CDCL.aplf +27 -62
@@ 1,79 1,44 @@
 r←{print}CDCL(Vars Clauses);Assignments;Choices;ClauseIds;DISPLAY;Extra;ExtraIds;NewAssignments;NewClauseIds;NewClauses;OriginalClauses;Trail;UNSAT;c;l;m;MakeChoice;n;⎕IO
 ⎕IO←0

 :If 0=⎕NC'print'
     print←0
 :EndIf
 :If print=0
     DISPLAY←{}
 :Else
     DISPLAY←{⎕←⍵}
 :End

 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
 Choices←Assignments←0⍴⍨≢Vars
 ClauseIds←⍳≢Clauses
 OriginalClauses←Clauses
 Trail←⍬
 :While 0∊Assignments
     (NewClauses NewClauseIds NewAssignments)←Clauses ClauseIds Assignments

 AllClauses←Clauses
 t←0 4⍴0 ⍝ the trail of information
 :While Vars≠⍥≢t
     :If MakeChoice
         MakeChoice←0
         NewAssignments[n←Assignments⍳0]←1
         Choices[n]←l←l+1
         NewClauses⍪←n=⍳≢Vars
         NewClauseIds,←¯1 ⍝ the id for this kind of choices
         n←⊃(⍳≢Vars)~t[;2]
         l+←1
         Clauses⍪←n=⍳≢Vars
         ClauseIds,←¯1 ⍝ the id for this kind of choices
     :EndIf

     ⍝ Unit propagation
     :While (~∨⌿UNSAT NewClauses)∧(≢NewClauses)>n←1⍳⍨+/|NewClauses
         Trail,←n⌷NewClauseIds            ⍝ Add the clause used to the trail
         n←⍸|c←n⌷NewClauses               ⍝ Pick out the clause and variable
         NewAssignments[n]←c[n]           ⍝ Update the assignments
         m←,NewClauses[;n]×c[n]           ⍝ Make a mask..
         NewClauses[⍸m=¯1;n]←0            ⍝ Simplify clauses
         NewClauses←(~m=1)⌿NewClauses     ⍝ Remove true clauses
         NewClauseIds←(~m=1)⌿NewClauseIds ⍝ Remove true clauses ids

     :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]
     :EndWhile

     :If ∨⌿UNSAT NewClauses
     :If MakeChoice~⍤⊢←∨⌿UNSAT Clauses
         :If l=0
             'Not satisfiable'⎕SIGNAL 11
         :EndIf

         c←OriginalClauses⌷⍨⊃(UNSAT NewClauses)/NewClauseIds
         :While 1<+⌿0=(0≠c)⌿Assignments
             c←×c+(⊃⌽Trail)⌷OriginalClauses
             Trail↓⍨←¯1 ⍝ shorten the trail
         c←AllClauses⌷⍨⊃(UNSAT Clauses)/ClauseIds
         :While 1<+⌿l=(t[;2]∊⍸|c)⌿t[;1]
             c←×c+AllClauses⌷⍨⊃⌽t[;0]
             t↓⍨←¯1 ⍝ shorten the trail
         :EndWhile

         ⍝ Add learned clause to clause list
         OriginalClauses⍪←c

         ⍝ Calculate new level
         Choices+←l×Choices=0 ⍝ all variables are chosen at a level
         l←⊃1↓{⍵[⍒⍵]}(0≠c)⌿Choices

         AllClauses⍪←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

         Trail←(l≥+\Trail=¯1)⌿Trail ⍝ shorten trail
         ((l<Choices)⌿Choices)←0 ⍝ undo choice levels

         ⍝ Update the list of current clauses
         Clauses←×Assignments+⍤1⊢OriginalClauses
         ClauseIds←⍳≢Clauses
         m←Assignments≢⍤1⊢Clauses
         (Clauses ClauseIds)←m∘⌿¨Clauses ClauseIds

     :Else
         (Clauses ClauseIds Assignments)←NewClauses NewClauseIds NewAssignments
         MakeChoice←1
         (Clauses ClauseIds)←{(c≢⍤1⊢⍵)∘⌿¨⍵(⍳≢⍵)}×AllClauses+⍤1⊢c←t[;3]@(t[;2])⊢0⍴⍨≢Vars
     :EndIf
 :EndWhile
 DISPLAY'Result assignments: ',Vars PRETTY Assignments
 r←Assignments
 r←t[⍋t[;2];3]
 DISPLAY'Result assignments: ',Vars PRETTY r