2 Search Results for "Bradley, Felix"

Document

DOI: 10.4230/LIPIcs.SAT.2024.13

Entailing Generalization Boosts Enumeration

Authors: Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon

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

Abstract

Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.

Cite as

Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing Generalization Boosts Enumeration. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fried_et_al:LIPIcs.SAT.2024.13,
  author =	{Fried, Dror and Nadel, Alexander and Sebastiani, Roberto and Shalmon, Yogev},
  title =	{{Entailing Generalization Boosts Enumeration}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{13:1--13:14},
  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.13},
  URN =		{urn:nbn:de:0030-drops-205351},
  doi =		{10.4230/LIPIcs.SAT.2024.13},
  annote =	{Keywords: Generalization, Minimization, Prime Implicant, AllSAT, SAT, Circuits}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2022.9

A Metatheoretic Analysis of Subtype Universes

Authors: Felix Bradley and Zhaohui Luo

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract

Subtype universes were initially introduced as an expressive mechanisation of bounded quantification extending a modern type theory. In this paper, we consider a dependent type theory equipped with coercive subtyping and a generalisation of subtype universes. We prove results regarding the metatheoretic properties of subtype universes, such as consistency and strong normalisation. We analyse the causes of undecidability in bounded quantification, and discuss how coherency impacts the metatheoretic properties of theories implementing bounded quantification. We describe the effects of certain choices of subtyping inference rules on the expressiveness of a type theory, and examine various applications in natural language semantics, programming languages, and mathematics formalisation.

Cite as

Felix Bradley and Zhaohui Luo. A Metatheoretic Analysis of Subtype Universes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bradley_et_al:LIPIcs.TYPES.2022.9,
  author =	{Bradley, Felix and Luo, Zhaohui},
  title =	{{A Metatheoretic Analysis of Subtype Universes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.9},
  URN =		{urn:nbn:de:0030-drops-184520},
  doi =		{10.4230/LIPIcs.TYPES.2022.9},
  annote =	{Keywords: Type theory, coercive subtyping, subtype universes}
}

Refine by Author
1 Bradley, Felix
1 Fried, Dror
1 Luo, Zhaohui
1 Nadel, Alexander
1 Sebastiani, Roberto
Show More...

Refine by Classification
1 Mathematics of computing → Solvers
1 Theory of computation → Type theory

Refine by Keyword
1 AllSAT
1 Circuits
1 Generalization
1 Minimization
1 Prime Implicant
Show More...

Refine by Type
2 document

Refine by Publication Year
1 2023
1 2024