Bachelor Thesis

Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau

Department of Computer Science,

Gottlieb-Daimler-Straße, 67663 Kaiserslautern, Germany

Supervisors:     Prof. Dr. Anthony W. Lin

Prof. Matthew Hague

I hereby declare that I am the sole author of this bachelor thesis and that the work contained herein is my own except where explicitly stated otherwise in the text. I further declare that I have not submitted this thesis at any other institution in order to obtain a degree.

Kaiserslautern, t]@c@

Alexander Mayorov

Variable independence and decomposability are algorithmic techniques for simplifying logical formulas by tearing apart connections between free variables. These techniques were originally proposed to speed up query evaluation in constraint databases, in particular by representing the query as a Boolean combination of formulas with no interconnected variables. They also have many other applications in SMT, string analysis, databases, automata theory and other areas. However, the precise complexity of variable independence and decomposability has been left open especially for the quantifier-free theory of linear real arithmetic (LRA), which is central in database applications. We introduce a novel characterization of formulas admitting decompositions and use it to show that it is $ \coNP $-complete to decide variable decomposability over LRA. As a corollary, we obtain that deciding variable independence is in the second level of the polynomial hierarchy. These results substantially improve the best known double-exponential time algorithms for variable decomposability and independence. In many practical applications, it is important not only to decide variable independence/decomposability algorithmically but also to be able to efficiently eliminate connections between variables whenever possible. We design and implement an algorithm for this problem, which is optimal in theory, exponentially faster compared to the current state-of-the-art algorithm and efficient on various microbenchmarks. In particular, our algorithm is the first one to overcome a fundamental barrier between non-discrete and discrete first-order theories (for the latter, the problem is significantly easier, and many techniques yielding efficient algorithms are known). Formulas arising in practice often have few or even no free variables that are perfectly independent. In this case, our algorithm can compute a best-possible approximation of a decomposition, which can be used to optimize database queries by exploiting partial variable independence, which is present in almost every logical formula or database query constraint.

I wish to express my sincere thanks to my supervisor Anthony Lin for his guidance, continuous support, advice and for the helpful and inspiring discussions we had. I am also very grateful to him for providing me with all the necessary facilities for my research. I would like to thank my co-supervisor Matthew Hague and Daniel Stan for their guidance, useful feedback, comments and for the fruitful discussions we had throughout the entire period of research.

I want to also express my profound gratitude to my family and friends for providing me with unfailing support and continuous encouragement throughout the process of researching and writing this thesis. Thank you.

§ INTRODUCTION

§ PRELIMINARIES

§ UPPER BOUNDS

§ LOWER BOUNDS

§ EXPERIMENTS

§ CONCLUSIONS AND FUTURE WORK

[1]
Sanjeev Arora and Boaz Barak, Computational complexity: a modern
approach, Cambridge University Press, 2009.

[2]
Sheldon Axler, Linear algebra done right, Springer, 2015.

[3]
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A Junttila, Peter
Van Rossum, Stephan Schulz, and Roberto Sebastiani, An incremental and
layered procedure for the satisfiability of linear arithmetic logic., TACAS,
vol. 5, Springer, 2005, pp. 317–333.

[4]
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, and
Roberto Sebastiani, Delayed theory combination vs. nelson-oppen for
satisfiability modulo theories: a comparative analysis, Annals of
Mathematics and Artificial Intelligence 55 (2009), no. 1-2, 63.

[5]
Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph M
Wintersteiger, Programming z3, Engineering Trustworthy Software
Systems: 4th International School, SETSS 2018, Chongqing, China, April 7–12,
2018, Tutorial Lectures 4 (2019), 148–201.

[6]
Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche,
Ramsey quantifiers over automatic structures: Complexity and
applications to verification, Proceedings of the 37th Annual ACM/IEEE
Symposium on Logic in Computer Science, 2022, pp. 1–14.

[7]
Pablo Barceló, Chih-Duo Hong, Xuan Bach Le, Anthony W. Lin, and Reino
Niskanen, Monadic decomposability of regular relations, 46th
International Colloquium on Automata, Languages, and Programming, ICALP
2019, July 9-12, 2019, Patras, Greece, 2019, pp. 103:1–103:14.

[8]
Alexander Brodsky, Joxan Jaffar, and Michael J. Maher, Toward practical
constraint databases, Proceedings of the 19th International Conference on
Very Large Data Bases (San Francisco, CA, USA), VLDB '93, Morgan Kaufmann
Publishers Inc., 1993, p. 567–580.

