My research interests cover the areas of Computational Logic (CL), Automated Reasoning, Verification, Software Synthesis, Artificial Intelligence (AI) and the application of logic in AI. The main theme of my research is the development and application of different logical frameworks and softwares to perform reasoning in areas such as verification, planning, common-sense reasoning, etc. To further my research, I use tools and tricks from a wide range of areas including both theoretical areas such as model theory and type theory, and more practical areas such as solver development algorithms and software synthesis techniques.
Motivation and Background
Thanks to the ever-growing availability of computational resources in the form of higher clock speeds, more memory, more CPU cores, and grids with more computational units, we are now in a position to solve computational problems that were previously perceived to be forever out of reach. Hence, nowadays, computational research is no longer limited to the boundaries of computer science departments. However, continued development of intensive computing is contingent on the growth of paradigms that make problem solving accessible to everyone.
Model and solve paradigm is the most prominent method to facilitate problem solving by, first, modeling those problems mathematically and, then, using general-purpose solvers to obtain solutions to such mathematical models. This paradigm separates the mathematical structure of a problem from its realization in a computer and, thus, relieves researchers from having to know programming. The model and solve paradigm has already been employed in a variety of fields such as obtaining the true ground state of a physical system through using general-purpose maximum satisfiability (MAXSAT) solvers to solve generalized Ising models [7]. Similarly, in operations research (OR), general-purpose mixed integer program (MIP) solvers are used to optimize industrial processes such as logistical delivery systems [17]. Other examples include using satisfiability (SAT) solvers and satisfiability modulo theory (SMT) solvers to verify the correctness of pieces of hardware and software respectively [18, 12].
The commonality between all the above examples is that the underlying problem is so complex that the only method capable of handling such complexities is a rigorous and tireless search in the space of possible solutions as performed by general-purpose solvers. For instance, when verifying a piece of hardware, we are interested in possible inputs that would cause an undesired output. Non-existence of such an input guarantees the correctness of said hardware. Hence, we use SAT solvers to methodically search for those possible buggy inputs.
The past decade has witnessed the development of many efficient solvers for various computationally complex problems. In many cases, when a general-purpose solver S is applicable to a complex problem P, it outperforms special-purpose solvers developed for P . The reason for such extraordinary performance is found in the amount of engineering that has gone through the years into developing a general-purpose solver. Such an amount of engineering cannot be usually afforded to go into developing any problem-specific solver.
However, existing solvers are not applicable to all problems and, sometimes, one needs to reconfigure an existing solver to suit his/her purposes. Unfortunately, only the experts within solver development communities know how solvers work internally. Therefore, adapting an existing solver to a specific problem is practically infeasible for those outside solver development communities. My research goal is to address such issues.
My research aims to develop model and solve techniques that allow researchers without expertise in solver development to specialize general-purpose solvers for their own particular domain of interest. This way, I intend to bring model and solve paradigm to a wider audience within the scientific computing community.
Problem definition
Despite all the advancements in devising efficient (CDCL-based) solvers, all existing solvers are restricted by a core set of constructs that they support, e.g. clauses in SAT, normal/disjunctive rules in ASP, or available theories in SMT. Thus, solving a complex problem using such solvers involves an encoding of that problem’s constraints using the basic constructs of a solver. Such an encoding process is problematic on two fronts:
- It hinders non-specialists from using that solver because encoding (and, more importantly, efficient encoding) is a non-trivial and cumbersome task; and,
- Usually, encoding a problem loses the structure of that problem and, thus, causes underlying solvers to spend a substantial computational overhead to discover facts that would have been immediate otherwise.
Solutions
During years of research, I have tackled issues (1) and (2) in many different ways. What follows categorizes the various methods that I have used in this regard and it also gives a summary of my previous works regarding each method. The third method, i.e., declarative construction of problem-specific solvers, is a new solution to issues (1) and (2) that I have recently pioneered and constitutes my active area of research.
Solution 1: Extending the language of a solver:
One way to address issues (1) and (2) is to extend the language of a solver with new constructs. Such extensions, firstly, relieve users from having to encode their problem using basic constructs and, secondly, better preserves the structure of a problem. Examples of such language extensions include native handling of cardinality and pseudo-boolean constraints in SAT solvers (also known as PBSAT) as well as the introduction of new theory solvers in SMT. The following summarizes some of my previous works on language extensions:
I) Introducing and Implementing New Declarative Languages. I have worked on two new declarative languages with each language addressing some shortcomings of existing practical KR systems. In an LPAR-2012 publication [11], we introduced Enfragmo as an extension of first-order logic with arithmetic and aggregates and showed how Enfragmo can be used to declaratively specify complex modeling problems and how it can effectively convert arbitrary problem instances into instances of satisfiability problem. Moreover, in a JELIA-2016 publication [1], we introduced first-order clause programs as a declarative paradigm for specifying satisfiability instances in conjunctive normal form. We also introduced satgrnd as a grounding tool for first-order clause programs and showed how satgrnd allows efficient declarative programming by providing unparalleled access to constructs such as recursive definitions and aggregate/conditional atoms.
II) Extending Declarative Languages with Arithmetic. I studied the expressiveness of several practical KR systems in the presence of arithmetic. In particular, I showed that, while many declarative KR languages capture complexity class NP for search problems over the class of finite structures, their expressiveness results fail when they are extended with arithmetic. I showed that, in the presence of arithmetic, such languages can often axiomatize some computationally very hard problems (EXP time complete) while, at the same time, they cannot axiomatize natural arithmetical search problems in NP (such as integer factorization) [15]. I continued this direction in LPAR-2010 [16] where I introduced PBINT: an extension of first-order logic with bounded arithmetic so as to exactly express arithmetical search problems in NP. That is, every search problem involving arithmetic that can be solved in NP can also be axiomatized in PBINT and vice versa.
III) Justifications that Support Reasoning. I studied extensions of classical model theoretic semantics with justifications and showed that, doing so enables us to naturally describe (and also extend) many well-known non-monotonic semantics. In particular, my IJCAI-2013 publication [10] shows that stable models of a disjunctive logic program coincides with those completion models of that logic program that are intuitionistically justified. This gave rise to the the supported semantics for propositional programs: the first extension of stable model semantics that preserves both the minimality and the well-justifiedness of the original stable model semantics. Moreover, in a KR-2014 publication [8], I extended the idea of justifications to multi-context systems (MCS) and showed that the resulting MCS unifies and generalizes both previous main-stream semantics of MCSs, i.e., the equilibrium and the grounded equilibrium semantics.
Solution 2: Combining languages and solvers:
A more recent approach to address issues (1) and (2) is to combine solvers from different communities along with their respective languages. Such a combination of languages allows a non-specialist user to describe a problem’s constraints using the language that is most suited for modeling that constraint. Moreover, by definition, the users have access to many languages at once and they no longer need to encode the constructs of one language using those of another language. Thus, firstly, the problem’s structure will not be lost and, secondly, specialized propagation techniques that are developed for a language can still be used. The following summarizes my research in this area:
IV) Language-independent combination of declarative programs using modular systems. I introduced the framework of modular systems [14] in which every module can use its own language and its own semantics. These modules are combined in a model-theoretical fashion to form more complex modules and represent more complex problems. In [13], I addressed the problem of solving modular systems through a combination of individual solvers for each module.
V) Supported Semantics for Modular Systems. I introduced the idea of justifications to modular systems [9] and I showed that the new supported semantics for modular systems properly extends our model-theoretic semantics. I also showed that, under supported semantics, modular systems can simulate multi-context systems.
Solution 3: Declarative Construction of Problem-specific CDCL Solvers:
The third solution to problems (1) and (2) is to declaratively develop CDCL solvers that are tuned to a specific problem. This solution, that I have pioneered during the last two years, tries to provide a declarative programming framework that can describe both the problem itself (as is usual in declarative programming languages) and the solver that is used to solve this problem. The description of a solver can include new reasoning mechanisms that the solver uses to solve the problem in hand and/or the heuristics that might expedite the solving process. For example, pigeonhole principle’s unsatisfialibity is hard-to-prove using state-of-the-art SAT solvers because resolution is unable to count. Hence, if we declaratively describe the counting principle as a new reasoning mechanism, we will obtain a SAT solver that can easily prove the pigeonhole principle unsatisfiable. In the following, I summarize the papers that I have already published on this subject. This is currently my active area of research and, hence, more papers in this area will be forthcoming.
VI) SAT-to-SAT: a declaratively specializable SAT solver. In a recent AAAI 2016 publication [5], I showed how one can declaratively specialize a SAT solver with a new reasoning mechanism. I implemented a solver, called SAT-to-SAT, using this approach on top of Glucose and showed that problems such as Hamiltonian path can be described more succinctly and solved faster using the approach introduced in this paper. Also, following this trend, in [3, 6], I introduced a new QBF solver based on SAT-to-SAT, called xb-qsts, and showed that its out-of-box performance is comparable to existing state-of-the-art QBF solvers. Moreover, our xb-qsts solver was ranked 2nd in the latest QBF evaluation competition (QBFEval-16). Finally, in an ICLP 2016 publication [2] (which was also fast-tracked for publication in TPLP journal), we extend SAT-to-SAT’s method of describing new reasoning mechanisms to logic programs.
VII) Declarative construction of solvers for new languages. In a recent KR 2016 publication [4], I introduced a new methodology for declarative construction of CDCL-based solver for a new language by just describing the semantics of that languages using second-order logic. We applied this methodology to many existing KR languages and obtained new solvers for those languages. Despite the fact that the declarative description of these solvers were generally limited to only a few lines, we showed that the resulting solver are comparable in performance to existing state-of-the-art solvers for those languages. Two extensions of this work are currently under development. The first extension tries to enable our users to describe more than just the semantics of their new KR languages and the second extension tries to enable our users to also describe grounders for their new languages.
References
[1] Writing Declarative Specifications for Clauses. M. Gebser, T. Janhunen, R. Kaminski, T. Schaub, and S. Tahsharrofi. In proc. of 15th European Conference on Logic in Artificial Intelligence (JELIA’16), 2016.
[2] Stable-unstable Semantics: Beyond NP with Normal Logic Programs. B. Bogaerts, T. Janhunen and S. Tasharrofi. To appear in the proceedings of 32nd International Conference on Logic Programming (ICLP 2016), New York City, USA. 2016. Also, to appear in a special issue of the journal on Theory and Practice of Logic Programming (TPLP), 2016.
[3] SAT-to-SAT in QBFEval 2016. B. Bogaerts, T. Janhunen and S. Tasharrofi. In CEUR Post-proceedings of QBF-2016: International Workshop on Quantified Boolean Formulas. Bordeaux, France. 2016.
[4] Declarative Solver Development: Case Studies. B. Bogaerts, T. Janhunen and S. Tasharrofi. Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), Cape Town, South Africa, pp. 74 – 83, 2016.
[5] SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators. T. Janhunen, S. Tasharrofi, and E. Ternovska. In the proc. of the 30th Conference on Artificial Intelligence (AAAI’16), pp. 978 – 984, 2016.
[6] Solving QBF Instances With Nested SAT Solvers. B. Bogaerts, T. Janhunen and S. Tasharrofi. In the Proceedings of AAAI-16 Workshop on Beyond NP (BNP-16), 2016.
[7] Finding and proving the exact ground state of a generalized Ising model by convex optimization and MAXSAT. W. Huang, D. Kitchaev, S. Dacek, Z. Rong, A. Urban, S. Cao, C. Luo and G. Ceder. In arXiv preprint arXiv:1604.06722, 2016.
[8] Generalized Multi-Context Systems. S. Tasharrofi, and E. Ternovska. In the proc. of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR 2014), pp. 368 – 377, 2014.
[9] Supported Modular Systems. S. Tasharrofi and E. Ternovska. In the proceedings of the 7th workshop on answer set programming and other computing paradigms (ASPOCP 2014), Vienna, Austria, 2014.
[10] A Rational Extension of Stable Model Semantics to the Full Propositional Language. S. Tasharrofi. In the Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13), 2013.
[11] Enfragmo: A system for modelling and solving search problems with logic. A. Aavani, X. Wu, S. Tasharrofi, E. Ternovska, and D. Mitchell. In Proceedings of Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), 2012.
[12] Program Verification as Satisfiability Modulo Theories. N. Bjørner, K. McMillan, and A. Rybalchenko. SMT@ IJCAR-20: International Joint Conference on Automated Reasoning, pp. 3 – 11, 2012.
[13] Solving Modular Model Expansion: Case Studies. S. Tasharrofi, X. Wu, and E. Ternovska. In LNAI Postproceedings of the 19th International Conference on Applications of Declarative Programming and Knowledge Management and 25th Workshop on Logic Programming, 2012.
[14] A Semantic Account for Modularity in Multi-language Modelling of Search Problems. S. Tasharrofi and E. Ternovska. In Proceedings of FroCoS 2011: 8th International Symposium on Frontiers of Combining Systems, 2011.
[15] Built-in Arithmetic in Knowledge Representation Languages. S. Tasharrofi, E. Ternovska. Proc. NonMon at 30 (Thirty Years of Nonmon. Reasoning (Lexington, KY, USA, October 22-25, 2010)
[16] PBINT, a Logic for Modelling Search Problems Involving Arithmetic. S. Tasharrofi, E. Ternovska. Proc. LPAR-17, Yogyakarta (Indonesia) October 10-15, 2010. In ARCoSS subline of LNCS.
[17] The vehicle routing problem: latest advances and new challenges. B. Golden, S. Raghavan, and E. Wasil, eds. Vol. 43. Springer Science & Business Media, 2008.
[18] A survey of recent advances in SAT-based formal verification. M. Prasad, A. Biere, and A. Gupta. International Journal on Software Tools for Technology Transfer 7.2, pp. 156 – 173, 2005.