Study of branch and bound for incremental SAT

Satisfiability Problem (SAT) is a decision problem that is widely applied in a variety of real-world applications. One important issue when dealing with SAT problems is to maintain the satisfiability of a propositional formula when a conjunction of new clauses is added. This consists of solving SAT problems in an incremental way (also called incremental SAT). This has motivated us to develop a new method for solving incremental SAT. We will show in this thesis that our method outperforms the previous methods that have been proposed in the literature.; Temporal reasoning is another interesting topic. Temporal Constraint Satisfaction Problem (temporal CSP), as a special instance of temporal reasoning, is a framework useful for representing and answering queries about the times of events and the temporal relations between them. Current work on solving temporal CSP mainly focuses on performing a systematic search with constraint propagation on the original problem. This thesis provides a different approach which transforms the temporal CSP to SAT and then solves the resulting SAT to get the desired solutions. This allows us to solve incremental temporal CSP problems by converting them to incremental SAT and use the solving method we propose.