[9]
Alexander Brodsky and Yoram Kornatzky, The lyric language: Querying
constraint objects, Proceedings of the 1995 ACM SIGMOD International
Conference on Management of Data (New York, NY, USA), SIGMOD '95, Association
for Computing Machinery, 1995, p. 35–46.

[10]
A. Beimel and E. Kushilevitz, Learning boxes in high dimension,
Algorithmica 22 (1998), no. 1, 76–90.

[11]
Alexander Brodsky, Catherine Lassez, Jean-Louis Lassez, and Michael J. Maher,
Separability of polyhedra for optimal filtering of spatial and
constraint data, Journal of Automated Reasoning 23 (1999), no. 1,

[12]
A.R. Bradley and Z. Manna, The calculus of computation: Decision
procedures with applications to verification, Springer Berlin Heidelberg,

[13]
Stephen Boyd and Lieven Vandenberghe, Convex optimization, Cambridge
university press, 2004.

[14]
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu, What
is decidable about string constraints with the replaceall function, Proc.
ACM Program. Lang. 2 (2017), no. POPL.

[15]
Jan Chomicki, Dina Q. Goldin, and Gabriel M. Kuper, Variable independence
and aggregation closure, Proceedings of the Fifteenth ACM
SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 3-5,
1996, Montreal, Canada (Richard Hull, ed.), ACM Press, 1996, pp. 40–48.

[16]
J. Chomicki, D. Goldin, G. Kuper, and D. Toman, Variable independence in
constraint databases, IEEE Transactions on Knowledge and Data Engineering
15 (2003), no. 6, 1422–1436.

[17]
Ashok K. Chandra and David Harel, Computable queries for relational data
bases, Journal of Computer and System Sciences 21 (1980), no. 2,

[18]
Jan Chomicki, Temporal query languages: a survey, International
Conference on Temporal Logic, Springer, 1994, pp. 506–534.

[19]
Bob F. Caviness and Jeremy R. Johnson, Quantifier elimination and
cylindrical algebraic decomposition, Springer Science & Business Media,

[20]
Stavros Cosmadakis, Gabriel Kuper, and Leonid Libkin, On the orthographic
dimension of definable sets, Information processing letters 79
(2001), no. 3, 141–145.

[21]
Jan Chomicki and Peter Z. Revesz, Constraint-based interoperability of
spatiotemporal databases, GeoInformatica 3 (1999), no. 3, 211–243.

[22]
Bruno Dutertre and Leonardo De Moura, A fast linear-arithmetic solver for
dpll (t), Computer Aided Verification: 18th International Conference, CAV
2006, Seattle, WA, USA, August 17-20, 2006. Proceedings 18, Springer, 2006,
pp. 81–94.

[23]
, Integrating simplex with dpll (t), Computer Science Laboratory,
SRI International, Tech. Rep. SRI-CSL-06-01 (2006).

[24]
Leonardo De Moura and Nikolaj Bjørner, Z3: An efficient smt solver,
Proceedings of the Theory and Practice of Software, 14th International
Conference on Tools and Algorithms for the Construction and Analysis of
Systems (Berlin, Heidelberg), TACAS'08/ETAPS'08, Springer-Verlag, 2008,
p. 337–340.

[25]
Loris D’Antoni and Margus Veanes, The power of symbolic automata and
transducers, Computer Aided Verification: 29th International Conference, CAV
2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30,
Springer, 2017, pp. 47–67.

[26]
Heinz-Dieter Ebbinghaus and Jörg Flum, Finite model theory, Springer
Science & Business Media, 2005.

[27]
David Eisenbud, Commutative algebra: with a view toward algebraic
geometry, vol. 150, Springer Science & Business Media, 2013.

[28]
Herbert Edelsbrunner, Raimund Seidel, and Micha Sharir, On the zone
theorem for hyperplane arrangements, SIAM Journal on Computing 22
(1993), no. 2, 418–429.

[29]
Gerd Fisher, Lernbuch lineare algebra und analytische geometrie, 2 ed.,
Springer Vieweg Wiesbaden, 2012 (German).

[30]
Jean Gallier, Basics of affine geometry, pp. 6–61, Springer New York,
New York, NY, 2001.

[31]
Elmer G Gilbert, Daniel W Johnson, and S Sathiya Keerthi, A fast
procedure for computing the distance between complex objects in
three-dimensional space, IEEE Journal on Robotics and Automation 4
(1988), no. 2, 193–203.

[32]
Dina Q. Goldin and Paris C. Kanellakis, Constraint query algebras,
Constraints 1 (1996), no. 1, 45–83.

[33]
Martin Grötschel, László Lovász, and Alexander Schrijver,
Geometric algorithms and combinatorial optimization, vol. 2, Springer
Science & Business Media, 2012.

