• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling .
Mate Soos, Stephan Gocht and Kuldeep S. Meel.
In Proceedings of International Conference on Computer-Aided Verification (CAV), July 2020.
Given a Boolean formula, the problem of counting seeks to estimate the number of solutions of F while the problem of uniform sampling seeks to sample solutions uniformly at random. Counting and uniform sampling are fundamental problems in computer science with a wide range of applications ranging from constrained random simulation, probabilistic inference to network reliability and beyond. Despite intense theoretical and empirical investigations, development of scalable techniques for sampling and counting without sacrificing theoretical guarantees remains the holy grail. The past few years have witnessed the rise of hashing-based approaches that use XOR-based hashing and employ SAT solvers to solve the resulting CNF formulas conjuncted with XOR constraints. Since over 99% of the runtime of hashing-based techniques is spent inside the SAT queries, improving CNF-XOR solvers has emerged as a key challenge. In this paper, we identify the key performance bottlenecks in the recently proposed BIRD architecture, and we focus on overcoming these bottlenecks by accelerating the XOR handling within the SAT solver and on improving the solver integration through a smarter use of (partial) solutions. We integrate BIRD2 with the state of the art approximate model counter, ApproxMC3, and the state of the art almost-uniform model sampler UniGen2. Through an extensive evaluation over a large benchmark set of over 1896 instances, we observe that BIRD2 leads to consistent speed up for both counting and sampling, and in particular, we solve 77 and 51 more instances for counting and sampling respectively.
@inproceedings{SGM20,
title={
Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting
and Sampling
},
author={Soos, Mate and Gocht, Stephan and Meel, Kuldeep S.},
bib2html_pubtype={Refereed Conference},
booktitle=CAV,
month=jul,
bib2html_rescat={Solver Engineering,Counting, Sampling},
bib2html_dl_pdf={../Papers/cav20-sgm.pdf},
year={2020},
abstract={
Given a Boolean formula, the problem of counting seeks to estimate the
number of solutions of F while the problem of uniform sampling seeks to
sample solutions uniformly at random. Counting and uniform sampling are
fundamental
problems in computer science with a wide range of applications
ranging from constrained random simulation, probabilistic inference to
network reliability and beyond. Despite intense theoretical and empirical
investigations, development of scalable techniques for sampling and counting
without
sacrificing theoretical guarantees remains the holy grail. The past few
years have witnessed the rise of hashing-based approaches that use XOR-based
hashing and employ SAT solvers to solve the resulting CNF formulas
conjuncted
with XOR constraints. Since over 99\% of the runtime of hashing-based
techniques is spent inside the SAT queries, improving CNF-XOR solvers has
emerged as a key challenge.
In this paper, we identify the key performance bottlenecks in the recently
proposed BIRD architecture, and we focus on overcoming these bottlenecks by
accelerating the XOR handling within the SAT solver and on improving the
solver integration through a smarter use
of (partial) solutions. We integrate BIRD2 with the state of the art
approximate model counter, ApproxMC3, and the state of the art
almost-uniform model
sampler UniGen2. Through an extensive evaluation over a large benchmark set
of over 1896 instances, we observe that BIRD2 leads to consistent speed up
for both counting and sampling, and in particular, we solve 77 and 51 more
instances for counting and sampling respectively.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21