On Computing k-CNF Formula Properties

摘要: The latest generation of SAT solvers (e.g. [10,7]) generally have three key features: randomization variable selection, backtracking search, and some form clause learning. We present a simple algorithm with these features prove that for instances constant Δ (where is the clause-to-variable ratio) indeed has good worst-case performance, not only computing SAT/UNSAT but more general properties as well, such maximum satisfiability counting number satisfying assignments. In general, can determine any property computable via self-reductions on formula.