2 Search Results for "Jiang, Jie-Hong Roland"


Document
On the Complexity of k-DQBF

Authors: Long-Hin Fung and Tony Tan

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


Abstract
Recently Dependency Quantified Boolean Formula (DQBF) has attracted a lot of attention in the SAT community. Intuitively, a DQBF is a natural extension of quantified boolean formula where for each existential variable, one can specify the set of universal variables it depends on. It has been observed that a DQBF with k existential variables - henceforth denoted by k-DQBF - is essentially a k-CNF formula in succinct representation. However, beside this and the fact that the satisfiability problem is NEXP-complete, not much is known about DQBF. In this paper we take a closer look at k-DQBF and show that a number of well known classical results on k-SAT can indeed be lifted to k-DQBF, which shows a strong resemblance between k-SAT and k-DQBF. More precisely, we show the following. a) The satisfiability problem for 2- and 3-DQBF is PSPACE- and NEXP-complete, respectively. b) There is a parsimonious polynomial time reduction from arbitrary DQBF to 3-DQBF. c) Many polynomial time projections from SAT to languages in NP can be lifted to polynomial time reductions from the satisfiability of DQBF to languages in NEXP. d) Languages in the class NSPACE[s(n)] can be reduced to the satisfiability of 2-DQBF with O(s(n)) universal variables. e) Languages in the class NTIME[t(n)] can be reduced to the satisfiability of 3-DQBF with O(log t(n)) universal variables. The first result parallels the well known classical results that 2-SAT and 3-SAT are NL- and NP-complete, respectively.

Cite as

Long-Hin Fung and Tony Tan. On the Complexity of k-DQBF. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{fung_et_al:LIPIcs.SAT.2023.10,
  author =	{Fung, Long-Hin and Tan, Tony},
  title =	{{On the Complexity of k-DQBF}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{10:1--10:15},
  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.10},
  URN =		{urn:nbn:de:0030-drops-184729},
  doi =		{10.4230/LIPIcs.SAT.2023.10},
  annote =	{Keywords: Dependency quantified boolean formulas, existential variables, complexity}
}
Document
Quantifier Elimination in Stochastic Boolean Satisfiability

Authors: Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang, and Christoph Scholl

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)


Abstract
Stochastic Boolean Satisfiability (SSAT) generalizes quantified Boolean formulas (QBFs) by allowing quantification over random variables. Its generality makes SSAT powerful to model decision or optimization problems under uncertainty. On the other hand, the generalization complicates the computation in its counting nature. In this work, we address the following two questions: 1) Is there an analogy of quantifier elimination in SSAT, similar to QBF? 2) If quantifier elimination is possible for SSAT, can it be effective for SSAT solving? We answer them affirmatively, and develop an SSAT decision procedure based on quantifier elimination. Experimental results demonstrate the unique benefits of the new method compared to the state-of-the-art solvers.

Cite as

Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang, and Christoph Scholl. Quantifier Elimination in Stochastic Boolean Satisfiability. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.SAT.2022.23,
  author =	{Wang, Hao-Ren and Tu, Kuan-Hua and Jiang, Jie-Hong Roland and Scholl, Christoph},
  title =	{{Quantifier Elimination in Stochastic Boolean Satisfiability}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.23},
  URN =		{urn:nbn:de:0030-drops-166970},
  doi =		{10.4230/LIPIcs.SAT.2022.23},
  annote =	{Keywords: Stochastic Boolean Satisfiability, Quantifier Elimination, Decision Procedure}
}
  • Refine by Author
  • 1 Fung, Long-Hin
  • 1 Jiang, Jie-Hong Roland
  • 1 Scholl, Christoph
  • 1 Tan, Tony
  • 1 Tu, Kuan-Hua
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Problems, reductions and completeness

  • Refine by Keyword
  • 1 Decision Procedure
  • 1 Dependency quantified boolean formulas
  • 1 Quantifier Elimination
  • 1 Stochastic Boolean Satisfiability
  • 1 complexity
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2022
  • 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