元画像を表示

この記事はSYSKEN Advent Calendar 2021 19日目の記事です。

2週目が回ってきました、あらたです。

今回は夏休みの間に作っていたSATソルバーについて少し話をします。とはいえ、論理学を専攻しているわけではないので念のため以下にわかりやすい資料のリンクを貼っておきます。

• https://jssst-ppl.org/workshop/2017/slides/ppl2017_c4_soh.pdf
• https://rkx1209.hatenablog.com/entry/2017/12/17/175439

1. SATソルバーとは

次のような論理式を考えます。

(x1 | x2) & (!x1 | !x2)

x1とx2にfalseもしくはtrueを代入して、この論理式全体の値をtrueにできるでしょうか。答えは、可能です。例えばx1=true、x2=falseとしたときに、論理式全体の値をtrueにすることができます。このように、論理式が与えられたときに変数の値を適切に選んで、論理式全体の値をtrueにできるか判定する問題を、充足可能性問題（SAT問題: SATisfiability problem）と呼びます。そしてこの問題を解いてくれるようなプログラムをSATソルバーと呼びます。

今回は、このSATソルバーを使って二次方程式の解を求めることを目指します。

2. 1bit整数の演算

しかし、論理式を扱うSATソルバーに整数の問題が扱えるとは思えません。いったいどのようにして二次方程式を解かせればよいのでしょうか。

そのために、まずは計算機の仕組みに目を向けてみましょう。我々が使っているコンピューターは半加算器という組み合わせ回路を使って1bitの加算を実現しています。そしてこの回路では、0と1の二値を使って数を表現しています。共通点が見えてきました。

論理式においても、変数に代入できるのはfalseとtrueの二値のみです。つまりは、コンピューターと同じように行えば、論理式でも整数の演算を定義できるのではないのでしょうか。

はい、実は任意の組み合わせ回路はSAT問題に落とし込むことが可能であると知られています。そのために使うのが、Tseytin transformationです。例として、ANDゲートを取り上げてみましょう。Tseytin transformationにより、ANDゲートは次の論理式で表すことが可能です。

(!A | !B | C) & (A | !C) & (B | !C)

この論理式を充足するような変数A、B、Cの組は、常にC = A & Bの関係を満たしています。同様に、ORゲートやNOTゲート、XORゲートなども論理式で表現することが可能です。つまりは、論理式の世界で半加算器を実装してやれば、1bit整数の演算を定義できるというわけです。

3. 整数の演算

次に、2bit以上の整数の演算を定義したいです。そのためにBitVectorと呼ばれる理論を導入します。これは整数を2進数のバイナリとして扱い、その上で算術演算や論理演算などを定義する理論です。

なにやら難しい言葉が並んでいますが、要するに整数を2進数で表現して1bitずつ計算すれば2bit以上の整数の計算もできるよね、という話です。基本的には前節で述べたことの繰り返しなので、その詳細は省略します。

そんなこんなで、足し算をSAT問題に変換してSATソルバーに渡してあげると、SATソルバーで足し算を計算することができます。以下の画像では、11 + x = 15の解を求めています。

4. 二次方程式の解を求める

ここまでで、足し算をSAT問題に変換できることがわかりました。あとは論理回路の知識を使って掛け算を定義してやれば、二次方程式を表現できるようになります。

これはx^2 – 6x + 9 = 0 を解いたときのツイート

簡単な2次方程式が解けるようになった pic.twitter.com/VM0hAditN6

— arata (@arata_nvm) November 1, 2021

5. おわりに

普段使っているangrやz3で「SATソルバー」という単語を聞いたことはありましたが、その背景理論まで学んだのは初めてでした。今後はこのSATソルバーを使ってSMTソルバーを実装できると面白そうだなと思っています。

明日はTomooki君の投稿です。お楽しみに！

元画像を表示

この記事は、SYSKEN Advent Calendar 2021 3日目の記事です。

あらたです。 後期中間試験が終わり、最近は寒い日が続くようになってきました。

今回はシステム研究部で開発・運用を行っている入退室管理システムについて書いていきます。

目次

• 背景
• 作ったもの
• 使用した技術
• 感想

背景

昨年度から本校では感染症対策のため、課外活動に参加した学生を記録するようになりました。これを受けてシステム研究部では、Google Formsを使用して課外活動に参加した部員を記録していました。しかしこの方法は、正直に言ってかなり面倒です。記録を取るためだけに以下の行程が必要になります。

