28 problems

The iterated logarithm function is defined recursively by … For a positive integer $k$, $k$-SAT asks whether a Boolean formula with $n$ variables has a satisfying assignment. Stron…

Let $\mathcal{U}\mathcal{HIT}_{\!\delta=k}$ denote the class of unsatisfiable non-singular hitting clause-sets of deficiency $k$, where two different clauses clash in at least one…

Let $K$-SAT instances be represented as dilute spin-glass models, with a fictive temperature taken to $T\to0$ so that the ground-state entropy describes the logarithm of the number…

Strong Exponential-Time Hypothesis. No such algorithmic shortcuts exist for the general, unrestricted $K$-SAT problem.

The strong exponential time hypothesis concerns Boolean satisfiability. For an integer $k\geq 3$, let ${\sc k\text{-Sat}}$ denote the problem of deciding satisfiability of Boolean…

Let $\Sigma_1$ and $\Sigma_2$ be disjoint signatures, and let ${\mathcal{T}}_1$ and ${\mathcal{T}}_2$ be decidable theories over them. Let ${\mathcal{T}}_1\oplus{\mathcal{T}}_2$ be…

Let $\varphi$ be a [?]

Let $q$-CNFSAT denote the satisfiability problem for conjunctive normal form formulas whose clauses have at most $q$ literals, and let $n$ be the number of variables in the input f…

Restart usefulness conjecture. Restarts are useful for $texttt{Alfa}$ with $texttt{SLS} in { texttt{SRWA}, texttt{probSAT}, texttt{YalSAT} }$.

Weak Conjecture. The runtime of $texttt{Alfa}$ with $texttt{SLS} in { texttt{SRWA}, texttt{probSAT}, texttt{YalSAT} }$ is long-tailed.

Strong Conjecture. The runtime of $texttt{Alfa}$ with $texttt{SLS} in { texttt{SRWA}, texttt{probSAT}, texttt{YalSAT} }$ follows a Johnson SB distribution.

Johnson SB runtime conjecture. The runtimes of Alfa-type algorithms all follow a Johnson SB distribution, regardless of the problem domain.

Variable-occurrence conjecture. There is a variable $z \in \mathsf{var}(F)$ such that

Let a Boolean set theory formula be a formula in the variant $\textnormal{\textsf{BST}}\otimes$ of Boolean set theory with the unordered Cartesian product operator, and let the sat…

Solution-space shattering conjecture. The solution-space shattering brought by XORs might be the reason for the weakness of local-search solvers in handling XORs.

Exponential Time Hypothesis. There is no $2^{o(n)}$-time algorithm for textsc{3-SAT} on $n$-variable instances.

Let 3-SAT be the satisfiability problem for Boolean formulas in conjunctive normal form whose clauses have at most three literals. A problem is solvable in subexponential time if,…

Consider the planar 1-in-3 Satisfiability problem in which all variables lie inside a clause cycle, where the clause cycle connects all clauses in an arbitrary order, and the assoc…

For every $\varepsilon>0$, let $k_{\varepsilon}$ be an integer such that $k_{\varepsilon}$-SAT on $n$ variables cannot be solved in $O(2^{(1-\varepsilon)n})$ time. Strong Exponenti…

Linear Finiteness Conjecture. For $k\in\mathbb{N}$, $k\geq 2$,

Exact-variable Finiteness Conjecture. For every $k\in\mathbb{N}$,

Finiteness Conjecture. For every $k \in \mathbb{N}$, the number $n(F)$ of variables of an $F \in \Uclashns$ with $?=k$ is bounded.

Decidability conjecture. Satisfiability for $\mathsf{ECTL}^*$ with constraints over $\mathcal{T}_{\infty}$ is decidable.

Let $\mathcal{U}\mathcal{HIT}_{\!\delta=k}$ be the class of unsatisfiable hitting clause-sets of deficiency $k$. Let $\operatorname{singind}(F)$ denote the singular index of $F$, a…

Let $\vec\Phi=\vec\Phi_4(n,m)$ be a uniformly random 4-SAT formula with $n$ variables and $m$ clauses. Write $r=m/n$. The random 4-SAT threshold conjecture. The threshold for the e…