Tony Tan

CSL Conference 2026 Conference Paper

Analysis of Logics with Arithmetic

• Michael Benedikt
• Chia-Hsuan Lu
• Tony Tan

We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional "global cardinality constraints": restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.

AAAI Conference 2026 Conference Paper

Model Counting for Dependency Quantified Boolean Formulas

• Long-Hin Fung
• Che Cheng
• Jie-Hong Roland Jiang
• Friedrich Slivovsky
• Tony Tan

Dependency Quantified Boolean Formulas (DQBF) generalize QBF by explicitly specifying which universal variables each existential variable depends on, instead of relying on a linear quantifier order. The satisfiability problem of DQBF is NEXP-complete, and many hard problems can be succinctly encoded as DQBF. Recent work has revealed a strong analogy between DQBF and SAT: k-DQBF (with k existential variables) is a succinct form of k-SAT, and satisfiability is NEXP-complete for 3-DQBF but PSPACE-complete for 2-DQBF, mirroring the complexity gap between 3-SAT (NP-complete) and 2-SAT (NL-complete). Motivated by this analogy, we study the model counting problem for DQBF, denoted #DQBF. Our main theoretical result is that #2-DQBF is #EXP-complete, where #EXP is the exponential-time analogue of #P. This parallels Valiant's classical theorem stating that #2-SAT is #P-complete. As a direct application, we show that first-order model counting (FOMC) remains #EXP-complete even when restricted to a PSPACE-decidable fragment of first-order logic and domain size two. Building on recent successes in reducing 2-DQBF satisfiability to symbolic model checking, we develop a dedicated 2-DQBF model counter. Using a diverse set of crafted instances, we experimentally evaluated it against a baseline that expands 2-DQBF formulas into propositional formulas and applies propositional model counting. While the baseline worked well when each existential variable depends on few variables, our implementation scaled significantly better to larger dependency sets.

TACAS Conference 2026 Conference Paper

Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing

• Chia-Hsuan Lu
• Tony Tan
• Michael Benedikt

SAT Conference 2025 Conference Paper

Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas

• Che Cheng
• Long-Hin Fung
• Jie-Hong Roland Jiang
• Friedrich Slivovsky
• Tony Tan

Dependency Quantified Boolean Formulas (DQBF) extend Quantified Boolean Formulas by allowing each existential variable to depend on an explicitly specified subset of the universal variables. The satisfiability problem for DQBF is NEXP-complete in general, with only a few tractable fragments known to date. We investigate the complexity of DQBF with k existential variables (k-DQBF) under structural restrictions on the matrix - specifically, when it is in Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) - as well as under constraints on the dependency sets. For DNF matrices, we obtain a clear classification: 2-DQBF is PSPACE-complete, while 3-DQBF is NEXP-hard, even with disjoint dependencies. For CNF matrices, the picture is more nuanced: we show that the complexity of k-DQBF ranges from NL-complete for 2-DQBF with disjoint dependencies to NEXP-complete for 6-DQBF with arbitrary dependencies.

SAT Conference 2023 Conference Paper

On the Complexity of k-DQBF

• Long-Hin Fung
• Tony Tan

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.

Highlights Conference 2016 Conference Abstract

Reasoning with difference on roles in description logic ALC

• Tony Tan
• Jan Van den Bussche
• Xiaowang Zhang

We present an algebra

Highlights Conference 2013 Conference Abstract

Regular graphs and the spectra of two-variable logic with counting

• Eryk Kopczyński
• Tony Tan

For a formula $\phi$ over a signature including predicates $P_1. .. P_k$, we define the image of $\phi$ as the set of tuples $(n_1. .. n_k)$ such that there is a model of $\phi$ where exactly $n_i$ elements satisfy $P_i$. For example, if each author has written exactly 2 papers, and each paper has exactly 3 authors, then 2*total number of authors=3*total number of authors. This can be seen as a generalization of the well known notion of a spectrum. Our main result is that, for formulae of FO2C, spectra and images are definable in Presburger arithmetic, and thus semilinear (and closed under complement).

MFCS Conference 2009 Conference Paper

On Pebble Automata for Data Languages with Decidable Emptiness Problem

• Tony Tan

Abstract In this paper we study a subclass of pebble automata (PA) for data languages for which the emptiness problem is decidable. Namely, we show that the emptiness problem for weak 2-pebble automata is decidable, while the same problem for weak 3-pebble automata is undecidable. We also introduce the so-called top view weak PA. Roughly speaking, top view weak PA are weak PA where the equality test is performed only between the data values seen by the two most recently placed pebbles. The emptiness problem for this model is still decidable.

MFCS Conference 2005 Conference Paper

Approximating Polygonal Objects by Deformable Smooth Surfaces

• Ho-Lun Cheng
• Tony Tan

Abstract We propose a method to approximate a polygonal object by a deformable smooth surface, namely the t -skin defined by Edelsbrunner for all 0< t < 1. We guarantee that they are homeomorphic and their Hausdorff distance is at most ε >0. Such construction makes it possible for fully automatic, smooth and robust deformation between two polygonal objects with different topologies. En route to our results, we also give an approximation of a polygonal object with a union of balls.