1. QRコードをスマホで読み取る
2. 必要な情報を記入する
3. 送信する

1回の記録に1分かかると考えれば、5年間ある高専生活のうち30時間を無駄にすることになります。貴重な青春時代をそんなことで失うわけにはいきません。そこで、学生証だけで記録を取ることができる本システムのアイデアを思いつきました。

作ったもの

部室の入室時と退出時に学生証をかざすと、氏名と時刻が自動で記録されます。同時にSlackのチャンネルにも投稿され、誰が部室にいるのかを観測できます。

初期バージョンの開発期間は1日で、部費で購入してもらった機器が届いたその日のうちに動くものをつくりました。高専プロコンで忙しい時期に他のことをしたくなるのはよくあることだと思います。

使用した技術

構成図は以下のようになっています。

クライアントサイド

ハードウェアとして、鯖室にあったRaspberry Pi Model B+ v1.2と購入したSony PaSoRi RC-S380を使用しています。ここらへんの機材を発掘できるのは鯖室のよいところだと思います。

こちら側でしている処理は非常に単純で、学生証から読み取った学籍番号をサーバーに投げるだけです。インターネットへの接続や重複を防ぐ処理など面倒な部分がいくつかありましたが、それだけでした。

サーバーサイド

GolangとEchoでAPIサーバーを実装して、それをHerokuにデプロイしています。クライアントから受け取った情報は適切な加工を施したあとにGoogle Sheetsへ保存します。

最初はDBに保存しようと考えていましたが、データの取り出しやすさや安定性を考え最終的にGoogle Sheetsを選択しました。スマホからもデータを確認することができるため、よい選択だったのではと考えています。

「記録されたデータの可視化を行うサイトを構築する」というアイデアもありましたが、氏名や学籍番号、活動時間といった個人情報がインターネットに公開されるのはまずいと考え断念しました。ただ、かなりの量のデータが収集されるため、部内ハッカソンでなにかに活かせればと思っています。

感想

今のところは元気に動いてくれていてとても楽しいです。アイデア段階ではまったく想定していなかった活用方法もあり、なかなか便利なシステムになりました。特に、誰が部室にいるのかを把握できるようになったのは一つの革命だと思っています。

一方で、以前までシス研で使用されていた鍵管理ツールのように製作者依存の運用になっていることは大きな課題です。部として運用するための仕組みを整えつつ、今後もシステムを改善していきたいです。

明後日はTomookiの投稿です。お楽しみに！

元画像を表示

こんにちは、2年生のarataです。

11月14日に開催されたKOSENセキュリティコンテスト2020に参加したのでその報告です。弊学からは1チームのみの参加でした。

目次

• KOSENセキュリティコンテスト2020とは
• 結果
• 感想

1. KOSENセキュリティコンテスト2020とは

全国の高専生を対象としたコンテストです。情報セキュリティに関連した技術を用いて、出題された問題を解きそのスコアを競います。今年は24の高専から51チームが参加していました。

2. 結果

チーム”helix”として参加して51チーム中7位でした。

去年と同じ順位というのは何ともコメントし難いのですが、まあ精進を怠った当然の結果でしょう。

3. 感想

去年は学校のプロキシが悪さをしていたので、今年は別の回線を用意していたのですがとくにトラブルは発生しなかったので良かったです。

また、テスト前にも関わらず一緒に参加してくれたtamuaki君には感謝の言葉しかないです。

来年も頑張ります。

元画像を表示

はじめまして、1年生のarataです。
1ヶ月ぐらい前の話ですが、高専セキュコン2019に参加したのでWriteupのついでに参加記を書きます。

コンテストにはチーム”helix”(画像では”hex”)として友人2人と参加し、結果は7位でした。

1. 高専セキュコンとは

CTFと呼ばれる、セキュリティの技術や知識を競うコンテストの一つです。暗号を解読したり実行ファイルを解析したりして、”フラグ”と呼ばれる文字列を手に入れると得点を得ることができます。

詳細は下記の公式サイトを見てください。

https://www.ishikawa-nct.ac.jp/lab/I/k_seccon2019/

2. Writeup

Writeupを書くまでがCTFというような慣習があるので書きました。
10分クオリティかつそこそこ長くなるので、こちらにまとめてあります。

3. 終わりに

いかがで　チームとしてCTFに参加するのも高専セキュコンに参加するのも初めてでしたが楽しむことができました。ただ、7位という微妙な順位で終わってしまったのがかなり悔しかったので、次回は5位以内を目指したいです。