Amitabha Roy, Christopher Wilson

A {\em supermodel} is a satisfying assignment of a boolean formula

for which any small alteration, such as a single bit flip, can be

repaired by another small alteration, yielding a nearby

satisfying assignment. We study computational problems associated

with super models and some generalizations thereof. For general

formulas, ...
more >>>

Lance Fortnow, Dieter van Melkebeek

We show new tradeoffs for satisfiability and nondeterministic

linear time. Satisfiability cannot be solved on general purpose

random-access Turing machines in time $n^{1.618}$ and space

$n^{o(1)}$. This improves recent results of Lipton and Viglas and

Fortnow.

Lefteris Kirousis, Phokion G. Kolaitis

A dichotomy theorem for a class of decision problems is

a result asserting that certain problems in the class

are solvable in polynomial time, while the rest are NP-complete.

The first remarkable such dichotomy theorem was proved by

T.J. Schaefer in 1978. It concerns the ...
more >>>

Eli Ben-Sasson, Nicola Galesi

We study the space complexity of refuting unsatisfiable random $k$-CNFs in

the Resolution proof system. We prove that for any large enough $\Delta$,

with high probability a random $k$-CNF over $n$ variables and $\Delta n$

clauses requires resolution clause space of

$\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$,

for any $0<\epsilon<1/2$. For constant $\Delta$, ...
more >>>

Michele Zito

We prove that, with high probability, the space complexity of refuting

a random unsatisfiable boolean formula in $k$-CNF on $n$

variables and $m = \Delta n$ clauses is

$O(n \cdot \Delta^{-\frac{1}{k-2}})$.

Luca Trevisan

We describe a deterministic algorithm that, for constant k,

given a k-DNF or k-CNF formula f and a parameter e, runs in time

linear in the size of f and polynomial in 1/e and returns an

estimate of the fraction of satisfying assignments for f up to ...
more >>>

Fahiem Bacchus, Shannon Dalmao

Bayesian inference and counting satisfying assignments are important

problems with numerous applications in probabilistic reasoning. In this

paper, we show that plain old DPLL equipped with memoization can solve

both of these problems with time complexity that is at least as

good as all known algorithms. Furthermore, DPLL with memoization

more >>>

Olivier Dubois, Yacine Boufkhad, Jacques Mandler

$k$-SAT is one of the best known among a wide class of random

constraint satisfaction problems believed to exhibit a threshold

phenomenon where the control parameter is the ratio, number of

constraints to number of variables. There has been a large amount of

work towards estimating ...
more >>>

Sven Baumer, Rainer Schuler

The satisfiability problem of Boolean Formulae in 3-CNF (3-SAT)

is a well known NP-complete problem and the development of faster

(moderately exponential time) algorithms has received much interest

in recent years. We show that the 3-SAT problem can be solved by a

probabilistic algorithm in expected time O(1,3290^n).

more >>>

Piotr Berman, Marek Karpinski, Alexander D. Scott

We study approximation hardness and satisfiability of bounded

occurrence uniform instances of SAT. Among other things, we prove

the inapproximability for SAT instances in which every clause has

exactly 3 literals and each variable occurs exactly 4 times,

and display an explicit ...
more >>>

Amin Coja-Oghlan, Andreas Goerdt, André Lanka, Frank Schädlich

Abstract. It is known that random k-SAT formulas with at least

(2^k*ln2)*n random clauses are unsatisfiable with high probability. This

result is simply obtained by bounding the expected number of satisfy-

ing assignments of a random k-SAT instance by an expression tending

to 0 when n, the number of variables ...
more >>>

Piotr Berman, Marek Karpinski, Alexander D. Scott, Alexander D. Scott

We prove results on the computational complexity of instances of 3SAT in which every variable occurs 3 or 4 times.

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

Ryan Williams

We prove the first time-space tradeoffs for counting the number of solutions to an NP problem modulo small integers, and also improve upon the known time-space tradeoffs for Sat. Let m be a positive integer, and define MODm-Sat to be the problem of determining if a given Boolean formula has ... more >>>

Dieter van Melkebeek

