A Survey of Satisfiability Modulo Theory <s> Let F <s> Abstract We prove that, for infinitely many disjunctive normal form propositional calculus tautologies ξ, the length of the shortest resolution proof of ξ cannot be bounded by any polynomial of the length of ξ. The tautologies we use were introduced by Cook and Reckhow (1979) and encode the pigeonhole principle. Extended resolution can furnish polynomial length proofs of these formulas. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Let F <s> Boolean satisfiability is probably the most studied of the combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in electronic design automation (EDA), as well as in artificial intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff which achieves significant performance gains through careful engineering of all aspects of the search-especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on difficult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO. <s> BIB002 </s> A Survey of Satisfiability Modulo Theory <s> Let F <s> A method and apparatus for managing power consumption in a computer system wherein the method and apparatus is compliant with the proposed Advanced Configuration and Power Interface (ACPI) specification. In one embodiment, a power management processor is sandwiched between platform hardware and the ACPI register layer. The processor processes all operating power management commands and requests while remaining transparent to the user and the operating system. In so doing, routine power management functions, so classified by the operating system, are implemented by the operating system. Sophisticated power management features, on the other hand, are implemented by the present invention independent from operating system control. Accordingly, in the present invention, the operating system need not suspend processing of other threads to process sophisticated power management procedures. <s> BIB003 </s> A Survey of Satisfiability Modulo Theory <s> Let F <s> We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers. <s> BIB004 </s> A Survey of Satisfiability Modulo Theory <s> Let F <s> When checking answers coming from automatic provers, or when skeptically integrating them into proof assistants, a major problem is the wide variety of formats of certicates, which forces to write lots of dierent checkers. In this paper, we propose to use the extended resolution as a common format for every propositional prover. To be able to do this, we detail two algorithms transforming proofs computed respectively by tableaux provers and provers based on BDDs into this format. Since this latter is already implemented for SAT solvers, it is now possible for the three most common propositional provers to share the same certicates. <s> BIB005
′ be the conjunction of clauses forming the problem. The DavisPutnam-Logemann-Loveland algorithm (DPLL) decides a propositional formula in CNF (conjunction of clauses) by maintaining a partial assignment of the variables (that is, an assignment to only some of the variables) and Boolean constraint propagation: if we have assigned a = f , b = t and we have a clause a ∨ ¬b ∨ c, then we can derive c = t. If an assignment satisfies all clauses, then the algorithm terminates with one solution. If it falsifies at least one clause, then there is no solution for our starting partial assignment (thus no solution at all if our starting partial assignment was empty). If propagation is insufficient to conclude, then the algorithm chooses a variable x and a true value b and extends the assignment with x = b; if no solution is found for that assignment, then it backtracks and replaces it by x =b. The solver thus constructs a search tree. The practical performance of the solver depends highly on the heuristics for choosing x and b. Much effort has been put into researching these heuristics, such as Variable State Independent Decaying Sum (VSIDS) BIB002 ; understanding why they work well is an active research topic. The Boolean constraint propagation phase must be implemented very efficiently, using data structures that minimize the traversal of irrelevant data (clauses that will not result in further propagation); e.g. the two watched literals per clause scheme [47, §4.5. From a run of the DPLL algorithm concluding to unsatisfiability one can extract a resolution proof of unsatisfiability. The proof has the form of a tree whose leaves are some of the original clauses of the problem (constituting an unsatisfiable core) and whose inner nodes correspond to the choices made during the search. Each inner node is the application of the resolution rule: knowing C 1 ∨ a and C 2 ∨ā, where C 1 and C 2 are clauses and a is a choice variable, one can derive C 1 ∨ C 2 , written: Example 3. Consider the system of clauses 7. Boolean clause propagation from unit clause φ simplifiesφ ∨ g andφ ∨ h into g and h respectively, and removes clauseḡ ∨h ∨ φ. Since g and h are now t, we can remove clausesē ∨ g and f ∨ g, b ∨ h, and c ∨ h, and simplifyḡ ∨ e ∨ f into e ∨ f andh ∨b ∨c intob ∨c: The system no longer has unit clauses to propagate and thus must pick a literal, for instance b. By propagation, the system now reaches a contradiction. Since contradiction was reached from assumption b, the converseb must be assumed. In fact, it is possible to derive the learned clauseb by resolution from the set of clauses: From any "unsatisfiable" run of a DPLL (even in the CDCL variant, see below) solver, a resolution proof can be extracted. This is a fundamental limitation of that approach, since it is known that for certain families of formulas, such as the pigeonhole principle BIB001 , any resolution proof has exponential size in the size of the formula -thus any DPLL/CDCL solver will take exponential time. Performance was considerably increased by extending DPLL with clause learning, yielding constraint-driven clause learning (CDCL) algorithms BIB003 . In CDCL, when a partial assignments leads by propagation to the falsification of a clause, the deductions made during this propagation are analyzed to obtain a subset of the partial assignment sufficient to entail the falsification of this clause. This subset yields a conjunctionx 1 ∧ · · · ∧x n (wherex i is either x i or ¬x i ), such that its conjunction with F ′ is unsatisfiable. In other words, it yields a clause ¬x 1 ∨ · · · ∨ ¬x n that is a consequence of F ′ (in fact, that clause can be obtained by resolution from F ′ ). This clause can thus be conjoined to the problem F ′ without changing its set of solutions; but learning that clause may help cut branches in the search tree early. Again, the learned clause appears as the root of a resolution proof whose leaves are clauses of the original problem. Since the same learned clause may be used several times, the final proof appears as a directed acyclic graph (DAG, i.e., a tree with shared sub-branches). There exist formulas admitting DAG resolution proofs exponentially shorter than the smallest tree resolution proof  . A resolution proof, or a more compact format, may thus be produced during an "unsatisfiable" run. A highly optimized SAT or SMT solver is likely to contain bugs, so it may be desirable to have an independent, simpler, possibly formally verified checker reprocess such as proof BIB004  BIB005 ].