Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The ... more >>>

The classic Impagliazzo--Nisan--Wigderson (INW) psesudorandom generator (PRG) (STOC `94) for space-bounded computation uses a seed of length $O(\log n \cdot \log(nwd/\varepsilon))$ to fool ordered branching programs of length $n$, width $w$, and alphabet size $d$ to within error $\varepsilon$. A series of works have shown that the analysis of the ... more >>>

We introduce a new graph parameter called linear upper maximum induced
matching width \textsc{lu-mim width}, denoted for a graph $G$ by $lu(G)$.
We prove that the smallest size of the \textsc{obdd} for $\varphi$,
the monotone 2-\textsc{cnf} corresponding to $G$, is sandwiched
between $2^{lu(G)}$ and $n^{O(lu(G))}$.
The upper bound ... more >>>