Dataset supporting the paper: Truth table invariant cylindrical algebraic decomposition

The files in this data set support the paper "Truth table invariant cylindrical algebraic decomposition" by Russel Bradford, James H. Davenport, Matthew England, Scott McCallum and David Wilson. They include the following:

1. A Maple worksheet and library file concerning the Maple results for the worked examples throughout Sections 1-7 of the paper.
2. A zipped directory of files concerning the worked examples from Sections 1-7 of the paper, this time when studied with Qepcad-B.
3. The example set that is the subject of the experiments in Section 8.2 of the paper, whose results were summarised in Table 2, and an example Maple worksheet that uses this set as input.
4. A Maple worksheet that shows how the numbers from Maple in Table 3 in the paper were obtained.
5. A zipped directory of files showing how the numbers from Qepcad-B in Table 3 in the paper were obtained.

Subjects:
Complexity science
Mathematical sciences

Cite this dataset as:
Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D., 2015. Dataset supporting the paper: Truth table invariant cylindrical algebraic decomposition. Bath: University of Bath Research Data Archive. Available from: https://doi.org/10.15125/BATH-00076.

Export

[QR code for this page]

Data

ProjectionCAD.mpl
text/plain (225kB)
Creative Commons: Attribution-Share Alike 4.0

Maple Library file

Section1to7-Maple.mw
application/xml (159kB)
Creative Commons: Attribution-Share Alike 4.0

Maple worksheet for worked examples throughout Sections 1-7 of the paper

Section1to7-Maple.pdf
application/pdf (61kB)
Creative Commons: Attribution-Share Alike 4.0

PDF printout of Maple worksheet for worked examples throughout Sections 1-7 of the paper

Section1to7-Qepcad.zip
application/zip (12kB)
Creative Commons: Attribution-Share Alike 4.0

Qepcad-B files for worked examples throughout Sections 1-7 of the paper

Section82-ExampleSet.txt
text/plain (5kB)
Creative Commons: Attribution-Share Alike 4.0

Example set for experiments in Section 8.2 of the paper

Section82-ExampleSet.mw
application/xml (26kB)
Creative Commons: Attribution-Share Alike 4.0

Maple worksheet for experiments in Section 8.2 of the paper

Section82-ExampleSet.pdf
application/pdf (88kB)
Creative Commons: Attribution-Share Alike 4.0

PDF printout of Maple worksheet for experiments in Section 8.2 of the paper

Section83-Maple.mw
application/xml (59kB)
Creative Commons: Attribution-Share Alike 4.0

Maple worksheet for Table 3 in the paper

Section83-Maple.pdf
application/pdf (17kB)
Creative Commons: Attribution-Share Alike 4.0

PDF printout of Maple worksheet for Table 3 in the paper

Section83-Qepcad.zip
application/zip (15kB)
Creative Commons: Attribution-Share Alike 4.0

Qepcad-B files for Table 3 in the paper

Creators

Russell Bradford
University of Bath

Matthew England
Coventry University

Scott McCallum
Macquarie University

David Wilson
University of Bath

Contributors

University of Bath
Rights Holder

Documentation

Data collection method:

The data collection was by recording cell counts and timings of various CAD algorithms. A full explanation can be found in the associated paper. Regarding the example set in Section82-ExampleSet.txt, we note that the timings for Maple reported in the paper were from running Maple in command line mode. The same example set was tested in Qepcad. Here explicit ECs for a parent formula were entered in dynamically as products of the individual sub-formulae ECs, in cases where an explicit EC exists. Finally, the example set was also tested in Mathematica. Mathematica's CAD command does not return cell counts - these were obtained upon request to a Mathematica developer. Hence they are not recreatable using the information here (something outside the control of the present authors).

Technical details and requirements:

To run the Maple worksheet you will need a copy of the commercial computer algebra software Maple. This is currently available from http://www.maplesoft.com/products/maple/. The examples were run in Maple 16 (released Spring 2012). It is likely that the same results would be obtained in Maple 17, 18, 2015 and future versions, but this cannot be guaranteed. An additional code package, developed at the University of Bath and included in this dataset as `ProjectionCAD.mpl`, is required. If you do not have a copy of Maple you can still read the PDF printout of the worksheets. Qepcad-B is a free piece of software for Linux which can be obtained from http://www.usna.edu/CS/qepcadweb/B/QEPCAD.html.

Additional information:

Within the zipped directories Section1to7-Qepcad.zip and Section83-Qepcad.zip, all the files end in either "-in.txt" or "-out.txt". The former give input for Qepcad and the latter record output. Hence readers without access to Qepcad (e.g. on a Windows system) can still observe the output in the latter files. Within the file Section82-ExampleSet.txt, the 29 examples are defined in the following syntax, used by the TTICAD algorithm that is the subject of the paper: (a) First a line starting with "#" giving the full example name followed in brackets by the shortened name used in Table 2. (b) Then a second line in which the example is defined as a list of two sublists: (i) The first sublist defines the polynomials used. They are sorted into further lists, one for each formulae in the example. Each of these has two entries. The first is either a polynomial defining an equational constraint (EC); a list of polynomials defining multiple ECs; or an empty list (signalling no ECs). The second is a list of any non ECs. (ii) The second sublist is the variable ordering from highest (eliminate first in projection) to lowest. Note that Maple algorithms use this order by Qepcad-B the reverse. This text file doubles as a Maple function definition. When read into Maple the command GenerateInput is defined which can provide the input in formats suitable for the three Maple algorithms tested.

Methodology link:

Bradford, R., Davenport, J. H.., England, M., McCallum, S., and Wilson, D., 2016. Truth table invariant cylindrical algebraic decomposition. Journal of Symbolic Computation, 76, 1-35. Available from: https://doi.org/10.1016/j.jsc.2015.11.002.

England, M., Wilson, D., Bradford, R., and Davenport, J. H., 2014. Using the Regular Chains Library to Build Cylindrical Algebraic Decompositions by Projecting and Lifting. In: Mathematical Software – ICMS 2014. Springer Berlin Heidelberg, 458-465. Available from: https://doi.org/10.1007/978-3-662-44199-2_69.

England, M., and Wilson, D., 2015. An Implementation of Sub-CAD in Maple. Bath U.K.: Department of Computer Science, University of Bath. Available from: https://researchportal.bath.ac.uk/en/publications/an-implementation-of-sub-cad-in-maple.

Documentation Files

README.txt
text/plain (5kB)

Funders

Engineering and Physical Sciences Research Council (EPSRC)
https://doi.org/10.13039/501100000266

Real Geometry and Connectedness via Triangular Description
EP/J003247/1

Publication details

Publication date: 2015
by: University of Bath

Version: 1

DOI: https://doi.org/10.15125/BATH-00076

URL for this record: https://researchdata.bath.ac.uk/id/eprint/76

Related papers and books

Bradford, R., Davenport, J. H.., England, M., McCallum, S., and Wilson, D., 2016. Truth table invariant cylindrical algebraic decomposition. Journal of Symbolic Computation, 76, 1-35. Available from: https://doi.org/10.1016/j.jsc.2015.11.002.

Contact information

Please contact the Research Data Service in the first instance for all matters concerning this item.

Contact person: James Davenport

Departments:

Faculty of Science
Computer Science