Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > SATISFIABILITY:
Reports tagged with satisfiability:
TR00-010 | 12th January 2000
Amitabha Roy, Christopher Wilson

#### Supermodels and Closed Sets

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

TR00-028 | 17th April 2000
Lance Fortnow, Dieter van Melkebeek

#### Time-Space Tradeoffs for Nondeterministic Computation

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.

more >>>

TR00-082 | 17th August 2000
Lefteris Kirousis, Phokion G. Kolaitis

#### The Complexity of Minimal Satisfiability Problems

Revisions: 2

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

TR01-031 | 5th April 2001
Eli Ben-Sasson, Nicola Galesi

#### Space Complexity of Random Formulae in Resolution

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

TR01-079 | 6th September 2001
Michele Zito

#### An Upper Bound on the Space Complexity of Random Formulae in Resolution

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}})$.

more >>>

TR02-069 | 14th November 2002
Luca Trevisan

#### A Note on Deterministic Approximate Counting for k-DNF

Revisions: 1

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

TR03-003 | 19th December 2002
Fahiem Bacchus, Shannon Dalmao

#### DPLL with Caching: A new algorithm for #SAT and Bayesian Inference

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

TR03-007 | 15th January 2003
Olivier Dubois, Yacine Boufkhad, Jacques Mandler

#### Typical random 3-SAT formulae and the satisfiability threshold

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

TR03-010 | 13th February 2003
Sven Baumer, Rainer Schuler

#### Improving a probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs

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

TR03-022 | 11th April 2003
Piotr Berman, Marek Karpinski, Alexander D. Scott

#### Approximation Hardness and Satisfiability of Bounded Occurrence Instances of SAT

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

TR03-030 | 27th February 2003
Amin Coja-Oghlan, Andreas Goerdt, André Lanka, Frank Schädlich

#### Certifying Unsatisfiability of Random 2k-SAT Formulas using Approximation Techniques

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

TR04-111 | 30th November 2004
Piotr Berman, Marek Karpinski, Alexander D. Scott, Alexander D. Scott

#### Computational Complexity of Some Restricted Instances of 3SAT

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

more >>>

TR06-094 | 29th July 2006
Parikshit Gopalan, Phokion G. Kolaitis, Elitza Maneva, Christos H. Papadimitriou

#### The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies

Revisions: 1

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

TR07-036 | 6th April 2007
Ryan Williams

#### Time-Space Tradeoffs for Counting NP Solutions Modulo Integers

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

TR07-099 | 30th September 2007
Dieter van Melkebeek

#### A Survey of Lower Bounds for Satisfiability and Related Problems

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

TR07-126 | 5th November 2007
Nathan Segerlind

#### On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs

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

TR10-038 | 10th March 2010
Dieter van Melkebeek, Holger Dell

#### Satisfiability Allows No Nontrivial Sparsification Unless The Polynomial-Time Hierarchy Collapses

Revisions: 1

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

TR10-147 | 22nd September 2010
Dieter van Melkebeek, Thomas Watson

#### Time-Space Efficient Simulations of Quantum Computations

Revisions: 1

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

TR11-006 | 20th January 2011
Sebastian Müller, Iddo Tzameret

#### Average-Case Separation in Proof Complexity: Short Propositional Refutations for Random 3CNF Formulas

Revisions: 1

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

TR11-018 | 8th February 2011
Jochen Messner, Thomas Thierauf

#### A Kolmogorov Complexity Proof of the Lovász Local Lemma for Satisfiability

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.

more >>>

TR11-031 | 8th March 2011
Sam Buss, Ryan Williams

#### Limits on Alternation-Trading Proofs for Time-Space Lower Bounds

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

TR14-017 | 9th February 2014
Eli Ben-Sasson, Emanuele Viola

#### Short PCPs with projection queries

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

TR14-075 | 16th May 2014
Holger Dell

#### A simple proof that AND-compression of NP-complete problems is hard

Revisions: 3

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

TR15-101 | 15th June 2015
Patrick Scharpfenecker

#### On the structure of Solution-Graphs for Boolean Formulas

Revisions: 2

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

TR16-002 | 18th January 2016
Ryan Williams

#### Strong ETH Breaks With Merlin and Arthur: Short Non-Interactive Proofs of Batch Evaluation

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

TR16-022 | 22nd February 2016
Alexander Golovnev, Alexander Kulikov, Alexander Smal, Suguru Tamaki

#### Circuit size lower bounds and #SAT upper bounds through a general framework

Revisions: 2

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

TR17-188 | 22nd December 2017
Cody Murray, Ryan Williams

#### Circuit Lower Bounds for Nondeterministic Quasi-Polytime: An Easy Witness Lemma for NP and NQP

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

ISSN 1433-8092 | Imprint