This paper presents a symbolic model checking technique that replaces BDDs with boolean decision procedures such as Stålmarck's Method or the Davis & Putnam Procedure. The new approach avoids the space explosion of BDDs, generates counterexamples faster, and can sometimes speed up verification. It also produces counterexamples of minimal length. The authors introduce a bounded model checking procedure for LTL that reduces model checking to propositional satisfiability. They show that bounded LTL model checking can be done without a tableau construction. A model checker BMC based on bounded model checking is implemented, and preliminary results are presented. Model checking is a powerful technique for verifying reactive systems. It is gaining wide industrial acceptance due to its ability to find subtle errors in real commercial designs. Compared to other formal verification techniques, model checking is largely automatic. In model checking, the specification is expressed in temporal logic and the system is modeled as a finite state machine. For realistic designs, the number of states can be very large, making explicit state traversal infeasible. Symbolic model checking with boolean encoding can handle more than 10^20 states. BDDs, a canonical form for boolean expressions, have traditionally been used as the underlying representation for symbolic model checkers. However, for larger systems, BDDs become too large for currently available computers. Propositional decision procedures (SAT) also operate on boolean expressions but do not use canonical forms. They do not suffer from the potential space explosion of BDDs and can handle propositional satisfiability problems with thousands of variables. SAT-based techniques have been successfully applied in various domains, including hardware verification, modal logics, formal verification of railway control systems, and AI planning systems. The paper introduces a symbolic model checking technique based on SAT procedures. The basic idea is to consider counterexamples of a particular length k and generate a propositional formula that is satisfiable iff such a counterexample exists. The authors show that bounded model checking for LTL can be reduced to propositional satisfiability in polynomial time. They establish a correspondence between bounded model checking and general model checking. Unlike previous approaches to LTL model checking, their method does not require a tableau or automaton construction. The main advantages of their technique are: (1) bounded model checking finds counterexamples very fast due to the depth-first nature of SAT search procedures. (2) It finds counterexamples of minimal length, which helps users understand counterexamples more easily. (3) Bounded model checking uses much less space than BDD-based approaches. (4) Unlike BDD-based approaches, bounded model checking does not need a manually selected variable order or time-consuming dynamic reordering. Default splitting heuristics are usually sufficient. The authors implemented a tool BMC based on bounded model checking and presented examples where SAT-based model checking significantly outperforms BDD-based model checking. In some cases, bounded model checking detects errors instantly, while BDDs for the initial state cannotThis paper presents a symbolic model checking technique that replaces BDDs with boolean decision procedures such as Stålmarck's Method or the Davis & Putnam Procedure. The new approach avoids the space explosion of BDDs, generates counterexamples faster, and can sometimes speed up verification. It also produces counterexamples of minimal length. The authors introduce a bounded model checking procedure for LTL that reduces model checking to propositional satisfiability. They show that bounded LTL model checking can be done without a tableau construction. A model checker BMC based on bounded model checking is implemented, and preliminary results are presented. Model checking is a powerful technique for verifying reactive systems. It is gaining wide industrial acceptance due to its ability to find subtle errors in real commercial designs. Compared to other formal verification techniques, model checking is largely automatic. In model checking, the specification is expressed in temporal logic and the system is modeled as a finite state machine. For realistic designs, the number of states can be very large, making explicit state traversal infeasible. Symbolic model checking with boolean encoding can handle more than 10^20 states. BDDs, a canonical form for boolean expressions, have traditionally been used as the underlying representation for symbolic model checkers. However, for larger systems, BDDs become too large for currently available computers. Propositional decision procedures (SAT) also operate on boolean expressions but do not use canonical forms. They do not suffer from the potential space explosion of BDDs and can handle propositional satisfiability problems with thousands of variables. SAT-based techniques have been successfully applied in various domains, including hardware verification, modal logics, formal verification of railway control systems, and AI planning systems. The paper introduces a symbolic model checking technique based on SAT procedures. The basic idea is to consider counterexamples of a particular length k and generate a propositional formula that is satisfiable iff such a counterexample exists. The authors show that bounded model checking for LTL can be reduced to propositional satisfiability in polynomial time. They establish a correspondence between bounded model checking and general model checking. Unlike previous approaches to LTL model checking, their method does not require a tableau or automaton construction. The main advantages of their technique are: (1) bounded model checking finds counterexamples very fast due to the depth-first nature of SAT search procedures. (2) It finds counterexamples of minimal length, which helps users understand counterexamples more easily. (3) Bounded model checking uses much less space than BDD-based approaches. (4) Unlike BDD-based approaches, bounded model checking does not need a manually selected variable order or time-consuming dynamic reordering. Default splitting heuristics are usually sufficient. The authors implemented a tool BMC based on bounded model checking and presented examples where SAT-based model checking significantly outperforms BDD-based model checking. In some cases, bounded model checking detects errors instantly, while BDDs for the initial state cannot