资源描述：
《a proof complexity generatornew》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、AproofcomplexitygeneratorJanKrajcekyAcademyofSciencesandCharlesUniversity,PragueAbstractWede neamapg:f0;1gn!f0;1gn+1suchthatalloutputbitsarede nedby2DNFformulasintheinputbits,andsuchthatghasthefol-lowinghardnessproperty.Foranyb2f0;1gn+1nRng(g),formula (g
2、)bnaturallyexpressingthatb2=Rng(g)requiresexponentialsizeproofsinanyproofsystemforwhichthepigeonholeprincipleisexponentiallyhard.Wede neaclassofgeneratorsgeneralizinggandshowthatthereisauniversaloneinthisclass.Consideramapg:x2f0;1gn!y2f0;1gmde nedbycondition
3、syi'i(x)where'i(x)arepropositionalformulasinx=(x1;:::;xn)andm>n.Asthedomainofgissmallerthanf0;1gmthereareb2f0;1gmnRng(g).Foranysuchbtheformula (g)b(x):_bi6'i(x)i2[m]expressesthatb2=Rng(g)inthesensethat (g)bisatautologyi b2=Rng(g).Ouraimistode negforwhichth
4、e -formulasarehardtoprove.Whenall (g)brequiresuper-polynomial(resp.exponential)sizeproofsinaproofsystemPwesay(following[22])thatgishard(resp.exponentiallyhard)proofcomplexitygeneratorforP.The -formulashavebeende nedin[7]andindependentlyin[2],andtheirtheoryis
5、beingdeveloped(see[8,21,9,22,10,11,14]);theintroductionsto[9]or[22]o eramorecomprehensiveexposition.Theproperty"b2=Rng(g)"canbeexpressedbyatautologyevenformapsgwithoutputbitsde nedbynon-uniformNPcoNPconditionsontheinputbits.SuchageneralityallowedRazborov[22
6、]toformulateanintriguingconjectureaboutExtendedFregesystemEF(seealso[10]).Wedonotneedsuchageneralityhere.Keywords:propositionalproofcomplexity,pigeonholeprinciple.yPartiallysupportedinpartbygrantsA1019401,AV0Z10190503,MSM0021620839,201/05/0124,andLC505.1The
7、mapgwede neisexponentiallyhardforproofsystemsforwhichthepigeonholeprincipleisexponentiallyhard.Thisincludes,forexample,constantdepthFregesystemsFd,polynomialcalculusPCorthesystemfrom[5]combiningthetwo.Finallyweshowthatinaclassofgeneratorsgeneralizingg,wecall
8、themgadgetgenerators,thereisauniversalone.ExponentiallyhardgeneratorswerepreviouslyconstructedforresolutionR(see[9,Thm.4.2]and[22,Thms.2.10,2.20]).Mapsyieldinghard -formulasforpolynomialcalculus
