Satisfiability modulo theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulae over different theories. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. Here a commonly used tool is the cylindrical algebraic decomposition (CAD) to decompose the real space into cells where the constraints are truth-invariant through the use of projection polynomials. A CAD encodes more information than necessary for checking satisfiability. One approach to address this is to repackage the CAD theory into a search-based algorithm: one that guesses sample points to satisfy the formula, and generalizes guesses that conflict constraints to cylindrical cells around samples which are avoided in the continuing search. Such an approach can lead to a satisfying assignment more quickly, or conclude unsatisfiability with far fewer cells. A notable example of this approach is Jovanović and de Moura's NLSAT algorithm. Since these cells are being produced locally to a sample there is scope to use fewer projection polynomials than the traditional CAD projection. The original NLSAT algorithm reduced the set a little; while Brown's single cell construction reduced it much further still. However, it refines a cell polynomial-by-polynomial, meaning the shape and size of the cell produced depends on the order in which the polynomials are considered. The present paper proposes a method to construct such cells levelwise, i.e. built level-by-level according to a variable ordering instead of polynomial-by-polynomial for all levels. We still use a reduced number of projection polynomials, but can now consider a variety of different reductions and use heuristics to select the projection polynomials in order to optimize the shape of the cell under construction. The new method can thus improve the performance of the NLSAT algorithm. We formulate all the necessary theory that underpins the algorithm as a proof system: while not a common presentation for work in this field, it is valuable in allowing an elegant decoupling of heuristic decisions from the main algorithm and its proof of correctness. We expect the symbolic computation community may find uses for it in other areas too. In particular, the proof system could be a step towards formal proofs for non-linear real arithmetic. This work has been implemented in the SMT-RAT solver and the benefits of the levelwise construction are validated experimentally on the SMT-LIB benchmark library. We also compare several heuristics for the construction and observe that each heuristic has strengths offering potential for further exploitation of the new approach.

Cylindrical Algebraic Decomposition (CAD) is an established tool in the computer algebra community for computing with semi-algebraic sets / Tarski formulas. The key property of CAD is that it provides a representation in which geometric projection and set complement (the analogues of the logical operations of quantifier elimination and negation for Tarski formulas) are trivial. However, constructing a CAD often requires an impractical amount of time and space. Non-uniform CAD (NuCAD) was introduced with the goal of providing a more practically efficient alternative to CAD for computing with semi-algebraic sets / Tarski formulas. As a first step towards that goal, previous work has shown that Open NuCADs do provide a much more efficient representation than Open CADs. However, it hasn't been shown that the key operation of projection can be computed efficiently in the NuCAD representation, because while set complement is trivial for NuCADs, as it is for CADs, projection, in contrast to the CAD case, is not. This paper provides another step towards the larger goal by showing how projection can be done efficiently in the Open NuCAD representation. The importance of this contribution is not restricted to Open NuCADs, since the same approach to projection will carry over to the general case for NuCADs where, we hope, the practical benefits of the much smaller representation NuCAD provides will be even greater.

This paper introduces the notion of an Open Non-uniform Cylindrical Algebraic Decomposition (NuCAD), and presents an efficient model-based algorithm for constructing an Open NuCAD from an input formula. Using a limited experimental implementation of the algorithm, we demonstrate the effectiveness of the approach. NuCAD generalizes Cylindrical Algebraic Decomposition (CAD) as defined by Collins in his seminal work from the early 1970s, and extended in concepts like Hong's partial CAD. A NuCAD, like a CAD, is a decomposition of Rn into cylindrical cells. But unlike a CAD, the cells in a NuCAD need not be arranged cylindrically. It is in this sense that NuCADs are not uniformly cylindrical. However, NuCADs, like CADs, carry a tree-like structure that relates different cells. It is a very different tree but, as with the CAD tree structure, it allows some operations to be performed efficiently, for example locating the containing cell for an arbitrary input point.

