Contents

• About the Manual
• Conventions and Definitions
  • Conventions
  • Definitions
  
  
• Quick Start - Getting sbsat ready to run
  • Hardware Requirements
  • Getting SBSAT
  • Installing SBSAT
  • Compiling SBSAT
  • Testing SBSAT
  
  
• Quick Start - The basics of running SBSAT
  • Command line
  • A CNF formula as input
  • An input in canonical (BDD) form
  • An input in XOR format
  • Reusing functions (Macros)
  • Printing functions
  • An example of a complex canonical form input
  • Translating an expression to canonical form
  • Choosing a search procedure
  • Converting the input file
  
  
• Quick Start - Some advanced features of sbsat
  • Preprocessing
  • Heuristics
  • The lemma cache
  • Controlling preprocessing and search time
  • Creating and using an initialization file
  • Debugging
  
  
• Quick Start - Getting more help quickly
• Reference - Command line
  • General options
  • BDD table options
  • Input options
  • Output options
  • Preprocessing options
  • General solver options
  • SMURF Solver options
  • BDD WalkSAT solver options
  
  
• Reference - Initialization file
• Reference - Input formats
  • Canonical form
  • CNF format
  • DNF format
  • XOR format
  • Trace format
  • Prove format
  • SMURF format
  
  
• Reference - Preprocessing
  • Binary Decision Diagrams (BDDs)
  • Pattern Matching: CNF
  • Generalized Cofactor (GCF)
  • Branch Pruning
  • Strengthening
  • Inferences
  • Existential quantification
  • Clustering + Existential Quantification
  • Clustering + Existential Quantification + Safe
  • Dependent variable clustering
  • Rewind
  • Splitter
  • Universe
  
  
• Reference - Search heuristics
  • State Machines Used to Represent Functions (SMURFs)
  • Locally Skewed, Globally Balanced
  • Chaff-like
  • User defined search heuristic
  
  
• Reference - Search methods
  • Backtracking and Lemmas
  • BDD WalkSAT
  • WVF
  
  
• Reference - Output, results
  • Raw
  • Fancy
  
  
• Reference - Data structures
  • BDD database
  • SMURF
  • Lemma database
  
  
• Reference - Results: making BDDs from bmc
• Reference - Results: Experiments
• Reference - Debugging
  • Converting to another format
  • Printing internal forms
  
  
• Reference - Writing Exploitable Input