code: def dpll_satisfiable(s):
      
      clauses = conjuncts(to_cnf(s))
      symbols = prop_symbols(s)
      return dpll(clauses, symbols, {})
docs: Check satisfiability of a propositional sentence.
      This differs from the book code in two ways: (1) it returns a model
      rather than True when it succeeds; this is more useful. (2) The
      function find_pure_symbol is passed a list of unknown clauses, rather
      than a list of all clauses and the model; this is more efficient.
      >>> ppsubst(dpll_satisfiable(A&~B))
      {A: True, B: False}
      >>> dpll_satisfiable(P&~P)
      False