This paper establishes a randomized algorithm that finds a satisfying assignment for a satisfiable formula $F$ in 3-CNF in $O(1.32793^n)$ expected running time. The algorithms is based on the analysis of so-called strings, which are sequences of 3-clauses where non-succeeding clauses do not share a variable and succeeding clauses share ... more >>>

We analyze the efficiency of the random walk algorithm on random 3CNF instances, and prove em linear upper bounds on the running time
of this algorithm for small clause density, less than 1.63. Our upper bound matches the observed running time to within a multiplicative factor. This is the ... more >>>

DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satisfiability problem) and are widely used in applications. The recursion trees of DPLL algorithm executions on unsatisfiable formulas are equivalent to tree-like resolution proofs. Therefore, lower bounds for tree-like resolution (which ... more >>>

We may believe SAT does not have small Boolean circuits.
But is it possible that some language with small circuits
looks indistiguishable from SAT to every polynomial-time
bounded adversary? We rule out this possibility. More
precisely, assuming SAT does not have small circuits, we
show that ... more >>>

Boolean satisfiability problems are an important benchmark for questions about complexity, algorithms, heuristics and threshold phenomena. Recent work on heuristics, and the satisfiability threshold has centered around the structure and connectivity of the solution space. Motivated by this work, we study structural and connectivity-related properties of the space of solutions ... more >>>

A decade has passed since Alekhnovich and Razborov presented an algorithm that solves SAT on instances $\phi$ of size $n$ having tree-width $TW(\phi)$, using time (and space) bounded by $2^{O(TW(\phi))}n^{O(1)}$. Although there have been several papers over the ensuing years building on the work of Alekhnovich and Razborov there has ... more >>>