Finding unsatisfiable cores of a set of polynomials using the Gröbner basis algorithm

Abstract

Finding small unsatisfiable subformulas (unsat cores) of infeasible propositional SAT problems is an active area of research. Analogous investigations in the polynomial algebra domain are, however, somewhat lacking. This paper investigates an algorithmic approach to identify a small unsatisfiable core of a set of polynomials, where the corresponding polynomial ideal is found to have an empty variety. We show that such a core can be identified by employing extensions of the Buchberger’s algorithm. By further analyzing S-polynomial reductions, we identify certain conditions that are helpful in ascertaining whether or not a polynomial from the given generating set is a part of the unsat core. Our algorithm cannot guarantee a minimal unsat core; the paper describes an approach to refine the identified core. Experiments are performed on a variety of instances using a computer-algebra implementation of our algorithm.