4 Search Results for "Yang, Jiong"

Document
DOI: 10.4230/LIPIcs.SAT.2023.28
Explaining SAT Solving Using Causal Reasoning

Authors: Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
The past three decades have witnessed notable success in designing efficient SAT solvers, with modern solvers capable of solving industrial benchmarks containing millions of variables in just a few seconds. The success of modern SAT solvers owes to the widely-used CDCL algorithm, which lacks comprehensive theoretical investigation. Furthermore, it has been observed that CDCL solvers still struggle to deal with specific classes of benchmarks comprising only hundreds of variables, which contrasts with their widespread use in real-world applications. Consequently, there is an urgent need to uncover the inner workings of these seemingly weak yet powerful black boxes. In this paper, we present a first step towards this goal by introducing an approach called {CausalSAT}, which employs causal reasoning to gain insights into the functioning of modern SAT solvers. {CausalSAT} initially generates observational data from the execution of SAT solvers and learns a structured graph representing the causal relationships between the components of a SAT solver. Subsequently, given a query such as whether a clause with low literals blocks distance (LBD) has a higher clause utility, {CausalSAT} calculates the causal effect of LBD on clause utility and provides an answer to the question. We use {CausalSAT} to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings, such as the query above or the notion that clauses with high LBD experience a rapid drop in utility over time. Moreover, {CausalSAT} can address previously unexplored questions, like which branching heuristic leads to greater clause utility in order to study the relationship between branching and clause management. Experimental evaluations using practical benchmarks demonstrate that {CausalSAT} effectively fits the data, verifies four "rules of thumb", and provides answers to three questions closely related to implementing modern solvers.
Cite as

Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining SAT Solving Using Causal Reasoning. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2023.28,
  author =	{Yang, Jiong and Shaw, Arijit and Baluta, Teodora and Soos, Mate and Meel, Kuldeep S.},
  title =	{{Explaining SAT Solving Using Causal Reasoning}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.28},
  URN =		{urn:nbn:de:0030-drops-184909},
  doi =		{10.4230/LIPIcs.SAT.2023.28},
  annote =	{Keywords: Satisfiability, Causality, SAT solver, Clause management}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.58
Engineering an Efficient PB-XOR Solver

Authors: Jiong Yang and Kuldeep S. Meel

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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.
Cite as

Jiong Yang and Kuldeep S. Meel. Engineering an Efficient PB-XOR Solver. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 58:1-58:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.58},
  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}
}
Document
DOI: 10.4230/OASIcs.Fog-IoT.2020.10
Fog Network Task Scheduling for IoT Applications

Authors: Chongchong Zhang, Fei Shen, Jiong Jin, and Yang Yang

Published in: OASIcs, Volume 80, 2nd Workshop on Fog Computing and the IoT (Fog-IoT 2020)

Abstract
In the Internet of Things (IoT) networks, the data traffic would be very bursty and unpredictable. It is therefore very difficult to analyze and guarantee the delay performance for delay-sensitive IoT applications in fog networks, such as emergency monitoring, intelligent manufacturing, and autonomous driving. To address this challenging problem, a Bursty Elastic Task Scheduling (BETS) algorithm is developed to best accommodate bursty task arrivals and various requirements in IoT networks, thus optimizing service experience for delay-sensitive applications with only limited communication resources in time-varying and competing environments. To better describe the stability and consistence of Quality of Service (QoS) in realistic scenarios, a new performance metric "Bursty Service Experience Index (BSEI)" is defined and quantified as delay jitter normalized by the average delay. Finally, the numeral results shows that the performance of BETS is fully evaluated, which can achieve 5-10 times lower BSEI than traditional task scheduling algorithms, e.g. Proportional Fair (PF) and the Max Carrier-to-Interference ratio (MCI), under bursty traffic conditions. These results demonstrate that BETS can effectively smooth down the bursty characteristics in IoT networks, and provide much predictable and acceptable QoS for delay-sensitive applications.
Cite as

Chongchong Zhang, Fei Shen, Jiong Jin, and Yang Yang. Fog Network Task Scheduling for IoT Applications. In 2nd Workshop on Fog Computing and the IoT (Fog-IoT 2020). Open Access Series in Informatics (OASIcs), Volume 80, pp. 10:1-10:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:OASIcs.Fog-IoT.2020.10,
  author =	{Zhang, Chongchong and Shen, Fei and Jin, Jiong and Yang, Yang},
  title =	{{Fog Network Task Scheduling for IoT Applications}},
  booktitle =	{2nd Workshop on Fog Computing and the IoT (Fog-IoT 2020)},
  pages =	{10:1--10:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-144-3},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{80},
  editor =	{Cervin, Anton and Yang, Yang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Fog-IoT.2020.10},
  URN =		{urn:nbn:de:0030-drops-120049},
  doi =		{10.4230/OASIcs.Fog-IoT.2020.10},
  annote =	{Keywords: Task Scheduling, Internet of Things, fog network, delay sensitive}
}
Document
DOI: 10.4230/OASIcs.Fog-IoT.2020.11
Realizing Video Analytic Service in the Fog-Based Infrastructure-Less Environments

Authors: Qiushi Zheng, Jiong Jin, Tiehua Zhang, Longxiang Gao, and Yong Xiang

Published in: OASIcs, Volume 80, 2nd Workshop on Fog Computing and the IoT (Fog-IoT 2020)

Abstract
Deep learning has unleashed the great potential in many fields and now is the most significant facilitator for video analytics owing to its capability to providing more intelligent services in a complex scenario. Meanwhile, the emergence of fog computing has brought unprecedented opportunities to provision intelligence services in infrastructure-less environments like remote national parks and rural farms. However, most of the deep learning algorithms are computationally intensive and impossible to be executed in such environments due to the needed supports from the cloud. In this paper, we develop a video analytic framework, which is tailored particularly for the fog devices to realize video analytic service in a rapid manner. Also, the convolution neural networks are used as the core processing unit in the framework to facilitate the image analysing process.
Cite as

Qiushi Zheng, Jiong Jin, Tiehua Zhang, Longxiang Gao, and Yong Xiang. Realizing Video Analytic Service in the Fog-Based Infrastructure-Less Environments. In 2nd Workshop on Fog Computing and the IoT (Fog-IoT 2020). Open Access Series in Informatics (OASIcs), Volume 80, pp. 11:1-11:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{zheng_et_al:OASIcs.Fog-IoT.2020.11,
  author =	{Zheng, Qiushi and Jin, Jiong and Zhang, Tiehua and Gao, Longxiang and Xiang, Yong},
  title =	{{Realizing Video Analytic Service in the Fog-Based Infrastructure-Less Environments}},
  booktitle =	{2nd Workshop on Fog Computing and the IoT (Fog-IoT 2020)},
  pages =	{11:1--11:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-144-3},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{80},
  editor =	{Cervin, Anton and Yang, Yang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Fog-IoT.2020.11},
  URN =		{urn:nbn:de:0030-drops-120050},
  doi =		{10.4230/OASIcs.Fog-IoT.2020.11},
  annote =	{Keywords: Fog Computing, Convolution Neural Network, Infrastructure-less Environment}
}
  • Refine by Author
  • 2 Jin, Jiong
  • 2 Meel, Kuldeep S.
  • 2 Yang, Jiong
  • 1 Baluta, Teodora
  • 1 Gao, Longxiang
  • Show More...

  • Refine by Classification
  • 2 Computing methodologies → Artificial intelligence
  • 2 Theory of computation
  • 1 Computing methodologies → Object detection
  • 1 Networks

  • Refine by Keyword
  • 1 Causality
  • 1 Clause management
  • 1 Convolution Neural Network
  • 1 Fog Computing
  • 1 Gauss Jordan Elimination
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2020
  • 1 2021
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact