Search Results

Documents authored by Sheng, Aeacus

Artifact
Software
DOI: 10.4230/artifacts.26768
Dsc

Authors: Aeacus Sheng

Abstract
Cite as

Aeacus Sheng. Dsc (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26768,
   title = {{Dsc}}, 
   author = {Sheng, Aeacus},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:3426ce298c72bee5193a80074861219cff844070;origin=https://github.com/Aeacu2/Dsc;visit=swh:1:snp:dabe0de147e4a71e4c8a6cb04a350397ae70df98;anchor=swh:1:rev:bea2da7e663f4b543e057d36a4dba9bd422abc03}{\texttt{swh:1:dir:3426ce298c72bee5193a80074861219cff844070}} (visited on 2026-07-16)},
   url = {https://github.com/Aeacu2/Dsc},
   doi = {10.4230/artifacts.26768},
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2026.32
Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)

Authors: Aeacus Sheng, Wenda Li, and Paul B. Jackson

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes' rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm's theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches. We take an initial step towards efficient verified real root isolation by formally verifying two simple algorithms based on Descartes' rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms, present formal proofs of termination, soundness, and completeness, and discuss our code-generation efforts. Brief experiments show promising performance improvements over existing formally verified algorithms in Isabelle/HOL.
Cite as

Aeacus Sheng, Wenda Li, and Paul B. Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 32:1-32:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.ITP.2026.32,
  author =	{Sheng, Aeacus and Li, Wenda and Jackson, Paul B.},
  title =	{{Faster Verified Real Root Isolation with Descartes' Rule of Signs}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{32:1--32:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.32},
  URN =		{urn:nbn:de:0030-drops-270068},
  doi =		{10.4230/LIPIcs.ITP.2026.32},
  annote =	{Keywords: Isabelle/HOL, Real root isolation, Descartes' rule of signs}
}
Artifact
Software
DOI: 10.4230/artifacts.24212
jreeves3/ulc-cadical

Authors: Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule

Abstract
Cite as

Aeacus Sheng, Joseph E. Reeves, Marijn J. H. Heule. jreeves3/ulc-cadical (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24212,
   title = {{jreeves3/ulc-cadical}}, 
   author = {Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:615c90061cfad33b59249832fb0043defef84419;origin=https://github.com/jreeves3/ulc-cadical;visit=swh:1:snp:f96217667e13be0663f27340946c119cf64504c9;anchor=swh:1:rev:bb9484ab042c423c1c37fa63dbac3679957afff1}{\texttt{swh:1:dir:615c90061cfad33b59249832fb0043defef84419}} (visited on 2025-08-07)},
   url = {https://github.com/jreeves3/ulc-cadical},
   doi = {10.4230/artifacts.24212},
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.29
Reencoding Unique Literal Clauses

Authors: Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements.
Cite as

Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule. Reencoding Unique Literal Clauses. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.SAT.2025.29,
  author =	{Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Reencoding Unique Literal Clauses}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{29:1--29:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.29},
  URN =		{urn:nbn:de:0030-drops-237635},
  doi =		{10.4230/LIPIcs.SAT.2025.29},
  annote =	{Keywords: Satisfiability solving, auxiliary variables, graph coloring}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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