著者

迫 龍哉 宋 剛秀 番原 睦則 田村 直之 鍋島 英知 井上 克巳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.4, pp.4_16-4_29, 2016-10-25 (Released:2017-01-14)

---

近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,問題をSATに変換し,SATソルバーを用いて求解するSAT型ソルバーが成功を収めている.しかしながら,最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある.この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる.SATソルバー競技会のひとつであるSAT Race 2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された.本論文では,それを拡張したインクリメンタルSAT APIであるiSATを提案し,その応用について述べる.提案する拡張により,問題を簡潔に記述でき,Javaからの利用も可能になる.また,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対する実験結果を通じ,iSAT利用の有効性を示す.

著者

藤井 樹 伊藤 靖展 鍋島 英知

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会論文誌 (ISSN:13460714)

巻号頁・発行日

vol.34, no.3, pp.A-I91_1-16, 2019-05-01 (Released:2019-05-01)

参考文献数

14

---

We consider the laboratory assignment problem in which laboratories have minimum and maximum quotas. MSDA proposed by Fragiadakis, et al., is an efficient algorithm to solve the laboratory assignment problem, but it is incomplete to find a fair assignment. In this paper, we show three extensions of the laboratory assignment problem and translations from the extensions to constraint optimization problems. The first extension enables a completeness to find a fair assignment if it exists, but loses strategy-proofness. The original and first extended laboratory assignment problem may have no fair assignment. This is caused by redundant claims of an empty seat. The second extension based on the first one ensures that the laboratory assignment problem has at least one fair assignment by making a claim of an empty seat stricter. The third extension introduces tied ranks to students' preferences over laboratories, for example, students can specify multiple laboratories as their first choice. This extension gives the Žexibility to specify students' preferences and makes it possible to find more desirable assignments. The experimental results show that our approaches requires more computational time compared with MSDA, but can always find a fair assignment and a more desirable one.

著者

宋 剛秀 番原 睦則 田村 直之 鍋島 英知

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.4, pp.72-92, 2018-10-25 (Released:2018-12-26)

---

命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソフトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最新動向として,性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次に SAT ソルバーの利用技術の視点から,SAT ソルバーの機能面の進化と符号化技術を組み合わせることで,複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.

著者

岩沼 宏治 鍋島 英知 Koji Iwanuma Hidetomo Nabeshima

雑誌

人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence (ISSN:09128085)

巻号頁・発行日

vol.25, no.1, pp.86-95, 2010-01-01

著者

鍋島 英知 岩沼 宏治 井上 克巳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.4, pp.4_146-4_160, 2012-10-25 (Released:2012-11-25)

---

命題論理の充足可能性判定問題(SAT問題)を解くソルバーは,その飛躍的な性能向上に伴い,システム検証やプランニング・スケジューリング問題,制約充足・最適化問題等の様々な分野において活躍している.GlueMiniSat 2.2.5は,単位伝搬を促し矛盾の発生を促進する学習節を積極的に獲得する戦略に基づくSATソルバーである.学習節の評価尺度には,AudemardとSimonが開発したSATソルバーGlucoseで導入されたリテラルブロック距離を改良した尺度を用い,単位伝搬を促進する学習節を獲得・保持する.また良い学習節の獲得を促すため,非常に積極的なリスタート戦略を採る.我々は代表的SATソルバーであるMiniSat 2.2を基にこれらの手法を実装し,GlueMiniSat 2.2.5を開発した.GlueMiniSat 2.2.5は充足不能性の証明に強く,SAT 2011競技会のApplication部門において逐次型ソルバーとしてUNSATクラスで1位,SAT+UNSATクラスで2位を獲得している.また並列型ソルバーを含めても同部門UNSATクラスで2位を獲得している.

著者

小谷 忠史 中村 正人 岩沼 宏治 鍋島 英知

雑誌

情報処理学会研究報告データベースシステム(DBS)

巻号頁・発行日

vol.2002, no.67, pp.99-106, 2002-07-18

---

現在Webへのアクセス法としてPDAなど携帯端末の利用が増えてきている.PDAはWebページを何時でも何処でも表示できる利点があるが,幾つかの問題もある.小さな表示画面,遅い通信速度,操作性の悪さの問題などにより,PDAによって欲しい情報を即座に簡単に得るのは難しい.本論文ではWeb ページの時間的差分データの表示を念頭において,ユーザがWebページの表示する部分を事前に指定して,その部分の最新の差分情報を即座に容易に表示する手法を提案・考察する.また以上を実現する時間的差分データ監視・表示システムを実装し評価したので報告する.Access to World-Wide-Web (Web) by Personal DigitalAssistants (PDAs) has been increasing.PDAs can browse Web site WithPDAs anywhere at any time, but there are some difficult problems.For example,PDA's screen size is rather small, the transmission speed isconsiderably low and PDA's usability needs to be still improved.Therefore it is difficult for a user to get his information easily andquickly.To solve those problems,we study how to display some parts ofa Web page, which a user wants to watch continuously. In this paper wepropose a system which asks a user preliminarly which parts of a Webpage should be displayed on a PDA's display. This system continuously tries to detect the temporal difference of the target pages, and informs the user about the detected difference with PDAs in the appropriate form.

著者

鍋島 英知 宋 剛秀

出版者

社団法人人工知能学会

雑誌

人工知能学会誌 (ISSN:09128085)

巻号頁・発行日

vol.25, no.1, pp.68-76, 2010-01-01

被引用文献数

6