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

Jan Maly jmaly at dbai.tuwien.ac.at
Fri Feb 3 12:24:54 CET 2017

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.


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.

More information about the Proof-Complexity mailing list