[34]
Alberto Griggio, A practical approach to satisfiability modulo linear
integer arithmetic, Journal on Satisfiability, Boolean Modeling and
Computation 8 (2012), no. 1-2, 1–27.

[35]
Stéphane Grumbach, Philippe Rigaux, and Luc Segoufin, On the
orthographic dimension of constraint databases, Database Theory—ICDT’99:
7th International Conference Jerusalem, Israel, January 10–12, 1999
Proceedings 7, Springer, 1999, pp. 199–216.

[36]
Stéphane Grumbach, Philippe Rigaux, and Luc Segoufin,
Spatio-temporal data handling with constraints, GeoInformatica
5 (2001), no. 1, 95–115.

[37]
Branko Grünbaum, Convex polytopes, Springer New York, 2003.

[38]
Peter M. Gruber, Convex and discrete geometry, vol. 336, Springer, 2007.

[39]
Volker Gaede and Mark Wallace, An informal introduction to constraint
database systems, Constraint Databases and Applications: Second
International Workshop on Constraint Database Systems, CDB'97 Delphi, Greece,
January 11–12, 1997 CP'96 Workshop on Constraints and Databases Cambridge,
MA, USA, August 19, 1996 Selected Papers 2, Springer, 1996, pp. 7–52.

[40]
Christoph Haase, A survival guide to presburger arithmetic, ACM SIGLOG
News 5 (2018), no. 3, 67–82.

[41]
Paul R. Halmos, Linear algebra problem book, vol. 16, American
Mathematical Soc., 1995.

[42]
Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu,
Monadic decomposition in integer linear arithmetic, Automated
Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France,
July 1-4, 2020, Proceedings, Part I, 2020, pp. 122–140.

[43]
Lane A. Hemaspaandra and Mitsunori Ogihara, The complexity theory
companion, Springer Berlin Heidelberg, 2002.

[44]
Thomas W. Hungerford, Algebra, vol. 73, Springer Science & Business
Media, 2012.

[45]
Neil Immerman, Descriptive complexity, Springer Science & Business
Media, 2012.

[46]
Artur Jeż, Word equations in non-deterministic linear space, Journal
of Computer and System Sciences 123 (2022), 122–142.

[47]
Mats Jirstrand, Cylindrical algebraic decomposition-an introduction,
Linköping University, 1995.

[48]
N. Karmarkar, A new polynomial-time algorithm for linear programming,
Combinatorica 4 (1984), no. 4, 373–395.

[49]
Leonid Genrikhovich Khachiyan, A polynomial algorithm in linear
programming, Doklady Akademii Nauk, vol. 244, Russian Academy of Sciences,
1979, pp. 1093–1096.

[50]
Paris C. Kanellakis, Gabriel M. Kuper, and Peter Z. Revesz, Constraint
query languages, Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART
Symposium on Principles of Database Systems, April 2-4, 1990, Nashville,
Tennessee, USA (Daniel J. Rosenkrantz and Yehoshua Sagiv, eds.), ACM
Press, 1990, pp. 299–313.

[51]
Gabriel Kuper, Leonid Libkin, and Jan Paredaens, Constraint databases,
Springer, 2000.

[52]
Victor Klee, Elisabetta Maluta, Clemente Zanco, et al., Basic properties
of evenly convex sets, Journal of Convex Analysis 14 (2007), no. 1,

[53]
Daniel Kroening and Ofer Strichman, Decision procedures, Springer, 2016.

[54]
Bernhard Korte and Jens Vygen, Combinatorial optimization, 5 ed.,
vol. 21, Springer, 2012.

[55]
Leonid Libkin, Some remarks on variable independence, closure, and
orthographic dimension in constraint databases, SIGMOD Rec. 28
(1999), no. 4, 24–28.

[56]
Leonid Libkin, Variable independence, quantifier elimination, and
constraint representations, Automata, Languages and Programming (Berlin,
Heidelberg) (Ugo Montanari, José D. P. Rolim, and Emo Welzl, eds.),
Springer Berlin Heidelberg, 2000, pp. 260–271.

[57]
, Variable independence for first-order definable constraints,
ACM Trans. Comput. Logic 4 (2003), no. 4, 431–451.

[58]
, Elements of finite model theory, Texts in Theoretical Computer
Science. An EATCS Series, Springer Berlin Heidelberg, 2004.

[59]
David Marker, Model theory: an introduction, vol. 217, Springer Science
& Business Media, 2006.

[60]
Jirí Matousek, Lectures on discrete geometry, Graduate texts in
mathematics, Springer, New York, NY, 2013 (eng).

