In this paper we ask the question whether the extended Frege proof
system EF satisfies a weak version of the deduction theorem. We
prove that if this is the case, then complete disjoint NP-pairs
exist. On the other hand, if EF is an optimal proof system, ... more >>>

We prove a strong inapproximability result for routing on directed
graphs with low congestion. Given as input a directed graph on $N$
vertices and a set of source-destination pairs that can be connected
via edge-disjoint paths, we prove that it is hard, assuming NP
doesn't have $n^{O(\log\log n)}$ time randomized ... more >>>

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