6 problems

Near-threshold resolution lower-bound conjecture. For an instance size $n$ with no solution, $n\notin S$, if

A hitting formula is a set of Boolean clauses such that no two clauses can be simultaneously falsified. A hitting formula is unsatisfiable when no Boolean assignment satisfies all…

Let $F$ range over unsatisfiable CNF formulas with $n$ variables, and let $p$ be a fixed polynomial. Consider the propositional formulas $\mathrm{REF}(F,p(n))$ expressing that $F$…

The Stone tautologies are propositional principles associated with the Stone tautologies studied in the cited resolution-complexity literature. A pool and regRTI lower-bound conjec…

Let $\{F_n\}_{n=1}^{\infty}$ be families of $k$-CNF formulas of size $\Theta(n)$. The total space of a resolution refutation of $F_n$ is denoted by $\operatorname{TotSp}(F_n)$. Ale…

Let a clause set have regular resolution width bounded below by a function of its parameters, and consider regular resolution refutations of that clause set. Width-to-size conjectu…