@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{DMV17,
  title={The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas},
  author={Dudek, Jeffrey and Meel, Kuldeep S. and Vardi, Moshe Y.},
  year={2017},
  booktitle=IJCAI,
  month=aug,
  bib2html_dl_pdf={../Papers/ijcai17.pdf},
  bib2html_pubtype={Refereed Conference},
  bib2html_rescat={Phase Transitions},
  abstract={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 constraintsints (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 \emph{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-solving algorithms.
  },
}