A remark on pseudo proof systems and hard instances of the satisfiability problem
Rights accessOpen Access
European Commission's projectAUTAR - A Unified Theory of Algorithmic Relaxations (EC-H2020-648276)
We link two concepts from the literature, namely hard sequences for the satisfiability problem sat and so-called pseudo proof systems proposed for study by Krajícek. Pseudo proof systems are elements of a particular nonstandard model constructed by forcing with random variables. We show that the existence of mad pseudo proof systems is equivalent to the existence of a randomized polynomial time procedure with a highly restrictive use of randomness which produces satisfiable formulas whose satisfying assignments are probably hard to find.
CitationMaly, J., Muller, M. A remark on pseudo proof systems and hard instances of the satisfiability problem. "Mathematical logic quarterly", 20 Novembre 2018, vol. 64, núm. 6, p. 418-428.