Finding Reductions Automatically

Abstract. We describe our progress building the program ReductionFinder, which uses off-the-shelf SAT solvers together with the Cmodels system to automatically search for reductions between decision problems described in logic. Key words: Descriptive Complexity, First-Order Reduction, QuantifierFree Reduction, SAT Solver

• Type: Conference
• Year: 2010
• Where: BIRTHDAY
• Authors: Michael Crouch, Neil Immerman, J. Eliot B. Moss
• Keywords: Applied Computing, BIRTHDAY 2010, First-Order Reduction, Off-the-shelf Sat Solvers, Sat Solver