| The satisfiability of a propositional formula is one of the most studied problems in computer science, from both theoretical and practical standpoints. Algorithm based on techniques like stochastic local search [GW93, SKC93], backtracking search [SS96, Zha97, MMZ+01, GN02], and Stalmarck's proof procedure [SS98] have been implemented; their increasing efficiency has led to more problems being tackled by reduction to SAT. While some of these applications only require a yes-no answer, an increasing number of them relies on the solver's ability to provide a proof of unsatisfiability [ZM03], a satisfying assignment that is minimal according to some metric [ARMS02, CK03, RS04], or an enumeration of all satisfying assignments to a propositional formula [McM02].; In this thesis, an efficient algorithm for finding all satisfying assignments is proposed. First, new algorithms for hybrid satisfiability solving are proposed. Especially strong conflict analysis, new decision heuristic and incremental SAT algorithm are studied beside the implication and conflict analysis on different representations, such as And-Inverter Graphs, Binary Decision Diagrams and Conjunctive Normal Forms. The finding all solution is computationally hard because it requires exponential time in the worst case. All efforts should be made to get the set of satisfying assignment in a concise form. The efficient implementation for minimal satisfying and justification assignments are studied. To prune the search space efficiently with solution assignments, a new blocking clause analysis is also proposed. To show the efficiency of proposed solution enumeration algorithm, SAT-based unbounded model checking and decision procedure for linear arithmetic constraints solving are implemented. Analytical and experimental studies demonstrate that the solution enumeration algorithm proposed in this thesis are efficient enough to apply to many applications. |