In this work we describe how a message board can be used to teach a number of important concepts in cyber security in a novel and hands-on manner. The message board is used daily in class and serves the routine functions of disseminating information to students, offering a forum for interactive discussions, allowing a convenient method to copy and paste complex expressions, providing a venue for class interaction, permitting archiving of information, and serving as a general blackboard. We use the message board to illustrate and teach important cyber-security concepts and common attacks such as the following: authentication and cookies, cross-site scripting and injection attacks, man-in-the-middle attack on public-key cryptography, password selection, and password-file management. From the student-learning perspective the tool appears to work very well. We hope that others can make use of the message board in their lessons or incorporate parts of it to improve the educational experience of their students. The message board can be integrated seamlessly into a class to enhance hands-on learning.

This paper presents an algorithm that, roughly speaking, constructs a single open cell from a cylindrical algebraic decomposition (CAD). The algorithm takes as input a point and a set of polynomials, and computes a description of an open cylindrical cell containing the point in which the input polynomials have constant non-zero sign, provided the point is sufficiently generic. The paper reports on a few example computations carried out by a test implementation of the algorithm, which demonstrate the functioning of the algorithm and illustrate the sense in which it is more efficient than following the usual "open CAD" approach. Interest in the problem of computing a single cell from a CAD is motivated by a 2012 paper of Jovanovic and de Moura that require solving this problem repeatedly as a key step in NLSAT system. However, the example computations raise the possibility that repeated application of the new method may in fact be more efficient than the usual open CAD approach, both in time and space, for a broad range of problems.

Due to the high priority of cyber-security education, the United States Naval Academy rapidly developed and implemented a new cyber-security course that is required for all of its first-year students. During the fall semester in 2011, half of the incoming class (about 600 students) took the course through a total of 31 sections offered by 16 instructors from a variety of disciplines and backgrounds. In the following spring semester, the remaining half of the first-year students will take the course. This paper explains the motivation that instigated and drove course development, the curriculum, teaching mechanics implemented, personnel required, as well as challenges and lessons learned from the first offering of the course. The information contained in this paper will be useful to those thinking of implementing a technical course required of all students at the same level in an institution (in our case first-year students) and particularly those interested in implementing such a course in cyber security.

This paper describes a new method for simplifying Tarski formulas. The method combines simplifications based purely on the factor structure of inequalities ("black-box" simplification) with simplifications that require reasoning about the factors themselves. The goal is to produce a simplification procedure that is very fast, so that it can be applied --- perhaps many, many times --- within other algorithms that compute with Tarski formulas without ever slowing them down significantly, but which also produces useful simplification in a substantial number of cases. The method has been implemented and integrated into implementations of two important algorithms: quantifier elimination by virtual term substitution, and quantifier elimination by cylindrical algebraic decomposition. The paper reports on how the simplification method has been integrated with these two algorithms, and reports experimental results that demonstrate how their performance is improved.

We developed a new model for iList, our system that helps students learn linked list. The model is automatically extracted from past student data, and allows iList to track students' problem-solving behavior in order to provide targeted feedback. We evaluated the new model both intrinsically and extrinsically. We show that the model can match most student actions after a relatively small sequence of observations, and that iList can effectively use the new student tracker to provide feedback and help students learn.

We define the "combinatorial part" of a Tarski formula in which equalities and inequalities are in factored or partially-factored form. The combinatorial part of a formula contains only "monomial inequalities", which are sign conditions on monomials. We give efficient algorithms for answering some basic questions about conjunctions of monomial inequalities and prove the NP-Completeness/Hardness of some others.

Let V ⊂ Rr denote the real algebraic variety defined by the conjunction f = 0 ∧ g = 0, where f and g are real polynomials in the variables x1, ..., xr and let S be a submanifold of Rr-2. This paper proposes the notion of the analytic delineability of V on S with respect to the last 2 variables. It is suggested that such a notion could be useful in solving more efficiently certain quantifier elimination problems which contain the conjunction f = 0 ⊂ g = 0 as subformula, using a variation of the CAD-based method. Two bi-equational lifting theorems are proved which provide the basis for such a method.

This paper has two parts. In the first part we give a simple and constructive proof that quantifier elimination in real algebra is doubly exponential, even when there is only one free variable and all polynomials in the quantified input are linear. The general result is not new, but we hope the simple and explicit nature of the proof makes it interesting. The second part of the paper uses the construction of the first part to prove some results on the effects of projection order on CAD construction -- roughly that there are CAD construction problems for which one order produces a constant number of cells and another produces a doubly exponential number of cells, and that there are problems for which all orders produce a doubly exponential number of cells. The second of these results implies that there is a true singly vs. doubly exponential gap between the worst-case running times of several modern quantifier elimination algorithms and CAD-based quantifier elimination when the number of quantifier alternations is constant.

This paper presents RegeXeX (Regular expression exercises), an interactive system for teaching students to write regular expressions. The system poses problems (prose descriptions of languages), students enter solutions (regular expressions defining these languages), and the system provides feedback. What is novel in this system is the type of feedback: students are not merely told that a submitted regular expression is wrong, they are given examples of strings that the expression either matches and shouldn't or does not match and should, and asked to try again. Additionally, student responses need only be equivalent to the solution, not identical. Results of classroom experience with this system are also reported, and demonstrate its effectiveness in teaching students to write regular expressions with little or no instructor interaction.RegeXeX is a freely available, portable system, written in C++ and using the Qt library for its GUI. It is distributed with several exercise sets, but is designed so instructors can easily write their own. The system logs student work and offers facilities for submitting log-files to instructors as well, allowing for automatic grading, or in-depth analysis of student performance and evolution of responses throughout the exercise set.

This paper introduces an improved method for constructing cylindrical algebraic decompositions (CADs) for formulas with two polynomial equations as implied constraints. The fundamental idea is that neither of the varieties of the two polynomials is actually represented by the CAD the method produces, only the variety defined by their common zeros is represented. This allows for a substantially smaller projection factor set, and for a CAD with many fewer cells.In the current theory of CADs, the fundamental object is to decompose n-space into regions in which a polynomial equation is either identically true or identically false. With many polynomials, one seeks a decomposition into regions in which each polynomial equation is identically true or false independently. The results presented here are intended to be the first step in establishing a theory of CADs in which systems of equations are fundamental objects, so that given a system we seek a decomposition into regions in which the system is identically true or false --- which means each equation is no longer considered independently. Quantifier elimination problems of this form (systems of equations with side conditions) are quite common, and this approach has the potential to bring large problems of this type into the scope of what can be solved in practice. The special case of formulas containing two polynomial equations as constraints is an important one, but this work is also intended to be extended in the future to the more general case.

This paper presents an improved projection operator for the construction of CAD's of R3. It is shown that, typically, it suffices to include in projection only leading coefficients (along with discriminants and resultants) rather than all coefficients. Cases in which the leading coefficient alone does not suffice can be dealt with, in a sense, even more efficiently. Generalizing the improved projection operator to dimension greater than three is a topic of ongoing research.

Article Free Access Share on Guaranteed solution formula construction Author: Christopher W. Brown Department of Computer and Information Sciences, University of Delaware Department of Computer and Information Sciences, University of DelawareView Profile Authors Info & Claims ISSAC '99: Proceedings of the 1999 international symposium on Symbolic and algebraic computationJuly 1999 Pages 137–144https://doi.org/10.1145/309831.309890Published:01 July 1999Publication History 9citation229DownloadsMetricsTotal Citations9Total Downloads229Last 12 Months15Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Article Free Access Share on Simplification of truth-invariant cylindrical algebraic decompositions Author: Christopher W. Brown Department of Computer and Information Sciences, University of Delaware Department of Computer and Information Sciences, University of DelawareView Profile Authors Info & Claims ISSAC '98: Proceedings of the 1998 international symposium on Symbolic and algebraic computationAugust 1998 Pages 295–301https://doi.org/10.1145/281508.281652Published:01 August 1998Publication History 10citation211DownloadsMetricsTotal Citations10Total Downloads211Last 12 Months14Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF