[Proof Complexity] Preprint - Pseudo proof systems and hard instances of SAT

[Jan Maly]

Dear all,

a preliminary version of my new paper with Moritz Muller, called "Pseudo 
proof systems and hard instances of SAT", is  available on my webpage: 
http://www.dbai.tuwien.ac.at/staff/jmaly/. Please find the abstract 
below and let us know if you have any comments.

All the best, Jan.

Abstract:

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. Speaking 
in standard terms, pseudo-proof systems are propositional proof systems 
that are unsound in the sense that they might prove some falsifiable 
propositional formulas but falsifying assignments are in a certain sense 
hard to find. A hard sequence for a sat-algorithm is, roughly, a 
feasibly computable sequence of satisfiable propositional formulas such 
that the algorithm needs superpolynomial time on them. We show that the 
existence of pseudo proof systems with a certain property that we call 
madness is equivalent to the existence of so-called probably hard 
sequences computable by certain randomized polynomial time algorithms. 
We discuss variants of hard sequences and survey the relevant literature.