You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

A Faster Clause-Shortening Algorithm for SAT with No Restriction on Clause Length

Article type: Research Article

Authors: Dantsin, Evgeny | Wolpert, Alexander

Affiliations: Department of Computer Science, Roosevelt University, 430 S. Michigan Av., Chicago, IL 60605, USA. E-mails: edantsin@roosevelt.edu, awolpert@roosevelt.edu

Keywords: SAT with no restriction on clause length, upper bound, clause shortening

DOI: 10.3233/SAT190002

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 1, pp. 49-60, 2006

Received 1 July 2005
|
Revision received 1 November 2005
|
Published: 1 November 2005
Get PDF open access

Abstract

We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. This algorithm uses the clause-shortening approach proposed by Schuler [14]. The running time of the algorithm is O(2n(1−1/α)) where α=ln(m/n)+O(lnlnm) and n, m are respectively the number of variables and the number of clauses in the input formula. This bound is asymptotically better than the previously best known 2n(1−1/log(2m)) bound for SAT.

Show less