python の stderr の buffering

Python では,stderr がデフォルトでバッファリングされているようである.(cygwinからやっているのでそう見えるだけ??) stack overflow によると,以下のようにすれば良いそうだ.

import os
import sys
buf_arg = 0
if sys.version_info[0] == 3:
    os.environ['PYTHONUNBUFFERED'] = '1'
    buf_arg = 1
sys.stdout = os.fdopen(sys.stdout.fileno(), 'a+', buf_arg)
sys.stderr = os.fdopen(sys.stderr.fileno(), 'a+', buf_arg)

少なくとも,python 2.7 では,これでOKなようである.

keyword: standard error, standard out

SATソルバー,Tseytin 変換

SATソルバーを動かすときには,論理式をCNFで与えなければならない.初めからうまく書ければ良いが,ただでさえ論理式を作るのは面倒なので,論理式自体は普通に書いておいて,あとからCNFに変換した方が考えやすい.分配則を使って変換すると,論理式のサイズが指数的に増大してしまうので,Tseytin変換を用いる.Wikipediaの記事の通り変換すると,結構余計な変数を導入してしまう.以下のようにしたら良いように思う.まあ,後でSATソルバーが動くので,どれくらい益があるかわからないけれども.

基本的な考え方: 否定標準形の論理式 f を充足させたいとする.f の中に,a and b という部分があったとき,新しい変数 v を導入する.f が充足可能であることと, f’, not v or a, not v or b がみな充足可能であることが同値になる.ただし,f’ は, fk の a and b の部分を変数 v で置き換えたもの.

これを確認すると,まず,fが充足可能だとすると,その割当での a and b の値を v に割り当てれば,書き換え後の3つの論理式は充足される.逆に書き換え後の論理式が充足可能だとして,その割当で v が true であれば,a も b も true になるので,元の論理式列は充足される.vがfalseであるときには,fとf’は否定標準形なので,f は,a and b の部分が true であっても false であっても充足される.

ということで,論理式fが与えられたとき,以下の手続きで得られる節集合Cの全部が充足できることと,fが充足できることが同値になる:

f を否定標準形f0にする.「節集合」Cを空にして,「未処理論理式集合」Yをf0のみを含む集合として以下の手続きを繰返し行い,Yが空になったときのCが求めるものである.

  • Yから一つ論理式gを取り出す.
  • gがリテラル (変数やその否定) なら,gをCに追加する.
  • gが and(h1, .., hn) なら,h1, …, hn を Y に追加する.
  • gが or(h1, …, hn) の場合は,次のようにする.
    • h1, …, hn の中には or(…) の形のものが無いようにする.もし有ったら,リストに吸収してしまえば良い. (たとえば,or(v1, and(v2, or(v3, v4)), or(v5, or(v6, v7, v8), v9)) → or(v1, and(v2, or(v3, v4)), v5, v6, v7, v8, v9))
    • 各 j = 1, …, n に対して,リテラル xj と論理式の集合 Pj を次のように定める.
      • hj がリテラルなら,xj = hj.Pj は空集合.
      • hj が and(h1′, …, hm’) なら,新しい変数 v を導入して,xj = v.Pj = {or(not v, h1′), …, or(not v, hm’)}
    • そして,Cに,or(x1, …, xn) を追加し,各Pj の要素をすべて Y に追加する.

スリザーリンクをSATソルバーで解く

スリザーリンクをSATソルバーで解いてみた.
まずは,minisat-2.2.0を使用.以下の制約を与えた.

  1. 問題升の辺の数
  2. 各頂点につき,辺の数は0または2
  3. 辺にランクを与える.問題で1以上の値が与えられている升をひとつ任意に固定し,この升の周囲の辺をすべてランク0とする.他の辺は,隣接辺のどれかが自分よりもランクが低い

ランクに整数が出てくる.「2進エンコーディング」とした.つまり,各辺edgeと整数nに対し,「edgeのランクの2進表記の第n桁の値が1」という命題に変数を割り当てた.「順序エンコーディング」(rank(edge) < n という命題に変数を割り当てる) も考えたが,出てくる制約が大小比較だけなので,2進エンコーディングの方が変数の数が少ない分有利,と判断した.実験して比較すれば良いのだけれど.

動作させてみたが,結構時間がかかる.問題サイズが10×10だと1-2秒で返ってくるが,45×31だと,2分弱かかる.もちろん問題にも依存するだろうから,もっと計らなくてはいけないが.

そこで,今度は次の方針にしてみた: 制約1,2のみでSATソルバーで解かせ,出てきたものを輪に分解し,各々の輪について,そのどれかの辺はOFFでなければならない,という制約を追加して再びSATソルバーにかける.これを輪の数が1になるまで繰り返す,

この場合,(k+1)回目の制約条件はk回目のそれに対する追加なのだから,k回目の計算過程 (学習節とか) を覚えていて,k+1回目の計算で利用してほしい.でないと,毎回同じ計算を繰り返すことになって遅くなってしまう.いわゆるインクリメンタルな解法である.どうも,minisatは,インクリメンタルに行おうとすると,APIを使ったプログラムを書かなくてはならず,外側から起動するのではだめなようである.

そこで,Z3を使うことにした.Z3ならば整数の演算ができるので,辺の型はBoolのままだけれど,制約1,2の表現を「trueは1, falseは0として,和がn」として書いてみた.するとあまり速くない.上のminisat版と同じくらいかかる.制約1,2を元と同じようにBool式だけで書いてやったら,速くなった.45×31が,30秒強である.

keyword: slither link SAT solver incremental

minisat-2.2.0

minisat-2.2.0.tar.gz はminisat pageで配布されている.cygwinでコンパイルすることができる.ただし,READMEに書いてあるとおりにするとエラーになる.いささか乱暴だが,utils/System.cc の上の方 (多分23行目) にある

#if defined(__linux__)

を,

#if 1

と書き換えれば,コンパイルできる.

firefox で PDF の印刷がハングアップする件

firefox で PDF の印刷がハングアップする件について,Googleを引いて出てきた解決策が当たりだった.

ツール→オプション→詳細→ブラウズ→ハードウェアアクセラレーション機能を使用する のチェックマークを外す.

keywords: print pdf hangup freeze crash hang firefox 応答なし

 

firefox の java applet

firefox は,32bit版と64bit版があるが,64bit版では,Java applet は動作しない.32bit版のfirefoxでJava appletをどうささせるためには,当然,32bit版のJREをインストールする必要がある.JREは32bit版と64bit版の両方をインストールすることができるようだ.

keywords: アプレット

 

ファイルを使用しているプロセス

Windows で,ファイルを使用しているプロセスは,リソースモニターで見つけることができる.例えば,USBメモリが外せないときなどに使える.リソースモニターのCPUタブの「関連付けられたハンドル」の「検索ハンドル」のところに,適当に入力する.「D:」とか「C:\home\abc\def.txt」とか.そのファイルを開いているプロセスが表示される.

Keyword: file process open in use resource monitor