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ソルバーを動かすときには，論理式を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ソルバーで解いてみた．
まずは，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

LaTeX でサイズを調整するための geometry package に関する情報

• マニュアル (CTAN内)
• blog記事
• 用紙サイズ関係 (passオプションなど) by ZR氏

https://wiki.eclipse.org/Eclipse.ini#Specifying_the_JVM を参照．

eclipse.ini を書き換える．以下を，-vmargs の直前に追加．-vmは単独の行にすること．

-vm
(javaw.exeへのフルパス)

これでも，exit code=1 で失敗する場合には，javaw.exe でなく，jvm.dll へのフルパスを用いる．

LaTeX の2カラムの文書で \begin{table*}[b] としても 表がページ下部にうまく配置されずに後ろに回されてしまう．この場合は，\usepackage{stfloats} すると良いようだ．ついでに，[b] でなく， [bp] とすべきであるらしい．

keywords: tex, latex, two columns, bottom, table

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

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

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

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

Keyword: file process open in use resource monitor