@misc{oai:ir.soken.ac.jp:00002685,
 author = {宋, 剛秀 and ソウ, タケヒデ and SOH, Takehide},
 month = {2016-02-17, 2016-02-17},
 note = {   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., application/pdf, 総研大甲第1455号},
 title = {Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems},
 year = {}
}