ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

  1. 020 学位論文
  2. 複合科学研究科
  3. 17 情報学専攻

Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems

https://ir.soken.ac.jp/records/2685
https://ir.soken.ac.jp/records/2685
a467588e-65da-4ae7-b059-8254b1cf7cd3
名前 / ファイル ライセンス アクション
甲1455_要旨.pdf 要旨・審査要旨 (274.9 kB)
甲1455_本文.pdf 本文 (7.8 MB)
Item type 学位論文 / Thesis or Dissertation(1)
公開日 2012-04-02
タイトル
タイトル Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems
タイトル
タイトル Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems
言語 en
言語
言語 eng
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_46ec
資源タイプ thesis
著者名 宋, 剛秀

× 宋, 剛秀

宋, 剛秀

Search repository
フリガナ ソウ, タケヒデ

× ソウ, タケヒデ

ソウ, タケヒデ

Search repository
著者 SOH, Takehide

× SOH, Takehide

en SOH, Takehide

Search repository
学位授与機関
学位授与機関名 総合研究大学院大学
学位名
学位名 博士(情報学)
学位記番号
内容記述タイプ Other
内容記述 総研大甲第1455号
研究科
値 複合科学研究科
専攻
値 17 情報学専攻
学位授与年月日
学位授与年月日 2011-09-30
学位授与年度
値 2011
要旨
内容記述タイプ Other
内容記述    Optimization and enumeration problems have been actively studied. There are not only academic interests but also real world applications as many researches have been done for industrial purpose. However, despite the recent advancements in computer technology, there are still difficult problems to solve. To break this situation, we focus on technologies in solving propositional satisfiability (SAT). Although SAT technologies are not so focused as a method for optimization and enumeration problems, the recent progress of SAT technologies is so tremendous that it can be expected to become a potential approach. In this thesis, we particularly study a method utilizing SAT technologies, which is called incremental SAT solving, and apply it to optimization and enumeration problems.
   The propositional satisfiability problem (or the Boolean satisfiability problem), the SAT problem for short, is a problem that has been paid much attention in computer science. When a propositional formula is given, the solution of the SAT problem is whether there is an assignment satisfying the given formula or not. SAT technologies have been studied in several research domains such as computational logic and electronic design automation until today. In 1962, Davis et al. develop a procedure called DPLL, which has become the basis of modern SAT solvers. Since 2000, the effective implementation of SAT algorithms has become a popular topic as well as search strategies. For instance, a SAT solver Chaff features the two literal watching mechanism and it is outstanding to others. Following that, Eén and Sörensson polish up the implementations of previous solvers and provided an extensible SAT solver. These technologies are now matured and should be applied to a wide range of problems. However, since the solvers are developed for the SAT problem that is a decision problem, we need some extension to apply them to such a wide range of problems.
   In this thesis, we study a method called incremental SAT solving. It incrementally computes the satisfiability of a sub-problem obtained from a given original problem until a given goal condition is satisfied. We review how previous approaches utilizing SAT technologies are explained by this solving method. Following that, we also review several applications of it and how to utilize learned clauses for acceleration. The main contribution of this thesis is applying this incremental SAT solving to the following optimization and enumeration problems.
   We apply incremental SAT solving to an optimization problem, the two-dimensional strip packing problem (2SPP). In this problem, we are given a set of rectangles and one large rectangle called a strip. The goal of the problem is to pack all rectangles without overlapping, into the strip by minimizing the overall height of the packing. Although the 2SPP has been studied in operations research, some instances are still hard to solve. Our method solves the 2SPP by translating it into SAT problems through a propositional encoding called order encoding. The size of translated SAT problems tends to be large; thus, we apply several techniques to reduce the search space by symmetry breaking and positional relations of rectangles. Besides that, to compute the minimum height of a 2SPP, we apply incremental SAT solving with reusing learned clauses. For evaluation, we make comparisons with a constraint satisfaction solver and ad-hoc methods of 2SPP on 38 instances obtained from the literature.
   We then apply incremental SAT solving to the minimal active pathway finding problem that we propose to analyze metabolic pathways. In systems biology, identifying vital functions like glycolysis from a given metabolic pathway is important for better understanding of living organisms. The goal of the problem is to identifying such functional reaction sets in a given metabolic pathways. More specifically, we focus on enumerating minimal active pathways producing target metabolites from source metabolites. We translate laws of biochemical reactions into propositional formulas and apply incremental SAT solving to solve the problem. An advantage of our method is that each solution satisfies qualitative laws of biochemical reactions. Moreover, we can calculate such solutions for a cellular scale metabolic pathway within a few seconds. For evaluation, we apply it to a whole Escherichia coli metabolic pathway and make comparisons with previous approaches.
   In this thesis, we mainly investigate applications of SAT technologies. Apparently, it is simple and seems difficult to apply it to real world problems. However, it has remarkable potential to be core solvers for problems such as optimization and enumeration problems as we show throughout this thesis.
所蔵
値 有
フォーマット
内容記述タイプ Other
内容記述 application/pdf
戻る
0
views
See details
Views

Versions

Ver.1 2023-06-20 15:46:54.359557
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR 2.0
  • OAI-PMH JPCOAR 1.0
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3