QBF solvers implementing the QCDCL paradigm are powerful algorithms that
successfully tackle many computationally complex applications. However, our
theoretical understanding of the strength and limitations of these QCDCL
solvers is very limited.

In this paper we suggest to formally model QCDCL solvers as proof systems. We
define different policies that ... more >>>

We prove the equivalence of two fundamental problems in the theory of computation:

- Existence of one-way functions: the existence of one-way functions (which in turn are equivalent to pseudorandom generators, pseudorandom functions, private-key encryption schemes, digital signatures, commitment schemes, and more).

- Mild average-case hardness of $K^{poly}$-complexity: ... more >>>

Consider the following two fundamental open problems in complexity theory: (a) Does a hard-on-average language in $\NP$ imply the existence of one-way functions?, or (b) Does a hard-on-average language in NP imply a hard-on-average problem in TFNP (i.e., the class of total NP search problem)? Our main result is that ... more >>>