はてなブックマーク

人工知能学会誌 第25巻 第1号 (2010年1月) 特集「最近のSAT技術の発展」 特集「最近のSAT技術の発展」にあたって 井上 克巳 (国立情報学研究所) 田村 直之 (神戸大学) 命題論理の充足可能性判定問題(SAT)は，与えられた命題論理式の充足可能性を 判定する問題であり，最初にNP完全性が証明された問題でもある． SATは人工知能および計算機工学における最も基本的な問題として， 論理合成，システム検証，プランニング問題，スケジューリング問題， 制約充足問題，制約最適化問題，定理証明など，さまざまな分野に応用されている． 近年，106--107 個の変数をもつ大規模なSATインスタンス(SAT問題)を， 非常に高速に解くことが可能なSATソルバーが実現され，これらの分野への実用 的応用が急速に拡大している． このように，与えられた問題を論理式で表現しSATソルバーを用いて解くこ

はじめに ニコリなどによる 様々なパズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます． 数独(Sudoku)パズルをSugar制約ソルバーで解く カックロ(Kakuro, Cross Sums)パズルをSugar制約ソルバーで解く 美術館(Akari, Light Up)パズルをSugar制約ソルバーで解く 四角に切れ(Shiaku)パズルをSugar制約ソルバーで解く ナンバーリンク(Number Link)パズルをSugar制約ソルバーで解く ましゅ(Masyu)パズルをSugar制約ソルバーで解く スリザーリンク(Slitherlink)パズルをSugar制約ソルバーで解く 橋をかけろ(Hashiwokakero)パズルをSugar制約ソルバーで解く (一部作成中) ヤジリン(Yajilin)パズルをSugar制約ソルバーで

Please try Java with Cream. Although I personally prefer black coffee in real life... JAVA+CREAM=SOLVER What's New Copris (Constraint Programming in Scala) version 1.0.0 is released (August 28, 2011). Sugar version 1.14.6 became the winner in 3 categories out of 7 categories of the 2009 Fourth International CSP Solver Competition. A SAT-based Constraint Solver Sugar version 1.13 is repleased on Ju

Sugar is a SAT-based Constraint Solver. Constraint Satisfaction Problem (CSP) is encoded to a Boolean CNF formula, and it is solved by an external SAT solver. Sugar also can solve Constraint Optimization Problems (COP) and Max-CSP. Sugar is an award winning solver of global constraint categories at the International CSP Solver Competitions in 2008 and 2009, and of four categories at the 2008 Inter