publications
2026
- Tao’s Equational Proof Challenge Accepted (Work in progress)Lydia Kondylidou, Jasmin Blanchette, and Marijn J.H. Heule2026
In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.
- Enumerating Choice Terms in Model-Based Quantifier InstantiationLydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, and 1 more authorIn TACAS, 2026
Satisfiability modulo theories (SMT) solvers are widely used for determining the satisfiability of logical formulas with respect to back- ground theories. SMT solvers are traditionally based on first-order logic, but some also support higher-order logic. Recently, Kondylidou et al. introduced model-based quantifier instantiation with fast enumeration (MBQI-Enum), a quantifier instantiation strategy that works for both logics. A weakness of MBQI-Enum is that it does not find refutations when Hilbert choice terms are necessary. In this work, we present an extension of MBQI-Enum that enables it to reason effectively about Hilbert’s choice operator. The extended strategy substantially increases the success rate of the SMT solver cvc5 on higher-order benchmarks.
2025
- Augmenting Model-Based Instantiation with Fast EnumerationLydia Kondylidou, Andrew Reynolds, and Jasmin BlanchetteIn TACAS, 2025
Satisfiability-modulo-theories (SMT) solvers rely on various quantifier instantiation strategies to support first- and higher-order logic. We introduce MBQI-Enum, an approach that extends model-based quan- tifier instantiation (MBQI) with syntax-guided synthesis (SyGuS) tech- niques. Our approach targets first-order theories without well-established quantifier instantiation techniques and higher-order quantifiers that can benefit from instantiations with λ-terms. By incorporating a SyGuS enu- merator, it generates a broader set of candidate instantiations, including identity functions and terms containing uninterpreted symbols, thereby improving the effectiveness of MBQI.
2023
- Supporting a CDCL Sat Solver by BDD Methods - Masters ThesisLydia KondylidouJan 2023
Boolean satisfiability (SAT) is one of the most important problems of theoretical computer science with many practical applications in which Boolean Satisfiability (SAT) solvers are used in the background as high-performance reasoning engines. These applications include automated planning and scheduling, formal verification, and automated theorem proving. In the last decades, the performance of state-of-the-art SAT solvers has increased dramatically, thanks to the invention of advanced heuristics, preprocessing and inprocessing techniques, and data structures that allow efficient implementation of search space pruning. The in- creasing popularity of SAT in verification and synthesis encourages the search for additional speed-ups. This paper presents a new approach to support a Conflict Driven Clause Learning (CDCL) SAT solver with Binary Decision Diagram (BDD) techniques. While SAT and BDD techniques are often presented as mutually exclusive alternatives, this work points out that both can be improved by running in parallel and exchanging information. In this thesis, a BDD library is implemented in Rust, designed to support the latest version of the Glucose SAT solver. The proposed methods are based on efficient communication between the two architectures. Several benchmarks from the SAT competitions are run both on Glucose alone and Glucose with the contribution of the BDDs, and the results are compared. Eventually, the experiments show that the performance of Glucose is improved when running in parallel with the BDD solver.
2021
- Implementation and Comparison of Substitution Trees and Instance Tries - Bachelors ThesisLydia KondylidouMar 2021
Term indexing methods have a major impact on the speed of logic programming lan- guages and automated theorem proving systems. Substitution trees are well estab- lished term indexes for logic programming and theorem proving because of their per- formances. However, they rely on heuristics and ignore the partial order that is in- herent to terms. On the other hand, instance tries have been recently proposed as a novel term index for logic programming and automated theorem proving. Instance tries make use of the term order without having to resort to heuristics. In this bache- lor’s thesis, the efficiency of instance tries is examined in more detail on the basis of established benchmarks and and it is compared with that of substitution trees.