Title: From Hall’s Marriage Theorem to Boolean Satisfiability and Back

Abstract: I will describe an interesting connection between a famous combinatorial result known as Hall’s Marriage Theorem and Boolean Satisfiability (SAT) via a generalization of the Marriage Problem (the problem that the famous theorem is about) that I call the Fractional Marriage Problem, or FMP. I will describe how Hall's Marriage Theorem and the FMP come up in the context of an important technique in approximability theory known as LP rounding. I will show that the Marriage Problem encodes a new family of polynomially satisfiable SAT formulas, different from the classically known polynomially solvable SAT variants, 2-SAT, Horn-SAT and XOR-SAT. I will then describe a program for dicing up the SAT landscape (or the landscape of any other NP-Complete problem) via translations from problems in P.

Bio: Dr. Jonathan Lenchner has recently returned from a two and a half year stint as chief scientist of IBM's two African research labs, one in Nairobi, Kenya, the other in Johannesburg, South Africa. The labs work focused on computational approaches to healthcare, micro-financing, water security, transparency in dealing with government, and other areas. Together with colleagues, Jon introduced the idea of trading groundwater extraction rights on an open market, an idea that is similar to that of trading carbon credits. IBM, together with two partner organizations are building a system to support such trading in California - work that will then be taken to the Cape Town region of South Africa.  Prior to his time in Africa, Jon worked on the game strategy component of IBM's famous Jeopardy-playing system, worked with the Toronto Raptors of the National Basketball Association to help them with trades and draft picks, and built two robots. Jon's academic interests are in the areas of discrete, combinatorial, and computational geometry.