ナンバーリンクの http://bach.istc.kobe-u.ac.jp/papers/pdf/da2014talk.pdf でのSATエンコーディング、無向ではなく有向グラフとして形式化してるんだな…… 領域分割しての出次数と入次数の差による補題を表現するため？