ABSTRACT. The theory and practice of satisfiability solvers has experienced dramatic advances in the past couple of decades. This fact attracted the attention of researchers that work with hard combinatorial problems with the hope that if suitable and efficient SAT encodings of these problems can be established, then SAT solvers can be used to solve large instances of such problems effectively. On the other hand SAT researchers have been interested in hard combinatorial problems and produced significant breakthroughs using custom-tailored highly-tuned SAT solvers implementations. It turns out that both these approaches have had a number of successes already and it is safe to assume that a lot more successes are to be expected in the near future. Combinatorics is a vast source of very hard and challenging problems, often containing thousands of discrete variables, and i firmly believe that the interaction between SAT researchers and combinatorialists will continue to be very fruitful.

ABSTRACT. Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems for polynomial systems over the reals. It has long been studied by the Symbolic Computation community, and has found recent interest in the Satisfiability Checking community.

The present report describes a proof of concept implementation of an Incremental CAD algorithm in \textsc{Maple}, where CADs are built and then refined as additional polynomial constraints are added. The aim is to make CAD suitable for use as a theory solver for SMT tools who search for solutions by constantly reformulating logical formula and querying whether a logical solution is admissible.

We describe experiments for the proof of concept, which clearly display the computational advantages compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard valuation).

ABSTRACT. The cylindrical algebraic decomposition is a popular method for quantifier elimination for non-linear real algebra. We use it as a theory solver in the context of satisfiability-modulo-theories solving to solve a sequence of related problems consisting of a conjunction of constraints. To improve our technique in practice, we consider different optimizations in the projection phase based on equational constraints.

We review the existing ideas and propose how to modify an existing implementation. Though one could expect a significant speed-up for large problems, we discuss why our expectations are somewhat lower, in particular, because satisfiable problems tend not to benefit from the modifications at all. Finally, we evaluate several different implementations and demonstrate a significant improvement due to the usage of equational constraints.

ABSTRACT. In this paper we consider formulas that are conjunctions of linear clauses, i.e., of linear equations. Such formulas are very interesting because they encode CNF constraints that are typically very hard for SAT solvers. We introduce a new proof system SRES that works with linear clauses and show that SRES is implicationally and refutationally complete. Algebraically speaking, linear clauses correspond to products of linear polynomials over a ring of Boolean polynomials. That is why SRES can certify if a product of linear polynomials lies in the ideal generated by some other such products, i.e., the SRES calculus decides the ideal membership problem. Furthermore, an algorithm for certifying inconsistent systems of the above shape is described. We also establish the connection with an another combined proof system R(lin).

ABSTRACT. We consider problems originating in economics that may be solved automatically using mathematical software. We present and make freely available a new benchmark set of such problems. The problems have been shown to fall within the framework of non-linear real arithmetic, and so are in theory soluble via Quantifier Elimination (QE) technology as usually implemented in computer algebra systems. Further, they all can be phrased in prenex normal form with only existential quantifiers and so are also admissible to those Satisfiability Module Theory (SMT) solvers that support the QF_NRA logic. There is a great body of work considering QE and SMT application in science and engineering, but we demonstrate here that there is potential for this technology also in the social sciences.

ABSTRACT. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale verification of arithmetic gate-level circuits, such as multipliers, to large bit-widths. There is also a large body of work on theoretical aspects of propositional algebraic proof systems in the proof complexity community starting with the seminal paper introducing the polynomial calculus. We show that the polynomial calculus provides a frame-work to define a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level verification of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked efficiently with independent tools.

ABSTRACT. Unknot recognition is one of the fundamental questions in low dimensional topology. In this work, we show that this problem can be encoded as a validity problem in the existential fragment of the first-order theory of real closed fields. This encoding is derived using a well-known result on \su representations of knot groups by Kronheimer-Mrowka. We further show that applying existential quantifier elimination to the encoding enables an \unknot algorithm with a complexity of the order $2^{\OO(n)}$, where $n$ is the number of crossings in the given knot diagram. Our algorithm is simple to describe and has the same runtime as the currently best known unknot recognition algorithms. This leads to an interesting class of problems, of interest to both SMT solving and knot theory.

ABSTRACT. CoCoALib is a C++ software library offering operations on polynomials, ideals of polynomials, and related objects. The principal developers of CoCoALib are members of the SC-square project. We give an overview of the latest developments of the library, especially those relating to the project SC-square.

The CoCoA software suite includes also the programmable, interactive system CoCoA-5. Most of the operations in CoCoALib are also accessible via CoCoA-5. The programmability of CoCoA-5 together with its interactivity help in fast prototyping and testing conjectures.

ABSTRACT. One does not need the gift of clairvoyance to predict that in the near future autonomously driving cars will occupy a significant place in our everyday life. In fact, in designated and even public test-drive areas it is reality even now. Autonomous driving comes with the ambition to make road traffic safer, more efficient, more economic, and more comfortable -- and thus to ``make the world a bit better''. Recent accidents with automatic cars resulting in severe injuries and death, however, spark a debate on the safety validation of autonomous driving in general. The biggest challenge for autonomous driving to become a reality is thus most likely not the actual development of intelligent vehicles themselves but their rigorous validation that would justify the necessary level of confidence. It is common sense that classical test approaches are by far not feasible in this emerging area of autonomous driving as these would induce billions of kilometers of real-world driving in each release cycle. To cope with the tremendous complexity of traffic situations that a self-driving vehicle must deal with -- without doing any harm to any other traffic participants -- a promising approach to safety validation is virtual simulation, i.e.\ driving the huge amount of test kilometers in a virtual but realistic simulation environment. A particular interest here is in the validation of the behavior of the autonomous car in rather critical traffic scenarios.

In this position paper, we concentrate on one important aspect in virtual safety validation of autonomous driving, namely on the specification and concretization of critical traffic scenarios. This aspect gives rise to complex and challenging constraint systems to be solved, to which we believe the SC$^2$ community may give essential contributions by their rich variety of diverse methods and techniques.

ABSTRACT. We report on a prototypical tool for Satisfiability Modulo Theory solving for quantifier-free formulas in Non-linear Real Arithmetic or, more precisely, real closed fields, which uses a computer algebra system as the main component. This is complemented with two heuristic techniques, also stemming from computer algebra, viz.~interval constraint propagation and subtropical satisfiability. Our key idea is to make optimal use of existing knowledge and work in the symbolic computation community, reusing available methods and implementations to the most possible extent. Experimental results show that our approach is surprisingly efficient in practice.

ABSTRACT. The recognition that Symbolic Computation tools could benefit from techniques from the world of Satisability Checking was a primary motivation for the founding of the SC2 community. These benefits could be further demonstrated by the existence of "SMT-like" queries in legacy computer algebra systems; that is, computations which seek to decide satisfiability or identify a satisfying witness.

The Maple CAS has been under continuous development since the 1980s and its core symbolic routines incorporate many heuristics, some of which are "SMT-like". We describe ongoing work to compose an inventory of such "SMT-like" queries extracted from the built-in Maple library, most of which were added long before the inclusion in Maple of explicit software links to SAT/SMT tools. Some of these queries are expressible in the SMT-LIB format using existing logics, and it hoped that an analysis of those that cannot be so expressed could help inform future development of the SMT-LIB standard.

ABSTRACT. Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non-clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms. We demonstrate on a concrete example several heuristic techniques for the automation of natural-style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra. Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behaviour in zero, bounding the epsilon-bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions. These techniques are being implemented in the Theorema system and are able to construct automatically natural-style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.