[61]
David Monniaux, A quantifier elimination algorithm for linear real
arithmetic, Logic for Programming, Artificial Intelligence, and Reasoning
(Berlin, Heidelberg) (Iliano Cervesato, Helmut Veith, and Andrei Voronkov,
eds.), Springer Berlin Heidelberg, 2008, pp. 243–257.

[62]
Mattia Montanari, Nik Petrinic, and Ettore Barbieri, Improving the gjk
algorithm for faster and more reliable distance queries between convex
objects, ACM Transactions on Graphics (TOG) 36 (2017), no. 3,

[63]
Ezra Miller and Bernd Sturmfels, Combinatorial commutative algebra,
Graduate texts in mathematics, vol. 277, Springer New York, 2005.

[64]
Oliver Markgraf, Daniel Stan, and Anthony W. Lin, Learning union of
integer hypercubes with queries, Computer Aided Verification (Cham)
(Alexandra Silva and K. Rustan M. Leino, eds.), Springer International
Publishing, 2021, pp. 243–265.

[65]
Greg Nelson and Derek C. Oppen, Simplification by cooperating decision
procedures, ACM Trans. Program. Lang. Syst. 1 (1979), no. 2,

[66]
Derek C. Oppen, Complexity, convexity and combinations of theories,
Theoretical Computer Science 12 (1980), no. 3, 291–302.

[67]
Peter Orlik and Hiroaki Terao, Arrangements of hyperplanes, Springer
Berlin Heidelberg, 1992.

[68]
Andreas Paffenholz, Polyhedral geometry and linear optimization,
Technische Universität Darmstadt (2010).

[69]
M. Presburger, Über die vollständigkeit eines gewissen systems
der arithmetik ganzer zahlen, in welchem die addition als einzige operation
hervortritt, 92–101.

[70]
Jan Paredaens, Jan Van den Bussche, and Dirk Van Gucht, Towards a theory
of spatial database queries (extended abstract), Proceedings of the
Thirteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database
Systems (New York, NY, USA), PODS '94, Association for Computing Machinery,
1994, p. 279–288.

[71]
Peter Z. Revesz, Constraint databases: A survey, Semantics in Databases
(Berlin, Heidelberg) (Bernhard Thalheim and Leonid Libkin, eds.), Springer
Berlin Heidelberg, 1998, pp. 209–246.

[72]
Raghu Ramakrishnan and Johannes Gehrke, Database management systems,
vol. 3, McGraw-Hill New York, 2003.

[73]
Margarita M. L. Rodriguez and José Vicente-Pérez, On finite
linear systems containing strict inequalities, J. Optim. Theory Appl.
173 (2017), no. 1, 131–154.

[74]
Alexander Schrijver, Theory of linear and integer programming, John
Wiley & Sons, 1998.

[75]
Uwe Schöning, Logic for computer scientists, Springer, 2008.

[76]
Michael Sipser, Introduction to the theory of computation, Introduction
to the Theory of Computation, Cengage Learning, 2012.

[77]
Ryan Stansifer, Presburger’s article on integer airthmetic: Remarks and
translation, Tech. Report TR84-639, Cornell University, Computer Science
Department, September 1984.

[78]
Richard P. Stanley, An introduction to hyperplane arrangements,
Geometric combinatorics 13 (2004), no. 389-496, 24.

[79]
David Toman, A point-based temporal extension of sql, International
Conference on Deductive and Object-Oriented Databases, Springer, 1997,
pp. 103–121.

[80]
Katrin Tent and Martin Ziegler, A course in model theory, no. 40,
Cambridge University Press, 2012.

[81]
Moshe Y. Vardi, The complexity of relational query languages (extended
abstract), Proceedings of the Fourteenth Annual ACM Symposium on Theory of
Computing (New York, NY, USA), STOC '82, Association for Computing Machinery,
1982, p. 137–146.

[82]
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, and Sergey Bereg,
Monadic decomposition, J. ACM 64 (2017), no. 2.

[83]
Luc Vandeurzen, Marc Gyssens, and Dirk Van Gucht, On the desirability and
limitations of linear spatial database models, Advances in Spatial Databases
(Berlin, Heidelberg) (Max J. Egenhofer and John R. Herring, eds.), Springer
Berlin Heidelberg, 1995, pp. 14–28.

[84]
Günter M. Ziegler, Lectures on polytopes, vol. 152, Springer Science
& Business Media, 2012.

§ FACTS ABOUT LINEAR DEPENDENCIES

§ ANALYSIS OF THE COVERING ALGORITHM

§ PROOF OF THE OVERSPILLING THEOREM <REF>