3 Search Results for "Zhang, Guoqiang"

Document
DOI: 10.4230/LIPIcs.SAT.2024.17
Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem

Authors: Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Parallelization of SAT solvers is an important technique for improving solver performance. The selection of the learnt clauses to share among parallel workers is crucial for its efficiency. Literal block distance (LBD) is often used to evaluate the quality of clauses to select. We propose a new method, Parallel Clause sharing based on graph Structure (PaCS), to select good clauses for sharing. First, we conducted three preliminary experiments to assess the performance of LBD in parallel clause sharing: a performance comparison between the LBD and clause size, an analysis of the utilization of shared clauses, and a comparison of the LBD values of shared clauses at originating and receiving workers. These experiments indicate that the LBD may not be optimal for learnt clause sharing. We attribute the results to the LBD’s inherent dependency on decision trees. Each parallel worker has a unique decision tree; thus, a sharing clause that is good for its originating worker may not be good for others. Therefore, we propose PaCS, a search-independent method that uses the graph structure derived from the input CNF of SAT problems. PaCS evaluates clauses using their edges' weight in the variable incidence graph. Using the input CNF’s graph is effective for parallel clause sharing because it is the common input for all parallel workers. Furthermore, using edge weight can select clauses whose variables' Boolean values are more likely to be determined. Performance evaluation experiments demonstrate that our strategy outperforms LBD by 4% in the number of solved instances and by 12% in PAR-2. This study opens avenues for further improvements in parallel-solving strategies using the structure of SAT problems and reinterpretations of the quality of learnt clauses.
Cite as

Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba. Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{iida_et_al:LIPIcs.SAT.2024.17,
  author =	{Iida, Yoichiro and Sonobe, Tomohiro and Inaba, Mary},
  title =	{{Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.17},
  URN =		{urn:nbn:de:0030-drops-205392},
  doi =		{10.4230/LIPIcs.SAT.2024.17},
  annote =	{Keywords: SAT Solver, Structure of SAT, Parallel application, Clause Learning}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.19
On Limits of Symbolic Approach to SAT Solving

Authors: Dmitry Itsykson and Sergei Ovcharov

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧, ∃, reordering) algorithms. We prove the first exponential lower bound of OBDD(∧, ∃, reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧, ∃, reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧, ∃, reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHP^{n+1}_n.
Cite as

Dmitry Itsykson and Sergei Ovcharov. On Limits of Symbolic Approach to SAT Solving. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.SAT.2024.19,
  author =	{Itsykson, Dmitry and Ovcharov, Sergei},
  title =	{{On Limits of Symbolic Approach to SAT Solving}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.19},
  URN =		{urn:nbn:de:0030-drops-205415},
  doi =		{10.4230/LIPIcs.SAT.2024.19},
  annote =	{Keywords: Symbolic quantifier elimination, OBDD, lower bounds, tree-like resolution, proof complexity, error-correcting codes, binary pigeonhole principle}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.15
Best-Effort Lazy Evaluation for Python Software Built on APIs

Authors: Guoqiang Zhang and Xipeng Shen

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
This paper focuses on an important optimization opportunity in Python-hosted domain-specific languages (DSLs): the use of laziness for optimization, whereby multiple API calls are deferred and then optimized prior to execution (rather than executing eagerly, which would require executing each call in isolation). In existing supports of lazy evaluation, laziness is "terminated" as soon as control passes back to the host language in any way, limiting opportunities for optimization. This paper presents Cunctator, a framework that extends this laziness to more of the Python language, allowing intermediate values from DSLs like NumPy or Pandas to flow back to the host Python code without triggering evaluation. This exposes more opportunities for optimization and, more generally, allows for larger computation graphs to be built, producing 1.03-14.2X speedups on a set of programs in common libraries and frameworks.
Cite as

Guoqiang Zhang and Xipeng Shen. Best-Effort Lazy Evaluation for Python Software Built on APIs. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ECOOP.2021.15,
  author =	{Zhang, Guoqiang and Shen, Xipeng},
  title =	{{Best-Effort Lazy Evaluation for Python Software Built on APIs}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{15:1--15:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.15},
  URN =		{urn:nbn:de:0030-drops-140582},
  doi =		{10.4230/LIPIcs.ECOOP.2021.15},
  annote =	{Keywords: Lazy Evaluation, Python, API Optimization}
}
  • Refine by Author
  • 1 Iida, Yoichiro
  • 1 Inaba, Mary
  • 1 Itsykson, Dmitry
  • 1 Ovcharov, Sergei
  • 1 Shen, Xipeng
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Heuristic function construction
  • 1 Mathematics of computing → Solvers
  • 1 Software and its engineering → Dynamic compilers
  • 1 Software and its engineering → Runtime environments
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 1 API Optimization
  • 1 Clause Learning
  • 1 Lazy Evaluation
  • 1 OBDD
  • 1 Parallel application
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2024
  • 1 2021

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