Eli Ben-Sasson, Jakob Nordström

For current state-of-the-art satisfiability algorithms based on the

DPLL procedure and clause learning, the two main bottlenecks are the

amounts of time and memory used. Understanding time and memory

consumption, and how they are related to one another, is therefore a

question of considerable practical importance. In the field of ...
more >>>

Eli Ben-Sasson, Jakob Nordström

The k-DNF resolution proof systems are a family of systems indexed by

the integer k, where the kth member is restricted to operating with

formulas in disjunctive normal form with all terms of bounded arity k

(k-DNF formulas). This family was introduced in [Krajicek 2001] as an

extension of the ...
more >>>

Albert Atserias, Massimo Lauria, Jakob Nordström

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n^Omega(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. ... more >>>

Massimo Lauria, Jakob Nordström

We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size n^{Omega(d)} for values of d = d(n) from constant all the way up to n^{delta} for some universal constant delta. This shows that ... more >>>

Mladen Mikša, Jakob Nordström

We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good ... more >>>