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

__
TR07-107
| 26th October 2007
__

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

__
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

__
TR06-140
| 8th November 2006
__

Paul Beame, Russell Impagliazzo, Nathan Segerlind#### Formula Caching in DPLL

__
TR05-053
| 4th May 2005
__

Paul Beame, Nathan Segerlind#### Lower bounds for Lovasz-Schrijver systems and beyond follow from multiparty communication complexity

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

Nathan Segerlind

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

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

Paul Beame, Russell Impagliazzo, Nathan Segerlind

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

Paul Beame, Nathan Segerlind

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