Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleA Gr\"obner basis approach to CNF-formulae preprocessing.
Author(s) Christopher Condrat, Priyank Kalla
TypeBook, Chapter in Book, Conference Proceeding
AbstractThis 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.
URL http://link.springer.com/chapter/10.1007%2F978-3-540-71209-1_48
PublisherBerlin: Springer
Translation No
Refereed No