Research
Given below is the list of our current research projects with their brief descriptions and the people involved.
ArgoSAT
ArgoSAT is freely available and open source SAT solver developed under the terms of GPL licence. It aims to serve as a flexible platform for making various experiments in the field of SAT solving. The solver consists of a DPLL based core, extended with multiple satellite components implementing various heuristics (e.g., for decision literal and variable selection, for restarting, for managing the clause database) and various additional features (e.g., logging, progress tracking, GUI interaction). The DPLL core is based on abstract transition rules given by S. Krstic and A. Goel, and is verified within the Isabelle theorem prover.
ArgoSmArT
We are developing ArgoSmArT, a system for choosing suitable parameters' values for ArgoSAT solver. The system could be used for any SAT solver with minor modfications. It uses data mining techniques for choosing parameters' values based on syntactical structure of a boolean formula being solved. The current version of ArgoSmArT has achieved significant improvements in performance compared to it's base solver and we are working on further development.
This system is a part of a larger research direction of speeding up and analyzing SAT solvers using data mining, machine learning, and statistical techniques. Some of the ongoing and planned research tasks are:
- stochastic optimization of parameters' values for various families of boolean formulae which would improve performance of ArgoSmArT
- statistical analysis of behavior of parameters and their interactions which would deepen our understanding of SAT solver functioning, and point to good ways of combining heuristics that modern SAT solvers use
- learning to control SAT solver by reinforcement learning
- finding new variable selection strategies based on data mining tehcniques
- making deeper insights into the nature of SAT solving process
ArgoSMT
ArgoSMT (which is still in early phases of its development) is an open source, freely available SMT solver developed under the terms of GPL licence. It uses ArgoSAT as its propositional engine. Once fully developed, it will implement decision procedures for several background theories, including theories commonly used for SMT (e.g., EUF, LRA, LIA, and Bitvectors), and some novel theories motivated by applications (e.g., AllDifferent). It will also support Nelson-Oppen scheme for cooperating decision procedures. The main design goal of ArgoSMT is to make it flexible and allowing users to easily make its extensions. It will also serve as a research platform for making various experiments in the field of SMT solving. Its predecessors are the ArgoLib decision procedures library and GS framework.
Applications of SAT and SMT solvers
Our research also focuses on applications of SAT/SMT solving in solving optimization problems. Our proprietary tool ArgoTimetables, based exclusively on SAT solving, has successfully generated teaching timetables for several high-schools and universities in Belgrade, including the (Faculty of Mathematics). Also we have applied SAT solving techniques for logical criptoanalysis.
Formalisation and Verification of SAT/SMT Solvers
Since SAT/SMT solvers are used in applications that are very sensitive, their misbehavior could be both economically expensive and dangerous from the aspect of safety. Therefore, having trusted SAT/SMT solvers working in wider systems is vital. This can be achieved in two different ways: (i) extend solvers with the possibility of generating evidences for their claims (models for satisfiable input formulae and proofs of unsatisfiability for unsatisfiable input formulas), which are then checked by independent trusted checkers; and (ii) apply software verification techniques and verify the implementation of SAT/SMT solvers themselves.
We have verified a modern DPLL procedure, featuring conflict analysis, clause learning and two-watch unit propagation scheme, which is a base of most state-of-the-art SAT and SMT solvers. The proof documents are available from Archive of Formal Proofs and from a local repository. Our current and future research focuses on efficient code generation from Isabelle specification. We plan to generate both full SAT solvers and unsatisfiability proof checkers based on some DPLL techniques. We also plan to verify some algorithms and techniques used in SMT solving and generate verified SMT solvers.
GCLC/WinGCLC
GCLC (from "Geometry Constructions->LaTeX converter") is a tool for visualizing and teaching geometry, and for producing mathematical illustrations. Its basic purpose is converting descriptions of mathematical objects (written in the GCL language) into digital figures. GCLC provides easy-to-use support for many geometrical constructions, isometric transformations, conics, and parametric curves. The basic idea behind GCLC is that constructions are formal procedures, rather than drawings. Thus, in GCLC, producing mathematical illustrations is based on "describing figures" rather than of "drawing figures". This approach stresses the fact that geometrical constructions are abstract, formal procedures and not figures. A figure can be generated on the basis of abstract description, in the Cartesian model of a plane. These digital figures can be displayed and exported to LaTeX files (or some other format). WinGCLC is the Windows version of GCLC and provides a range of additional functionalities.
More about GCLC can be found on the GCLC page.
Geometrical Theorem Proving
Formalizations of Euclidean geometry within proof assistants (Isabelle and Coq) have already been developed for several axiom systems, such as Hilbert's one and Tarski's one. These formalizations are important for building formalized mathematical knowledge base, but also in mathematical education and in applications of computational geometry. We are developing a method for automated proving of theorems of Euclidean geometry. The method is based on simple forward-chaining, but should still prove a large number of theorems and export proofs to proof assistants such as Isabelle. We also implemented Chou's area method, Wu's method, and Groebner bases method for geometrical theorem proving and we are working on their different extensions.
LAV
LAV is a software verification tool built on top of the LLVM compiler infrastructure, and available under the UIUC open source license.
LAV combines symbolic execution, SAT encoding of program's behavior and some features of bounded model checking. Namely, single blocks of the code are modelled by first-order logic formulae constructed by symbolic execution, while relationships between blocks are modelled by propositional formulae. Formulae that describe blocks' behavior are combined with correctness conditions for individual commands to produce correctness conditions of the program to be verified. These conditions are passed to a SMT solver covering a suitable combination of theories. There is support for export to linear arithmetic, bit-vector arithmetic, the theory of uninterpreted functions (and Ackermannization, as its alternative), and the theory of arrays. LAV can use the following SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments suggest that the presented approach is competitive with related tools, so it can be used as a useful alternative for some sorts of verification tasks.
For more information on what LAV is and what it can do, see the LAV page.
meSAT
System meSAT (multiple encodings of CSP to SAT) is freely available and open source CSP solver developed under the terms of GPL licence. The system translates specifications of finite linear CSP problems into SAT instances using several well-known encodings, and their combinations. The system also performs reduction to SMT and PB. A methodology for selecting a suitable encoding based on simple syntactic features of the input CSP instance is also developed.
More information on meSAT can be found on meSAT page.
SpeCS
SpeCS is a sound and complete SPARQL query containment solver. The approach reduces the query containment problem to the satisfiability problem in FOL and therefore enables the usage of state of the art SMT solvers (SpeCS uses Z3 solver). It covers the most common SPARQL language constructs (conjunctive and cyclic queries, union, filter, from clauses, blank nodes and projections, bind, subqueries, optional, minus, graph, expressions within select clause, builtin functions, etc.) and reasoning under RDF SCHEMA entailment regime. The containment problem can be considered in both standard and subsumption form. Renaming of projection variables is also supported.
For more information, see SpeCS page.