Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Submitting institution
-
Swansea University / Prifysgol Abertawe
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 28694
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-319-40970-2_15
- Title of conference / published proceedings
- Theory and Applications of Satisfiability Testing – SAT 2016
- First page
- 228
- Volume
- 9710
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- June
- Year of publication
- 2016
- URL
-
http://cs.swan.ac.uk/~csoliver/papers.html#PYTHAGOREAN2016C
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 38
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Expanding the Cube-and-Conquer (C&C) method developed by Kullmann and Heule, this paper presents the most significant application to date of Satisfiability/Constraint Solving to Automated Theorem Proving, solving a long-standing problem of Combinatorics posed by Ron Graham. Besides the core algorithm and its adaptation, a (very large) formal proof of correctness was extracted, which provided strong impetus for further development of methods for extraction of proofs and their verification (based on early work by Kullmann and further developed by Heule). These developments were presented to the general computer science audience in the CACM 2017 paper 'The Science of Brute Force'.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -