SAT変換に基づく制約ソルバーとその性能評価
本論文では，SAT変換に基づく制約ソルバーであるSugarの概要とその性能評価結果について述べる．Sugarは，制約充足問題(CSP)，制約最適化問題(COP)および最大制約充足問題(Max-CSP)を，命題論理の充足可能性判定問題(SAT問題) に変換し，MiniSat等の高速なSATソルバーを用いて求解を行うシステムである．SAT変換には，order encodingと名付けた新しい方法を用いており，従来広く用いられているdirect encodingやsupport encodingよりも，多くの問題に対して高速な求解が可能である．本論文では，order encodingの説明を含めたSugarの概要について述べた後，2008年に開催された第3回国際CSPソルバー競技会およびMax-CSPソルバー競技会での結果を基にSugarの性能評価結果を報告する．なお，Sugarは同競技会の10
SAT/SMTソルバの仕組み
NLP コロキウム https://nlp-colloquium-jp.github.io/ で発表した際のスライドです。 論文: https://arxiv.org/abs/2205.01954 GitHub: https://github.com/joisino/wordtour 概要 単語埋め込みは現代の自然言語処理の中核技術のひとつで、文書分類や類似度測定をはじめとして、さまざまな場面で使用されていることは知っての通りです。しかし、ふつう埋め込み先は何百という高次元であり、使用する時には多くの時間やメモリを消費するうえに、高次元埋め込みを視覚的に表現できないため解釈が難しいことが問題です。そこで本研究では、【一次元】の単語埋め込みを教師なしで得る方法を提案します。とはいえ、単語のあらゆる側面を一次元で捉えるのは不可能であるので、本研究ではまず単語埋め込みが満たすべき性質を健全性と完
制約充足問題として最強のボジョレーを求める - Debug me
ちゃお......舞いおりん......† 今回は#ajiting Advent Calendar 2015の8日目ということでVOYAGE GROUPの多目的スペースAjitoにむりやり絡めて話そうと思います。 はじめに 先月の話になってしまいますが、今年もボジョレーヌーボーが解禁されました。 解禁日はAjitoでも終業後に飲んでる人がちらほらいたそうです (私はその日体調悪くて家に直帰しました...†) さてボジョレーヌーボーといえば、毎年公開されるキャッチコピーが話題ですね。Wikipediaに年ごとのものが載っているのでちょっと挙げてみますとこんな感じです。 1995年「ここ数年で一番出来が良い」 1996年「10年に1度の逸品」 1997年「まろやかで濃厚。近年まれにみるワインの出来で過去10年間でトップクラス」 1998年「例年のようにおいしく、フレッシュな口当たり」 1999
The Problem with Curation
Recently I received a question from a user asking about "cabal hell" when installing one of my packages. The scenario in question worked fine for us, but for some reason it wasn't working for the user. When users report problems like this they usually do not provide enough information for us to solve it. So then we begin the sometimes arduous back and forth process of gathering the information we
GECODE - An open, free, efficient constraint solving toolkit
Gecode Gecode is an open source C++ toolkit for developing constraint-based systems and applications. Gecode provides a constraint solver with state-of-the-art performance while being modular and extensible. Gecode is: open Gecode is radically open for programming: it can be easily interfaced to other systems. It supports the programming of new constraints, branching strategies, and search engines
Introduction to Max-SAT and Max-SAT Evaluation
This document provides an introduction to Max-SAT and Max-SAT evaluation. It discusses SAT and related problems like Max-SAT and pseudo-boolean optimization. The author shares their experience submitting their solver "toysat" to the Max-SAT evaluation in 2013. For Max-SAT 2014, the author plans to submit improved versions of SCIP, FibreSCIP, and toysat. The document concludes by discussing interac
Sugar: a SAT-based Constraint Solver
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
<hr> <!– <img width=“20%” src=“banbara.png”><br> –> <font size=“-1”> <table> <tr> <td><img width=“150px” src=“soh.png”></td> <td class=“button2”><a href=“http://www.edu.kobe-u.ac.jp/istc-tamlab/”>Tamura Lab.</a><a href=“http://kix.istc.kobe-u.ac.jp/~soh/jp/”>T. Soh</a></td> </tr> </table> </font> <img src=“http://cgi.center.kobe-u.ac.jp:8000/cgi-bin/Count.cgi?df=svc00652-cspsat.dat%7Cdd=C” align=a
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.sci.brooklyn.cuny.edu/~zhou/papers/padl16.pdf
http://www.sci.brooklyn.cuny.edu/~zhou/papers/padl16_slides.pdf
CiteSeerX
https://www.cs.upc.edu/~oliveras/TDV/dl.pdf
MiniZinc
CSPLib: A problem library for constraints
Catalogue
Sudoku, Linear Optimization, and the Ten Cent Diet
SWI-Prolog -- library(clpfd): CLP(FD): Constraint Logic Programming over Finite Domains
SWI-Prolog -- library(clpb): CLP(B): Constraint Logic Programming over Boolean Variables
http://www.constraint.org/index_ja.html
Welcome to the ACP | Association for Constraint Programming