On Computing Minimal Independent Support and Its Applications to Sampling and Counting (Extended 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 combinatorial (SAT/SMT) solvers and universal hash functions that are typically encoded as XOR constraints of length n/2 for an input formula with n variables. It has been observed that lower density XORs are easy to reason in practice and the runtime performance of solvers greatly improves with the decrease in the length of XOR-constraints. Therefore, recent research effort has 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.