PhD Seminar • Software Engineering — Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial ConjecturesExport this event to calendar

Thursday, April 5, 2018 12:00 PM EDT

Edward Zulkoski, PhD candidate
David R. Cheriton School of Computer Science

We present a method and an associated system, called MathCheck, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counter example to the input conjecture. In addition, the combination enables a more efficient encoding of problems than a pure Boolean representation. 

As case studies, we study two open mathematical conjectures from graph theory regarding properties of hypercubes. The first conjecture states that any matching of any d-dimensional hypercube can be extended to a Hamiltonian cycle; the second states that given an edge-antipodal coloring of a hypercube there always exists a monochromatic path between two antipodal vertices. Previous results have shown the conjectures true up to certain low-dimensional hypercubes. We extend these two conjectures to higher-dimensional hypercubes.

Location 
DC - William G. Davis Computer Research Centre
3323
200 University Avenue West

Waterloo, ON N2L 3G1
Canada

S M T W T F S
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
1
2
3
4
5
  1. 2024 (100)
    1. April (23)
    2. March (27)
    3. February (25)
    4. January (25)
  2. 2023 (296)
    1. December (20)
    2. November (28)
    3. October (15)
    4. September (25)
    5. August (30)
    6. July (30)
    7. June (22)
    8. May (23)
    9. April (32)
    10. March (31)
    11. February (18)
    12. January (22)
  3. 2022 (245)
  4. 2021 (210)
  5. 2020 (217)
  6. 2019 (255)
  7. 2018 (217)
  8. 2017 (36)
  9. 2016 (21)
  10. 2015 (36)
  11. 2014 (33)
  12. 2013 (23)
  13. 2012 (4)
  14. 2011 (1)
  15. 2010 (1)
  16. 2009 (1)
  17. 2008 (1)