Accelerating SAT solving by common subclause elimination

Yaowei Yan, Chris E. Gutierrez, Jeriah Jn-Charles, Forrest S. Bao, Yuanlin Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

Boolean SATisfiability (SAT) is an important problem in AI. SAT solvers have been effectively used in important industrial applications including automated planning and verification. In this paper, we present novel algorithms for fast SAT solving by employing two common subclause elimination (CSE) approaches. Our motivation is that modern SAT solving techniques can be more efficient on CSE-processed instances. Empirical study shows that CSE can significantly speed up SAT solving.

Original languageEnglish
Title of host publicationProceedings of the 29th AAAI Conference on Artificial Intelligence, AAAI 2015 and the 27th Innovative Applications of Artificial Intelligence Conference, IAAI 2015
PublisherAI Access Foundation
Pages4224-4225
Number of pages2
ISBN (Electronic)9781577357049
StatePublished - Jun 1 2015
Event29th AAAI Conference on Artificial Intelligence, AAAI 2015 and the 27th Innovative Applications of Artificial Intelligence Conference, IAAI 2015 - Austin, United States
Duration: Jan 25 2015Jan 30 2015

Publication series

NameProceedings of the National Conference on Artificial Intelligence
Volume6

Conference

Conference29th AAAI Conference on Artificial Intelligence, AAAI 2015 and the 27th Innovative Applications of Artificial Intelligence Conference, IAAI 2015
Country/TerritoryUnited States
CityAustin
Period01/25/1501/30/15

Fingerprint

Dive into the research topics of 'Accelerating SAT solving by common subclause elimination'. Together they form a unique fingerprint.

Cite this