@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/
@article{IMMV16,
  title={
    On Computing Minimal Independent Support and Its Applications to Sampling
    and Counting
  },
  bib2html_dl_pdf={../Papers/constraints16.pdf},
  code={https://bitbucket.org/kuldeepmeel/mis},
  author={
    Ivrii, Alexander and Malik, Sharad and Meel, Kuldeep S. and Vardi, Moshe Y.
  },
  journal={Constraints},
  volume={21},
  number={1},
  month=sep,
  year={2016},
  bib2html_rescat={Counting,Sampling},
  bib2html_pubtype={Journal},
  abstract={
    Constrained sampling and counting are two fundamental problems arising in
    domains ranging from artificial intelligence and security, to hardware and
    software testing. Recent approaches to approximate solutions for these
    problems rely on employing SAT solvers and universal hash functions that are
    typically encoded as XOR constraints of length n/2 for an input formula with
    n variables. As the runtime performance of SAT solvers heavily depends on
    the length of XOR constraints, recent research effort has been focused on
    reduction of length of XOR constraints. Consequently, a notion of
    Independent Support was proposed, and it was shown that constructing XORs
    over independent support (if known) can lead to a significant reduction in
    the length of XOR constraints without losing the theoretical guarantees of
    sampling and counting algorithms. In this paper, we present the first
    algorithmic procedure (and a corresponding tool, called MIS) to determine
    minimal independent support for a given CNF formula by employing a reduction
    to group minimal unsatisfiable subsets (GMUS). By utilizing minimal
    independent supports computed by MIS, we provide new tighter bounds on the
    length of XOR constraints for constrained counting and sampling.
    Furthermore, the universal hash functions constructed from independent
    supports computed by MIS provide two to three orders of magnitude
    performance improvement in state-of-the-art constrained sampling and
    counting tools, while still retaining theoretical guarantees.
  },
}