Daniel Rolf

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 >>>

Michael Alekhnovich, Eli Ben-Sasson

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 >>>

Michael Alekhnovich, Edward Hirsch, Dmitry Itsykson

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 >>>

Albert Atserias

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 >>>

Parikshit Gopalan, Phokion G. Kolaitis, Elitza Maneva, Christos H. Papadimitriou

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 >>>

Eric Allender, Shiteng Chen, Tiancheng Lou, Periklis Papakonstantinou, Bangsheng Tang

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 >>>

Mikolas Janota, Joao Marques-Silva

Over the years, proof systems for propositional satisfiability (SAT)

have been extensively studied. Recently, proof systems for

quantified Boolean formulas (QBFs) have also been gaining attention.

Q-resolution is a calculus enabling producing proofs from

DPLL-based QBF solvers. While DPLL has become a dominating technique

for SAT, QBF has been tackled ...
more >>>

Joao Marques-Silva, Mikolas Janota

Propositional Satisfiability (SAT) solvers are routinely used for

solving many function problems.

A natural question that has seldom been addressed is: what is the

best worst-case number of calls to a SAT solver for solving some

target function problem?

This paper develops tighter upper bounds on the query complexity of

more >>>

Mikolas Janota, Leroy Chew, Olaf Beyersdorff

Several calculi for quantified Boolean formulas (QBFs) exist, but

relations between them are not yet fully understood.

This paper defines a novel calculus, which is resolution-based and

enables unification of the principal existing resolution-based QBF

calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based

calculus ...
more >>>

Ronald de Haan, Stefan Szeider

We present a list of parameterized problems together with a complexity classification of whether they allow a fixed-parameter tractable reduction to SAT or not. These parameterized problems are based on problems whose complexity lies at the second level of the Polynomial Hierarchy or higher. The list will be updated as ... more >>>

Dmitry Itsykson, Alexander Knop

Itsykson and Sokolov in 2014 introduced the class of DPLL($\oplus$) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of DPLL algorithms that split by variables. DPLL($\oplus$) algorithms solve in polynomial time systems of linear equations modulo two ... more >>>

Valentine Kabanets, Zhenjian Lu

A polynomial threshold function (PTF) is defined as the sign of a polynomial $p\colon\bool^n\to\mathbb{R}$. A PTF circuit is a Boolean circuit whose gates are PTFs. We study the problems of exact and (promise) approximate counting for PTF circuits of constant depth.

Satisfiability (#SAT). We give the first zero-error randomized algorithm ... more >>>