Informal Workshop on Satisfiability Checking and Symbolic Computation (SC-Square)

The use of advanced methods to solve practical and industrially relevant problems by computers has a long history. Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; and more recent developments in the area of Satisfiability Checking are starting to tackle similar problems but with different algorithmic and technological solutions.

Though both communities have made remarkable progress in the last decades, they need to be further strengthened to tackle practical problems of ever increasing size and complexity. Their separate tools (computer algebra systems and SMT solvers) are urgently needed to address prevailing problems having a direct effect on our society. For example, Satisfiability Checking is an essential backend for assuring the security and the safety of computer systems.

In various scientific areas, Symbolic Computation is able to deal with large mathematical problems far beyond the scope of pencil and paper solutions.

Currently the two communities are largely disjoint and unaware of the achievements of one another, despite there being strong reasons for them to discuss and collaborate, since they share many central interests. However, up to now, researchers from these two communities rarely interact, and also their tools lack common, mutual interfaces for unifying their strengths. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction.

These are the main objectives of the SC-square CSA, an EU-funded project whose goal is to initiate cross-fertilization of both fields to allow for combining the knowledge, experience and the technologies in these two communities, to enable the development of radically improved software tools.

General Info

Start: 17 May 2017 15:00
End: 17 May 2017 18:00
Location: Sala Stringa, FBK Povo

Programme

• PASCAL FONTAINE
  Short bio: Pascal Fontaine is an assistant professor (maître de conférence) at Université de Lorraine, Nancy (France) and conducts research within the INRIA group VeriDis, a joint team at LORIA and Max-Planck-Institut für Informatik, Saarbrücken.
  Title: Subtropical satisfiability and off-the-shelf computer algebra as procedures for SMT.
  Abstract: Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose an incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques. We will also report on using an off-the-shelf computer algebra system as a theory reasoner for QF_NRA. Together with subtropical satisfiability and interval constraint propagation, this provides a reasonably strong complete decision procedure.

• JAMES DAVENPORT
  Short Bio: James Davenport studied at Cambridge, getting his PhD "On the Integration of Algebraic Functions" there in 1979: the implementation was in the Reduce computer algebra system. He then went to IBM Yorktown Heights, where he worked on what became the Axiom strongly typed computer algebra system, back to Cambridge, then to Grenoble, where he taught using the Macsyma computer algebra system, and started his book "Calcul Formel". He then moved to the University of Bath in 1983, being at that University for 2/3 of its life. He has also visited many French universities, KTH in Stockholm, Waterloo and Western Ontario in Canada, and New York University. As well as integration and algebra system design, he has worked on polynomial system solving and real algebraic geometry, the last mostly in the Maple computer algebra system. He is the coordinator of the SC-square project.
  Title: Making Cylindrical Algebraic Decomposition more problem-sensitive
  Abstract: Collins' original motivation for Cylindrical Algebraic Decomposition was to solve Quantifier Elimination over the reals, i.e. reduce "forall x{k+1} exists x{k+2}. Phi(x_1...x_n)" to "Psi(x_1...x_k)", where Phi and Psi are boolean combinations of polynomial equalities and inequalities. A CAD for this is also a CAD for any other problem involving the same polynomials with the quantified variables in the same order (but possibly different quantifiers). This seems like overkill. McCallum [1999a] showed how to do better if Phi can be viewed as "f=0 and Phi". This therefore handles "Theta := (f_1=0 and g_1>0) or (f_2=0 and g_2>0)" by writing it as "f_1f_2=0 and Theta". We showed in [Bradford et al 2013b] how to handle Theta directly, and more efficiently. In [Bradford et al 2016a] we extended this to cases like "Xi:=(f_1=0 and g_1>0) or g_2>0", where there is no equational constraint. We will describe these methods, and how they can extend to multiple equational constraints.

• ERIKA ABRAHAM
  Short Bio: Erika Abraham is a full professor at RWTH Aachen University, Germany. She is the head of the research group "Theory of Hybrid Systems". Her research interests include decision procedures, SMT-solving, non-linear optimization, bounded model checking, modeling, synthesis, and analysis of hybrid systems, and analysis of probabilistic systems.
  Title: Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics​
  Abstract: Checking the satisfiability of quantifier-free real-arithmetic formulas is a practically highly relevant but computationally hard problem. Some beautiful mathematical decision procedures implemented in computer algebra systems are capable of solving such problems, however, they were developed for more general tasks like quantifier elimination, therefore their applicability to satisfiability checking is often restricted. In computer science, recent advances in satisfiability-modulo-theories (SMT) solving led to elegant embeddings of such decision procedures in SMT solvers in a way that combines the strengths of symbolic computation methods and heuristic-driven search techniques. In this talk we discuss such embeddings and show that they might be quite challenging but can lead to powerful synergies and open new lines of research.