Software
Treewidzard - An Engine for Tree-Decomposition-Based Algorithms
Coming Soon.
LUBP - Learning Unitary Branching Programs
Description.
LUBP is a software that implements a heuristic for the construction of unitary branching programs (UBPs) consistent with a given dataset. The idea is that such a UBP may be regarded as a point in a complex Stiefel manifold of appropriate dimension, while the search for an UBP consistent with a given dataset may be regarded as a minimization problem over this manifold. We approach this minimization problem by combining Riemannian gradient descent theory with local optimization.
Download.
Please visit github.com/autoproving/lubp for instructions on how to download, install and use our program.
Citation.
The algorithm implemented in our program is described in detail in the following publication, where you will also find experimental results and a theoretical study of unitary branching programs.
- Unitary Branching Programs: Learnability and Lower Bounds.
Fidel Ernesto Diaz Andino, Maria Kokkou, Mateus de Oliveira Olieira, Farhad Vadiee.
Proceedings of the 38th International Conference on Machine Learning.
3TST - Three-Terminal Steiner Tree
Description.
3TST – Three-Terminal Steiner Tree is a heuristic for the Steiner Tree Problem. Intuitively, the heuristic works by replacing 3-terminal subtrees of a prospective solution with lighter 3-terminal subtrees. This process is repeated until it receives a termination signal. This is a general-purpose Steiner tree heuristic that has performed very well on standard benchmarks when compared with state-or-the-art algorithms on moderate-size instances (up to thousands of vertices). Our solver was also able to handle well very large sparse graphs (with millions of vertices).
Download.
Please visit github.com/autoproving/3tst for instructions on how to download, install and use our program.
Citation.
A detailed description of the heuristic implemented in our program and experimental results can be found in the following publication.
- Three is Enough for Steiner Trees
Emmanuel Arrighi, Mateus de Oliveira Oliveira
19th Symposium on Experimental Algorithms (SEA 2021)
Automated Theorem Proving from the Mindset of Parameterized Complexity Theory
The idea of proving or disproving mathematical statements using automated procedures has been contemplated for at least one century. Nevertheless, even though the field of automated reasoning has reached important milestones during the past few decades, the question of whether computers can significantly speed up the process of proof construction remains elusive.
The goal of this project is to identify a series of numerical parameters that are typically small in humanly produced proofs. Intuitively these parameters are intended to provide a numerical quantification of the complexity of a proof. Using information about these parameters, we will develop new algorithms that will be able to either find a proof of a given predetermined complexity or to determine that no such proof exists.
As a byproduct, we expect that our results will have the potential to improve significantly the automation capabilities of a variety of tools, such as proof assistants, software verification tools, specialist systems, etc.