2 Search Results for "Hall, Alexander"

Document
DOI: 10.4230/LIPIcs.SAT.2023.9
AllSAT for Combinational Circuits

Authors: Dror Fried, Alexander Nadel, and Yogev Shalmon

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

Abstract
Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.
Cite as

Dror Fried, Alexander Nadel, and Yogev Shalmon. AllSAT for Combinational Circuits. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{fried_et_al:LIPIcs.SAT.2023.9,
  author =	{Fried, Dror and Nadel, Alexander and Shalmon, Yogev},
  title =	{{AllSAT for Combinational Circuits}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{9:1--9:18},
  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.9},
  URN =		{urn:nbn:de:0030-drops-184717},
  doi =		{10.4230/LIPIcs.SAT.2023.9},
  annote =	{Keywords: AllSAT, SAT, Circuits}
}
Document
DOI: 10.4230/DagSemProc.05031.17
Network Discovery and Verification

Authors: Zuzana Beerliova, Felix Eberhard, Thomas Erlebach, Alexander Hall, Michael Hoffmann, Matus Mihalak, and L. Shankar Ram

Published in: Dagstuhl Seminar Proceedings, Volume 5031, Algorithms for Optimization with Incomplete Information (2005)

Abstract
Consider the problem of discovering (or verifying) the edges and non-edges of a network, modelled as a connected undirected graph, using a minimum number of queries. A query at a vertex v discovers (or verifies) all edges and non-edges whose endpoints have different distance from v. In the network discovery problem, the edges and non-edges are initially unknown, and the algorithm must select the next query based only on the results of previous queries. We study the problem using competitive analysis and give a randomized on-line algorithm with competitive ratio O(sqrt(n*log n)) for graphs with n vertices. We also show that no deterministic algorithm can have competitive ratio better than 3. In the network verification problem, the graph is known in advance and the goal is to compute a minimum number of queries that verify all edges and non-edges. This problem has previously been studied as the problem of placing landmarks in graphs or determining the metric dimension of a graph. We show that there is no approximation algorithm for this problem with ratio o(log n) unless P=NP. Furthermore, we prove that the optimal number of queries for d-dimensional hypercubes is Theta(d/log d).
Cite as

Zuzana Beerliova, Felix Eberhard, Thomas Erlebach, Alexander Hall, Michael Hoffmann, Matus Mihalak, and L. Shankar Ram. Network Discovery and Verification. In Algorithms for Optimization with Incomplete Information. Dagstuhl Seminar Proceedings, Volume 5031, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{beerliova_et_al:DagSemProc.05031.17,
  author =	{Beerliova, Zuzana and Eberhard, Felix and Erlebach, Thomas and Hall, Alexander and Hoffmann, Michael and Mihalak, Matus and Ram, L. Shankar},
  title =	{{Network Discovery and Verification}},
  booktitle =	{Algorithms for Optimization with Incomplete Information},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5031},
  editor =	{Susanne Albers and Rolf H. M\"{o}hring and Georg Ch. Pflug and R\"{u}diger Schultz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05031.17},
  URN =		{urn:nbn:de:0030-drops-594},
  doi =		{10.4230/DagSemProc.05031.17},
  annote =	{Keywords: on-line algorithms , set cover , landmarks , metric dimension}
}
  • Refine by Author
  • 1 Beerliova, Zuzana
  • 1 Eberhard, Felix
  • 1 Erlebach, Thomas
  • 1 Fried, Dror
  • 1 Hall, Alexander
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Solvers

  • Refine by Keyword
  • 1 AllSAT
  • 1 Circuits
  • 1 SAT
  • 1 landmarks
  • 1 metric dimension
  • Show More...

  • Refine by Type
  • 2 document

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