A Gröbner Basis Approach to CNF-Formulae Preprocessing
Christopher Condrat1
and Priyank Kalla1 
| (1) |
Department of Electrical and Computer Engineering, University of Utah, Salt Lake City, UT, USA |
Abstract
This paper presents a CNF SAT-formulae transformation technique employing Gröbner bases as a means to analyze the problem
structure. Gröbner-bases have been applied in the past for SAT; however, their use was primarily restricted to analyzing entire
problems for proof-refutation. In contrast, this technique analyzes limited subsets of problems, and uses the derived Gröbner
bases to yield new constraint-information. This information is then used to reduce problem structure, provide additional information
about the problem itself, or aid other preprocessing techniques. Contrary to the precepts of contemporary techniques, the
transformation often increases the problem size. However, experimental results demonstrate that our approach often improves
SAT-search efficiency in a number of areas, including: solve time, conflicts, number of decisions, etc.
This work is supported, in part, by a Faculty Early Career Development (CAREER) grant from the US National Science Foundation,
contract No. CCF-546859.
References secured to subscribers.