Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

SATNet is a differentiable maximum satisfiability (MAXSAT) solver designed to integrate logical reasoning into larger AI systems. In this work we explore the ability to extract and interpret the satisfiability (SAT) clauses learned via SATNet. We introduce a novel regularizer which can be used to coax SATNet weights into an interpretable form, and explore its efficacy through a series of experiments. We postulate the future use of program repair to allow for clause interpretation even where our regularization error is insufficiently small.