Z3によるXORを再現するニューラルネットワークの構築

#概要
Microsoftが作ったSAT SolverのZ3を用いて，基本的な論理素子を再現するニューラルネットワークの構築を行う．
それに伴い，１つのパーセプトロンではXORが再現不能であることを示す．
また，XOR再現可能なニューラルネットワークの構成を示す．

#関連する記事

Z3による汎用大域的最適化
http://qiita.com/kotauchisunsun/items/90bce940a1c08ca1b7ae

#実装するニューラルネットワーク
非常に単純なニューラルネットワークで２入力１出力のパーセプトロンを扱う．

出力は

```py
if w1 * i1 + w2 * i2 + b > 0:
    return 1
else:
    return 0
```

![image](https://qiita-image-store.s3.amazonaws.com/0/139643/702b632c-b5bf-b104-5a8a-dd17b072e774.png)


#実際のコード
以下のコードを用いて実行する．

nn_test.py:

```py
#coding:utf-8
import sys
from z3 import *

def and_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if i*j==1:
                ex = w1 * i + w2 * j + b > 0
            else:
                ex = w1 * i + w2 * j + b <= 0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

def or_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if i+j>0:
                ex = w1 * i + w2 * j + b > 0
            else:
                ex = w1 * i + w2 * j + b <= 0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

def nand_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if not i*j==1:
                ex = w1 * i + w2 * j + b > 0
            else:
                ex = w1 * i + w2 * j + b <= 0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

def xor_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if i+j==1:
                ex = w1 * i + w2 * j + b > 0.0
            else:
                ex = w1 * i + w2 * j + b <= 0.0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

if __name__ == "__main__":
    i1 = Real('i1')
    i2 = Real('i2')

    w1 = Real('w1')
    w2 = Real('w2')
    b  = Real('b')

    out = Real('out')

    s = Solver()

    table = {
        "and"  : and_def,
        "or"   : or_def, 
        "nand" : nand_def,
        "xor"  : xor_def,
    }

    table[sys.argv[1]](w1,w2,b,s)
```

#andの場合
| i1 | i2 | 出力 |
|:-:|:-:|:-:|
| 0  | 0 | 0 |
| 0  | 1 | 0 |
| 1  | 0 | 0 |
| 1  | 1 | 1 |

実行するコード

```shell-session
$ python nn_test.py and
> w1*0 + w2*0 + b <= 0
> sat
> [b = 0]
> w1*0 + w2*1 + b <= 0
> sat
> [w2 = 0, b = 0]
> w1*1 + w2*0 + b <= 0
> sat
> [w2 = 0, b = 0, w1 = 0]
> w1*1 + w2*1 + b > 0
> sat
> [w2 = 1, b = -1, w1 = 1]
```

ということが分かった．したがって，andを表すニューラルネットは，

```
w1 = 1
w2 = 1
b = -1
```

で表される．


#orの場合
| i1 | i2 | 出力 |
|:-:|:-:|:-:|
| 0  | 0 | 0 |
| 0  | 1 | 1 |
| 1  | 0 | 1 |
| 1  | 1 | 1 |

実行するコード

```shell-session
$ python nn_test.py or
> w1*0 + w2*0 + b <= 0
> sat
> [b = 0]
> w1*0 + w2*1 + b > 0
> sat
> [w2 = 1, b = 0]
> w1*1 + w2*0 + b > 0
> sat
> [w2 = 1, b = 0, w1 = 1]
> w1*1 + w2*1 + b > 0
> sat
> [w2 = 1, b = 0, w1 = 1]
```

ということが分かった．したがって，orを表すニューラルネットは，

```
w1 = 1
w2 = 1
b  = 0
```

で表される．


#nandの場合
| i1 | i2 | 出力 |
|:-:|:-:|:-:|
| 0  | 0 | 1 |
| 0  | 1 | 1 |
| 1  | 0 | 1 |
| 1  | 1 | 0 |

実行するコード

```shell-session
$ python nn_test.py nand
> w1*0 + w2*0 + b > 0
> sat
> [b = 1]
> w1*0 + w2*1 + b > 0
> sat
> [w2 = 0, b = 1]
> w1*1 + w2*0 + b > 0
> sat
> [w2 = 0, b = 1, w1 = 0]
> w1*1 + w2*1 + b <= 0
> sat
> [w2 = -1, b = 2, w1 = -1]
```

ということが分かった．したがって，nandを表すニューラルネットは，

```
w1 = -1
w2 = -1
b  = 2
```

で表される．nandができたので，これをもって，任意の論理回路がニューラルネットワークによって構築可能であることが分かる．


#xorの場合
| i1 | i2 | 出力 |
|:-:|:-:|:-:|
| 0  | 0 | 0 |
| 0  | 1 | 1 |
| 1  | 0 | 1 |
| 1  | 1 | 0 |

実行するコード

```shell-session
$ python nn_test.py xor
w1*0 + w2*0 + b <= 0
sat
[b = 0]
w1*0 + w2*1 + b > 0
sat
[w2 = 1, b = 0]
w1*1 + w2*0 + b > 0
sat
[w2 = 1, b = 0, w1 = 1]
w1*1 + w2*1 + b <= 0
unsat
Traceback (most recent call last):
  File "nn_test.py", line 73, in <module>
    table[sys.argv[1]](w1,w2,b,s)
  File "nn_test.py", line 51, in xor_def
    print s.model()
  File "/usr/lib/python2.7/dist-packages/z3.py", line 6100, in model
    raise Z3Exception("model is not available")
z3types.Z3Exception: model is not available
```

unsatと出力されてしまった．これから1つのパーセプトロンから，xorの構築は不能であることが分かった．
これはxorの出力が線形分離不能なことから起こる問題で，ニューラルネット界隈ではよく知られた問題だ．これがz3を用いても確認できたことが分かる．


#2段ニューラルネットワークによるxorの構築

以下のようなニューラルネットワークを考える．
これは入力層を2入力にして，2段にしたニューラルネットワークである．このニューラルネットワークを用いることで，xorが構築できるか確かめる．

![image](https://qiita-image-store.s3.amazonaws.com/0/139643/fc8b86be-3719-0893-fc96-3ae8f1c162a3.png)

xor_nn_test.py:

```py
#coding:utf-8

from z3 import *

if __name__ == "__main__":

    w1 = Real('w1')
    w2 = Real('w2')
    w3 = Real('w3')
    w4 = Real('w4')
    w5 = Real('w5')
    w6 = Real('w6')
    
    b1  = Real('b1')
    b2  = Real('b2')
    b3  = Real('b3')

    s = Solver()

    for i in [0.0,1.0]:
        for j in [0.0,1.0]:

            print "-*-" * 10
            o1 = Real('o1%d%d'%(i,j))
            o2 = Real('o2%d%d'%(i,j))
            o3 = Real('o3%d%d'%(i,j))

            s.add(o1 == If(w1 * i + w2 * j + b1 > 0.0 , 1.0, 0.0))
            s.add(o2 == If(w3 * i + w4 * j + b2 > 0.0 , 1.0, 0.0))
            s.add(o3 == w5 * o1 + w6 * o2 + b3)
            
            if i+j==1:
                s.add(o3 > 0.0)
            else:
                s.add(o3 <= 0.0)
            print s.check()
            print s.model()
```

```
$ python xor_nn_test.py
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [w5 = 0,
>  w6 = 0,
>  b3 = 0,
>  b2 = 1,
>  b1 = 1,
>  o300 = 0,
>  o200 = 1,
>  o100 = 1]
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [o301 = 1,
>  w4 = 0,
>  o300 = 0,
>  o201 = 0,
>  o101 = 0,
>  b3 = 1,
>  b2 = 0,
>  o200 = 0,
>  w5 = -1,
>  w2 = -1,
>  o100 = 1,
>  w6 = 0,
>  b1 = 1]
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [o301 = 1,
>  w3 = -1,
>  o300 = 0,
>  o101 = 1,
>  b2 = 1,
>  o200 = 1,
>  w5 = 1,
>  o310 = 1,
>  w6 = -1,
>  b1 = 0,
>  w4 = 0,
>  o201 = 1,
>  b3 = 1,
>  w2 = 1,
>  o110 = 0,
>  o100 = 0,
>  o210 = 0,
>  w1 = 0]
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [o301 = 1,
>  w3 = -1,
>  o300 = 0,
>  o101 = 1,
>  b2 = 2,
>  o200 = 1,
>  w5 = 1,
>  o310 = 1,
>  w6 = 1,
>  b1 = 0,
>  w4 = -1,
>  o201 = 1,
>  o111 = 1,
>  b3 = -1,
>  w2 = 1,
>  o110 = 1,
>  o211 = 0,
>  o311 = 0,
>  o100 = 0,
>  o210 = 1,
>  w1 = 1]
```

satしたことにより，図示したニューラルネットワークでxorが再現できることが分かった．その時の値は

```
w1 = 1
w2 = 1
w3 = -1
w4 = -1
w5 = 1
w6 = 1
b1 = 0
b2 = 2
b3 = -1
```

となることが分かる．この係数からニューラルネットワークについて考察を行うと，
左上のニューラルネットワークは

```
w1 = 1
w2 = 1
b1 = 0
```

という係数から構成されていることが分かる．この結果，左上のニューラルネットワークは"OR"であることが分かる．


左下のニューラルネットワークは

```
w3 = -1
w4 = -1
b2 = 2
```

という係数から構成されていることが分かる．この結果，左下のニューラルネットワークは"nand"であることが分かる．


最後の右のニューラルネットワークは

```
w5 = 1
w6 = 1
b3 = -1
```

という係数から構成されていることが分かる．この結果，左下のニューラルネットワークは"and"であることが分かる．

ここで出力をoutとすると

out = (i1 or i2) and not (i1 and i2)
ドモルガン則により，
out = (i1 or i2) and (not i1 or not i2)
out = (i1 and not i1) or (i1 and not i2) or (i2 and not i1) or (i2 and not i2)
ここで
i1 and not i1 = false
i2 and not i2 = false
なので
out = (i1 and not i2) or (i2 and not i1)
out = i1 xor i2

となり，outがi1,i2のxor出力になっていることが，ここからも分かる．
したがって，２段ニューラルネットワークでxor出力をZ3により再現できたことが分かる．


#まとめ
Z3により単純なパーセプトロンで，and,or,nandが構築可能であり，nandが構築不能であることを示した．
また，Z3で２段のニューラルネットワークでxorが構築可能であることを示した．また，その部分のパーセプトロンが，and,or,nandと同等の動作を確認し，論理式からもxorが出力されることを示した．