A study on the search algorithms in propositional logic with an application in bioluminescence tomography

This thesis is a study of search algorithms in automated reasoning with propositional logic: propositional satisfiability and maximum satisfiability. An application of propositional logic reasoning to bioluminescence tomography is introduced in the thesis.;Propositional satisfiability (SAT for short) is the problem of deciding whether or not a propositional expression is satisfiable. Local search algorithms, incomplete in natural, are one of the most effective methods for solving hard SAT problems. A complete local search algorithm is presented, which adds new clauses from ordered resolution at each local minimum so local minima disappear gradually and a global optimal solution is easily found.;The Maximum satisfiability problem (MAX-SAT for short) tries to find a truth assignment that satisfies the most clauses in a boolean expression. One of the most popular methods for MAX-SAT is based on branch-and-bound algorithms. Two new lower bound functions, which are consistently better than other lower bound functions, are introduced. Based on strongly connected components of the implication graph of a 2CNF formula, a new variable ordering and a simplification method are provided to improve performance.;Bioluminescence tomography (BLT for short) was introduced in 2002 to study biological processes in vivo at the cellular and molecular levels. This technique uses the surface measurement data of a small animal to recover the location and strength of the bioluminescence source. In the thesis, a new multi-view and multi-spectral bioluminescence tomography system is introduced to reduce the capture time and compensate for the decay of the bioluminescence signal. A temperature-modulated BLT algorithm is introduced by heating a small volume of tissue to create a signal difference, which is only related to the bioluminescence source in the heated volume. A depth-limited depth-first search algorithm using propositional logic reasoning is proposed to solve the BLT optimization problem. In this search algorithm, more biological information can be used as constraints, and it helps to prune the solution space and improves the result. The experimental results show the new algorithm can robustly recover the bioluminescent source information.