License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2021.58
URN: urn:nbn:de:0030-drops-153499
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15349/
Go to the corresponding LIPIcs Volume Portal

Yang, Jiong ; Meel, Kuldeep S.

Engineering an Efficient PB-XOR Solver

pdf-format:
LIPIcs-CP-2021-58.pdf (1.0 MB)

Abstract

Despite the NP-completeness of Boolean satisfiability, modern SAT solvers are routinely able to handle large practical instances, and consequently have found wide ranging applications. The primary workhorse behind the success of SAT solvers is the widely acclaimed Conflict Driven Clause Learning (CDCL) paradigm, which was originally proposed in the context of Boolean formulas in CNF. The wide ranging applications of SAT solvers have highlighted that for several domains, CNF is not a natural representation and the reliance of modern SAT solvers on resolution proof system limit their ability to efficiently solve several families of constraints. Consequently, the past decade has witnessed the design of solvers with native support for constraints such as Pseudo-Boolean (PB) and CNF-XOR.
The primary contribution of our work is an efficient solver engineered for PB-XOR formulas, i.e., formulas consisting of a conjunction of PB and XOR constraints. We first observe that a simple adaption of CNF-XOR architecture does not provide an improvement over baseline; our analysis highlights the need for careful engineering of the order of propagations. To this end, we propose three different tactics, all of which achieve significant performance improvements over the baseline. Our work is motivated by applications arising from binarized neural network verification where the verification of properties such as robustness, fairness, trojan attacks can be reduced to model counting queries; the state of the art model counters reduce counting to polynomially many SAT queries over the original formula conjuncted with randomly generated XOR constraints. To this end, we augment ApproxMC with LinPB and we call the resulting counter as ApproxMCPB. In an extensive empirical comparison over 1076 benchmarks, we observe that ApproxMCPB can solve 912 instances while the baseline version of ApproxMC4 (augmented with CryptoMiniSat) can solve only 802 instances.

BibTeX - Entry

@InProceedings{yang_et_al:LIPIcs.CP.2021.58,
  author =	{Yang, Jiong and Meel, Kuldeep S.},
  title =	{{Engineering an Efficient PB-XOR Solver}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{58:1--58:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15349},
  URN =		{urn:nbn:de:0030-drops-153499},
  doi =		{10.4230/LIPIcs.CP.2021.58},
  annote =	{Keywords: PB-XOR Solving, Pseudo-Boolean, XOR, Gauss Jordan Elimination, SAT-Solving, Model Counting}
}

Keywords: PB-XOR Solving, Pseudo-Boolean, XOR, Gauss Jordan Elimination, SAT-Solving, Model Counting
Collection: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Issue Date: 2021
Date of publication: 15.10.2021
Supplementary Material: The open source tools and benchmarks are available at:
Software (Source Code LinPB): https://github.com/meelgroup/linpb
Software (Source Code ApproxMCPB): https://github.com/meelgroup/approxmcpb
Dataset (BNN benchmarks and raw data of experiments): https://doi.org/10.5281/zenodo.5526835

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI