Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

A Gröbner Basis Approach to CNF-Formulae Preprocessing

Christopher CondratContact Information and Priyank KallaContact Information

(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.

Contact Information Christopher Condrat
Email: chris@g6net.com

Contact Information Priyank Kalla
Email: kalla@eng.utah.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.111 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)