~pmikkelsen/APL-sat

1ef71857afbc87204cbdc73b675fa076913556d6 — Peter Mikkelsen 2 years ago master
Add what I have
5 files changed, 57 insertions(+), 0 deletions(-)

A anySat.aplf
A parse.aplf
A satCount.aplf
A satisfiable.aplf
A tautology.aplf
A  => anySat.aplf +16 -0
@@ 1,16 @@
 anySat←{
     ⎕IO←0
     (vars bdd)←⍵
     bdd[1;1]=0:⎕SIGNAL 11
     2=≢vars:⍬ ⍝ No variables
     assignments←1⍴⍨¯2+≢vars
     assign←{
         ⍵<2:0
         (var low high)←bdd[⍵;]
         low=0:assign high
         assignments[var-2]←0
         assign low
     }
     _←assign ¯1+≢bdd
     (2↓vars),⍪assignments
 }

A  => parse.aplf +22 -0
@@ 1,22 @@
 R←parse expr;⎕IO;ops;tokens;vars;n;BDD;true;false;mk;build;_
 ⎕IO←0
 ops←'∧∨⍲⍱≠=~'
 tokens←{~∘' '¨⍵⊆⍨1++⌿+\(¯1∘⌽+⊢)(ops,'()')⍷⍤0 1⊢⍵},expr
 vars←∪(,¨'01'),tokens~,¨ops,'01()'
 n←≢vars
 tokens←{((⍳n),⍵)[vars⍳⊂⍵]}¨tokens
 BDD←2 3⍴n 0 0
 mk←{
     =⌿1↓⍵:⊃⌽⍵
     1=≢u←⍸∨/⍵⍷BDD:⊃u
     BDD⍪←⍵
     ¯1+≢BDD
 }
 build←{
     ⍺≥n:{⍵⊣{⍵<2:BDD[⍵;1 2]←1}⍵}⍎⍕⍵
     l←(⍺+1)∇ 0@(⍺∘=)⊢⍵
     h←(⍺+1)∇ 1@(⍺∘=)⊢⍵
     mk ⍺ l h
 }
 _←2 build tokens
 R←vars BDD

A  => satCount.aplf +11 -0
@@ 1,11 @@
 satCount←{
     ⎕IO←0
     bdd←⊃⌽⍵
     u←¯1+≢bdd
     count←{
         ⍵∊0 1:⍵×bdd[⍵;1]
         (var low high)←bdd[⍵;]
         +⌿{(count ⍵)×2*bdd[⍵;0]-var+1}¨low high
     }
     (count u)×2*bdd[u;0]-2
 }

A  => satisfiable.aplf +4 -0
@@ 1,4 @@
 satisfiable←{
     (vars bdd)←⍵
     1 1≡bdd[⎕IO+1;1+⍳2]
 }

A  => tautology.aplf +4 -0
@@ 1,4 @@
 tautology←{
     (vars bdd)←⍵
     (2 2⍴0 0 1 1)≡bdd[⍳2;1+⍳2]
 }