Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling
(2020) 32nd International Conference on Computer Aided Verification, CAV 2020 In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 12224 LNCS. p.463-484- 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. 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,... (More)
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. 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 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 the resulting system, called, with the state of the art approximate model counter, and the state of the art almost-uniform model sampler. Through an extensive evaluation over a large benchmark set of over 1896 instances, we observe that 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.
(Less)
- author
- Soos, Mate ; Gocht, Stephan LU and Meel, Kuldeep S.
- organization
- publishing date
- 2020
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
- series title
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
- editor
- Lahiri, Shuvendu K. and Wang, Chao
- volume
- 12224 LNCS
- pages
- 22 pages
- publisher
- Springer Gabler
- conference name
- 32nd International Conference on Computer Aided Verification, CAV 2020
- conference location
- Los Angeles, United States
- conference dates
- 2020-07-21 - 2020-07-24
- external identifiers
-
- scopus:85089223997
- ISSN
- 1611-3349
- 0302-9743
- ISBN
- 9783030532871
- DOI
- 10.1007/978-3-030-53288-8_22
- language
- English
- LU publication?
- yes
- id
- 8de5c475-9b32-458e-8474-113550a92ab8
- date added to LUP
- 2020-08-19 10:43:27
- date last changed
- 2024-06-27 22:56:49
@inproceedings{8de5c475-9b32-458e-8474-113550a92ab8,
abstract = {{<p>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. 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 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 the resulting system, called, with the state of the art approximate model counter, and the state of the art almost-uniform model sampler. Through an extensive evaluation over a large benchmark set of over 1896 instances, we observe that 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.</p>}},
author = {{Soos, Mate and Gocht, Stephan and Meel, Kuldeep S.}},
booktitle = {{Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings}},
editor = {{Lahiri, Shuvendu K. and Wang, Chao}},
isbn = {{9783030532871}},
issn = {{1611-3349}},
language = {{eng}},
pages = {{463--484}},
publisher = {{Springer Gabler}},
series = {{Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}},
title = {{Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling}},
url = {{http://dx.doi.org/10.1007/978-3-030-53288-8_22}},
doi = {{10.1007/978-3-030-53288-8_22}},
volume = {{12224 LNCS}},
year = {{2020}},
}