BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:SAT for the working mathematician - Giles Gardam (University of Bo
 nn)
DTSTART:20250722T151000Z
DTEND:20250722T160000Z
UID:TALK234613@talks.cam.ac.uk
DESCRIPTION:I will discuss solvers for the Boolean satisfiability problem 
 (SAT) as a tool for the working mathematician. SAT is NP-complete which me
 ans it is (in theory) broadly applicable but (in theory) very difficult\, 
 &nbsp\;however modern SAT solvers are able to solve remarkably large probl
 ems in practice. An example of this from my own experience is producing a 
 counterexample to the unit conjecture for group rings\, which had remained
  open for 80 years.&nbsp\;
LOCATION:External
END:VEVENT
END:VCALENDAR