# Dataset supporting the paper: Truth table invariant cylindrical algebraic decomposition

These files comprise the data set supporting the following paper: ########################################################################################## Truth table invariant cylindrical algebraic decomposition. Russel Bradford, James H. Davenport, Matthew England, Scott McCallum and David Wilson. http://opus.bath.ac.uk/38146/ ########################################################################################## See the file README.txt or the abstract for more details

The files in this data set support the following paper:

##########################################################################################

Truth table invariant cylindrical algebraic decomposition.

Russel Bradford, James H. Davenport, Matthew England, Scott McCallum and David Wilson.

http://opus.bath.ac.uk/38146/

##########################################################################################

Please find included the following:

##############################

1a) A Maple worksheet: Section1to7-Maple.mw

1b) A pdf printout of the worksheet: Section1to7-Maple.pdf

1c) A Maple Library file: ProjectionCAD.mpl

These files concern the Maple results for the worked examples throughout Sections 1-7 of the paper.

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, is required. To use it we need to read the Maple Library file within Maple as follows:

>>> read("ProjectionCAD.mpl"):

>>> with(ProjectionCAD):

More details on this Maple package are available in the technical report at http://opus.bath.ac.uk/43911/ and in the following publication:

M. England, D. Wilson, R. Bradford and J.H. Davenport. Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting. Proc ICMS 2014 (LNCS 8593). DOI: 10.1007/978-3-662-44199-2_69

If you do not have a copy of Maple you can still read the pdf printout of the worksheet.

##############################

2) A zipped directory WorkedExamples-Qepcad.zip

This directory also concerns the worked examples from Sections 1-7 of the paper, this time when studied with Qepcad-B.

Qepcad-B is a free piece of software for Linux which can be obtained from:

http://www.usna.edu/CS/qepcadweb/B/QEPCAD.html

All the files in the zipped directory 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.

To verify the output readers should use the following bash command to run a Qepcad input file "Ex-in.txt" and record the output in "Ex-out.txt".

>>> qepcad +N500000000 +L200000 < Ex-in.txt > Ex-out.txt

Windows users without Linux access can still read the existing output files in the folder.

##############################

3a) The text file: Section82-ExampleSet.txt

3b) A Maple worksheet: Section82-ExampleSet.mw

3b) A pdf printout of the worksheet: Section82-ExampleSet.pdf

The textfile defines the example set which is the subject of the experiments in Section 8.2, whose results were summarised in Table 2. Within the file the 29 examples are defined in the following syntax:

(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 the reverse.

This is the syntax used by the TTICAD algorithm that is the subject of the paper.

The 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. An example is given in the Maple worksheet / pdf. We note that the timings reported in the paper were from running Maple in command line mode. See also the notes for files (1) above.

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. See also Qepcad notes for file (2) above.

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).

##############################

4a) A Maple worksheet: Section83-Maple.mw

4b) A pdf printout of the worksheet: Section83-Maple.pdf

This shows how the numbers in Table 3 from Maple were obtained.

See also notes for files (1) above.

##############################

5a) A zipped directory Section83-Qepcad.zipped

This shows how the numbers in Table 3 from Qepcad were obtained.

See also notes for file (2) above.

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

## Data

ProjectionCAD.mpl

text/plain (225kB)

Creative Commons: Attribution-Share Alike 4.0

Section1to7-Maple.mw

application/xml (159kB)

Creative Commons: Attribution-Share Alike 4.0

Section1to7-Maple.pdf

application/pdf (61kB)

Creative Commons: Attribution-Share Alike 4.0

Section1to7-Qepcad.zip

application/zip (12kB)

Creative Commons: Attribution-Share Alike 4.0

Section82-ExampleSet.txt

text/plain (5kB)

Creative Commons: Attribution-Share Alike 4.0

Section82-ExampleSet.mw

application/xml (26kB)

Creative Commons: Attribution-Share Alike 4.0

Section82-ExampleSet.pdf

application/pdf (88kB)

Creative Commons: Attribution-Share Alike 4.0

Section83-Maple.mw

application/xml (59kB)

Creative Commons: Attribution-Share Alike 4.0

Section83-Maple.pdf

application/pdf (17kB)

Creative Commons: Attribution-Share Alike 4.0

Section83-Qepcad.zip

application/zip (15kB)

Creative Commons: Attribution-Share Alike 4.0

All data are available under a CC-BY-SA 4.0 licence

## Creators

Russell Bradford

University of Bath

James Davenport

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:

Cell counts and timings of various CAD algorithms.

## 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, pp.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

Faculty of Science

Computer Science