Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Nathan Segerlind:

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

TR07-107 | 26th October 2007
Nathan Segerlind

Exponential lower bounds and integrality gaps for tree-like Lovasz-Schrijver procedures

The matrix cuts of Lov{\'{a}}sz and Schrijver are methods for tightening linear relaxations of zero-one programs by the addition of new linear inequalities. We address the question of how many new inequalities are necessary to approximate certain combinatorial problems with strong guarantees, and to solve certain instances of Boolean satisfiability.

... more >>>

TR07-009 | 8th January 2007
Nathan Segerlind

Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability

Revisions: 1 , Comments: 1

We demonstrate a family of propositional formulas in conjunctive normal form
so that a formula of size $N$ requires size $2^{\Omega(\sqrt[7]{N/logN})}$
to refute using the tree-like OBDD refutation system of
Atserias, Kolaitis and Vardi
with respect to all variable orderings.
All known symbolic quantifier elimination algorithms for satisfiability
generate ... more >>>

TR06-140 | 8th November 2006
Paul Beame, Russell Impagliazzo, Nathan Segerlind

Formula Caching in DPLL

We consider extensions of the DPLL approach to satisfiability testing that add a version of memoization, in which formulas that the algorithm has previously shown to be unsatisfiable are remembered for later use. Such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability. We formalize these methods by ... more >>>

TR05-053 | 4th May 2005
Paul Beame, Nathan Segerlind

Lower bounds for Lovasz-Schrijver systems and beyond follow from multiparty communication complexity

We prove that an \omega(log^3 n) lower bound for the three-party number-on-the-forehead (NOF) communication complexity of the set-disjointness function implies an n^\omega(1) size lower bound for tree-like Lovasz-Schrijver systems that refute unsatisfiable CNFs. More generally, we prove that an n^\Omega(1) lower bound for the (k+1)-party NOF communication complexity of set-disjointness ... more >>>

ISSN 1433-8092 | Imprint