Ever since the fundamental work of Cook from 1971, satisfiability has been recognized as a central problem in computational complexity. It is widely believed to be intractable, and yet till recently even a linear-time, logarithmic-space algorithm for satisfiability was not ruled out. In 1997 Fortnow, building on earlier work by ... more >>>

Nathan Segerlind

We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The ``OBDD proof ... more >>>

Dieter van Melkebeek, Holger Dell

Consider the following two-player communication process to decide a language $L$: The first player holds the entire input $x$ but is polynomially bounded; the second player is computationally unbounded but does not know any part of $x$; their goal is to cooperatively decide whether $x$ belongs to $L$ at small ... more >>>

Dieter van Melkebeek, Thomas Watson

We give two time- and space-efficient simulations of quantum computations with

intermediate measurements, one by classical randomized computations with

unbounded error and the other by quantum computations that use an arbitrary

fixed universal set of gates. Specifically, our simulations show that every

language solvable by a bounded-error quantum algorithm running ...
more >>>

Sebastian Müller, Iddo Tzameret

Separating different propositional proof systems---that is, demonstrating that one proof system cannot efficiently simulate another proof system---is one of the main goals of proof complexity. Nevertheless, all known separation results between non-abstract proof systems are for specific families of hard tautologies: for what we know, in the average case all ... more >>>

Jochen Messner, Thomas Thierauf

Recently, Moser and Tardos [MT10] came up with a constructive proof of the Lovász Local Lemma. In this paper, we give another constructive proof of the lemma, based on Kolmogorov complexity. Actually, we even improve the Local Lemma slightly.

Sam Buss, Ryan Williams

This paper characterizes alternation trading based proofs that satisfiability is not in the time and space bounded class $\DTISP(n^c, n^\epsilon)$, for various values $c<2$ and $\epsilon<1$. We characterize exactly what can be proved in the $\epsilon=0$ case with currently known methods, and prove the conjecture of Williams that $c=2\cos(\pi/7)$ is ... more >>>

Eli Ben-Sasson, Emanuele Viola

We construct a PCP for NTIME(2$^n$) with constant

soundness, $2^n \poly(n)$ proof length, and $\poly(n)$

queries where the verifier's computation is simple: the

queries are a projection of the input randomness, and the

computation on the prover's answers is a 3CNF. The

previous upper bound for these two computations was

more >>>

Holger Dell

Drucker (2012) proved the following result: Unless the unlikely complexity-theoretic collapse coNP is in NP/poly occurs, there is no AND-compression for SAT. The result has implications for the compressibility and kernelizability of a whole range of NP-complete parameterized problems. We present a simple proof of this result.

An AND-compression is ... more >>>

Patrick Scharpfenecker

In this work we extend the study of solution graphs and prove that for boolean formulas in a class called CPSS, all connected components are partial cubes of small dimension, a statement which was proved only for some cases in [Schwerdtfeger 2013]. In contrast, we show that general Schaefer formulas ... more >>>

Ryan Williams

We present an efficient proof system for Multipoint Arithmetic Circuit Evaluation: for every arithmetic circuit $C(x_1,\ldots,x_n)$ of size $s$ and degree $d$ over a field ${\mathbb F}$, and any inputs $a_1,\ldots,a_K \in {\mathbb F}^n$,

$\bullet$ the Prover sends the Verifier the values $C(a_1), \ldots, C(a_K) \in {\mathbb F}$ and ...
more >>>

Alexander Golovnev, Alexander Kulikov, Alexander Smal, Suguru Tamaki

Most of the known lower bounds for binary Boolean circuits with unrestricted depth are proved by the gate elimination method. The most efficient known algorithms for the #SAT problem on binary Boolean circuits use similar case analyses to the ones in gate elimination. Chen and Kabanets recently showed that the ... more >>>

Cody Murray, Ryan Williams

We prove that if every problem in $NP$ has $n^k$-size circuits for a fixed constant $k$, then for every $NP$-verifier and every yes-instance $x$ of length $n$ for that verifier, the verifier's search space has an $n^{O(k^3)}$-size witness circuit: a witness for $x$ that can be encoded with a circuit ... more >>>