{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T19:56:11Z","timestamp":1783972571961,"version":"3.55.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,8]]},"abstract":"<jats:p>Recent universal-hashing based approaches to sampling and counting crucially depend on the runtime performance of SAT solvers on formulas expressed as the conjunction of both CNF constraints and variable-width XOR constraints (known as CNF-XOR formulas). In this paper, we present the first study of the runtime behavior of SAT solvers equipped with XOR-reasoning techniques on random CNF-XOR formulas. We empirically demonstrate that a state-of-the-art SAT solver scales exponentially on random CNF-XOR formulas across a wide range of XOR-clause densities, peaking around the empirical phase-transition location. On the theoretical front, we prove that the solution space of a random CNF-XOR formula 'shatters' at all nonzero XOR-clause densities into well-separated components, similar to the behavior seen in random CNF formulas known to be difficult for many SAT algorithms.<\/jats:p>","DOI":"10.24963\/ijcai.2017\/84","type":"proceedings-article","created":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T09:14:07Z","timestamp":1501233247000},"page":"600-606","source":"Crossref","is-referenced-by-count":11,"title":["The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas"],"prefix":"10.24963","author":[{"given":"Jeffrey M.","family":"Dudek","sequence":"first","affiliation":[{"name":"Rice University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[{"name":"Rice University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe","family":"Y. Vardi","sequence":"additional","affiliation":[{"name":"Rice University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"10584","event":{"name":"Twenty-Sixth International Joint Conference on Artificial Intelligence","theme":"Artificial Intelligence","location":"Melbourne, Australia","acronym":"IJCAI-2017","number":"26","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)","University of Technology Sydney (UTS)","Australian Computer Society (ACS)"],"start":{"date-parts":[[2017,8,19]]},"end":{"date-parts":[[2017,8,26]]}},"container-title":["Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T11:52:10Z","timestamp":1501242730000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2017\/84"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2017,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2017\/84","relation":{},"subject":[],"published":{"date-parts":[[2017,8]]}}}