~pmikkelsen/CDCL-apl

2b8c6361e1ea5120126c40340a01f8f63c0a7b90 — Peter Mikkelsen 1 year, 1 month ago 65bcb08
get rid of the store
1 files changed, 10 insertions(+), 18 deletions(-)

M CDCL.aplf
M CDCL.aplf => CDCL.aplf +10 -18
@@ 1,4 1,4 @@
 r←{print}CDCL(Vars Clauses);Assignments;Choices;ClauseIds;DISPLAY;Extra;ExtraIds;NewAssignments;NewClauseIds;NewClauses;OriginalClauses;Store;Trail;UNSAT;c;l;m;MakeChoice;n;⎕IO
 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'


@@ 16,7 16,7 @@
 Choices←Assignments←0⍴⍨≢Vars
 ClauseIds←⍳≢Clauses
 OriginalClauses←Clauses
 Store←Trail←⍬
 Trail←⍬
 :While 0∊Assignments
     (NewClauses NewClauseIds NewAssignments)←Clauses ClauseIds Assignments



@@ 38,11 38,9 @@
         NewClauses←(~m=1)⌿NewClauses     ⍝ Remove true clauses
         NewClauseIds←(~m=1)⌿NewClauseIds ⍝ Remove true clauses ids

         DISPLAY 'Level ',(⍕l),', setting: ',Vars[n]PRETTY c[n]
         DISPLAY'Level ',(⍕l),', setting: ',Vars[n]PRETTY c[n]
     :EndWhile

     Store,←⊂NewClauses NewClauseIds

     :If ∨⌿UNSAT NewClauses
         :If l=0
             'Not satisfiable'⎕SIGNAL 11


@@ 61,27 59,21 @@
         Choices+←l×Choices=0 ⍝ all variables are chosen at a level
         l←⊃1↓{⍵[⍒⍵]}(0≠c)⌿Choices

         DISPLAY 'Backtrack to level ',(⍕l),' with new clause: ',Vars SHOW c
         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
         (Clauses ClauseIds)←l⊃Store ⍝ re-store the clauses
         Store←(1+l)↑Store ⍝ drop newer stores

         ⍝ Add the learned clause(s)
         m←~ClauseIds∊⍨⍳≢OriginalClauses
         c←×Assignments+⍤1⊢m⌿OriginalClauses
         n←⍸m
         m←Assignments≢⍤1⊢c
         Clauses⍪←m⌿c
         ClauseIds,←m⌿n
         ⍝ Update the list of current clauses
         Clauses←×Assignments+⍤1⊢OriginalClauses
         ClauseIds←⍳≢Clauses
         m←Assignments≢⍤1⊢Clauses
         (Clauses ClauseIds)←m∘⌿¨Clauses ClauseIds

         ⍝ Update store at the current level
         Store[l]←⊂Clauses ClauseIds
     :Else
         (Clauses ClauseIds Assignments)←NewClauses NewClauseIds NewAssignments
         MakeChoice←1
     :EndIf
 :EndWhile
 DISPLAY 'Result assignments: ',Vars PRETTY Assignments
 DISPLAY'Result assignments: ',Vars PRETTY Assignments
 r←Assignments