Lower Bounds for QCDCL via Formula Gauge

Lower Bounds for QCDCL via Formula Gauge | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article Lower Bounds for QCDCL via Formula Gauge Benjamin Böhm, Olaf Beyersdorff This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-1796853/v1 This work is licensed under a CC BY 4.0 License Status: Published Journal Publication published 27 Sep, 2023 Read the published version in Journal of Automated Reasoning → Version 1 posted 7 You are reading this latest preprint version Abstract QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). We design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call gauge. We show that for a large class of QBFs, large (e.g. linear) gauge implies exponential lower bounds for QCDCL proof size. We illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL. QBF QCDCL proof complexity resolution lower bounds Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Published Journal Publication published 27 Sep, 2023 Read the published version in Journal of Automated Reasoning → Version 1 posted Editorial decision: Major revision 24 Jan, 2023 Reviews received at journal 19 Sep, 2022 Reviewers agreed at journal 13 Jul, 2022 Reviewers invited by journal 12 Jul, 2022 Editor assigned by journal 28 Jun, 2022 Submission checks completed at journal 28 Jun, 2022 First submitted to journal 26 Jun, 2022 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-1796853","acceptedTermsAndConditions":true,"allowDirectSubmit":false,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":116901683,"identity":"03c4a206-4177-4cdf-994a-7f82e2846586","order_by":0,"name":"Benjamin Böhm","email":"","orcid":"","institution":"Friedrich Schiller University Jena","correspondingAuthor":false,"submittingAuthor":false,"prefix":"","firstName":"Benjamin","middleName":"","lastName":"Böhm","suffix":""},{"id":116901684,"identity":"c5662c62-b5ec-4d47-961f-e68b3f92ea74","order_by":1,"name":"Olaf Beyersdorff","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAABL0lEQVRIie2RvWrDMBRGrzDYi0CrTNo+g4rBoRBS+iYRgUxuoHgvAoOzmGZ1lvYV7C1DoSoesugBPMZLpg7O1iGQyu7QH0ShW6E6k3TF4fsuArBY/iIeQIvE+5kCnBGiDxJwP2BGxQGUf1ICfyV+rRTy49GoEMdpBFqP+HKwaer9I6NBff0s4WQ0J8IptwbFT9xzgdSMr+6i4CLfMRrW84kuNoupdGNTDKtguEVpxQuF3QGWh9uwjlh1wBUXEofUqHh7gdIjf1LeTiu6WB4xnXLkDxIPX40K1sVSyQsMYa8w2it6olNM6/sJvhFcTYNcYb2LVqh66ZQpLys3NhUj3qIU+/X4dJl5Td1qhSyioEXZmN9vkrI1xXRMAK7ElwnKoPuyH7n8djftbbFYLP+VN0IPZ8jWS5j1AAAAAElFTkSuQmCC","orcid":"","institution":"Friedrich Schiller University Jena","correspondingAuthor":true,"submittingAuthor":false,"prefix":"","firstName":"Olaf","middleName":"","lastName":"Beyersdorff","suffix":""}],"badges":[],"createdAt":"2022-06-26 14:14:08","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-1796853/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-1796853/v1","draftVersion":[],"editorialEvents":[{"content":"https://doi.org/10.1007/s10817-023-09683-1","type":"published","date":"2023-09-27T15:01:57+00:00"}],"editorialNote":"","failedWorkflow":false,"files":[{"id":23524130,"identity":"fc7d7d6d-3922-466f-be97-1f8b7cc79fcd","added_by":"auto","created_at":"2022-07-06 14:24:58","extension":"pdf","order_by":0,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":677359,"visible":true,"origin":"","legend":"","description":"","filename":"upload.pdf","url":"https://assets-eu.researchsquare.com/files/rs-1796853/v1_covered.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"Lower Bounds for QCDCL via Formula Gauge","fulltext":[{"header":"Full Text","content":"This preprint is available for \u003ca href='/article/rs-1796853/latest.pdf' target='_blank'\u003edownload as a PDF\u003c/a\u003e."}],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":false,"highlight":"","institution":"","isAcceptedByJournal":true,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":false,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"journal-of-automated-reasoning","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"jars","sideBox":"Learn more about [Journal of Automated Reasoning](http://link.springer.com/journal/10817)","snPcode":"10817","submissionUrl":"https://submission.nature.com/new-submission/10817/3","title":"Journal of Automated Reasoning","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false},"keywords":"QBF, QCDCL, proof complexity, resolution, lower bounds","lastPublishedDoi":"10.21203/rs.3.rs-1796853/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-1796853/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). \nWe design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call gauge. We show that for a large class of QBFs, large (e.g. linear) gauge implies exponential lower bounds for QCDCL proof size. \nWe illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL.","manuscriptTitle":"Lower Bounds for QCDCL via Formula Gauge","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2022-07-06 14:24:49","doi":"10.21203/rs.3.rs-1796853/v1","editorialEvents":[{"type":"communityComments","content":0},{"type":"decision","content":"Major revision","date":"2023-01-24T15:57:13+00:00","index":"","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2022-09-19T10:22:21+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"7f23ba5a-6e1a-4bdd-93bc-2e0c60c6071d","date":"2022-07-13T08:34:55+00:00","index":"hide","fulltext":""},{"type":"reviewersInvited","content":"","date":"2022-07-12T18:41:49+00:00","index":"","fulltext":""},{"type":"editorAssigned","content":"","date":"2022-06-28T06:34:34+00:00","index":"","fulltext":""},{"type":"checksComplete","content":"","date":"2022-06-28T06:34:33+00:00","index":"","fulltext":""},{"type":"submitted","content":"Journal of Automated Reasoning","date":"2022-06-26T14:02:14+00:00","index":"","fulltext":""}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"journal-of-automated-reasoning","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"jars","sideBox":"Learn more about [Journal of Automated Reasoning](http://link.springer.com/journal/10817)","snPcode":"10817","submissionUrl":"https://submission.nature.com/new-submission/10817/3","title":"Journal of Automated Reasoning","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false}}],"origin":"","ownerIdentity":"04aaac82-bc4b-4bf6-a785-d07f9af2983d","owner":[],"postedDate":"July 6th, 2022","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"published-in-journal","subjectAreas":[],"tags":[],"updatedAt":"2023-10-02T15:07:12+00:00","versionOfRecord":{"articleIdentity":"rs-1796853","link":"https://doi.org/10.1007/s10817-023-09683-1","journal":{"identity":"journal-of-automated-reasoning","isVorOnly":false,"title":"Journal of Automated Reasoning"},"publishedOn":"2023-09-27 15:01:57","publishedOnDateReadable":"September 27th, 2023"},"versionCreatedAt":"2022-07-06 14:24:49","video":"","vorDoi":"10.1007/s10817-023-09683-1","vorDoiUrl":"https://doi.org/10.1007/s10817-023-09683-1","workflowStages":[]},"version":"v1","identity":"rs-1796853","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-1796853","identity":"rs-1796853","version":["v1"]},"buildId":"cBFmMYwuxLRRLfASyISRj","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}