Boolean equi-propagation for optimized SAT encoding

Amit Metodi, Michael Codish, Vitaly Lagoon, Peter J. Stuckey

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

14 Citations (Scopus)

Abstract

We present an approach to propagation based SAT encoding, Boolean equi-propagation, where constraints are modelled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied as a form of partial evaluation to simplify constraints prior to their encoding as CNF formulae. We demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings
PublisherSpringer
Pages621-636
Number of pages16
ISBN (Print)9783642237850
DOIs
Publication statusPublished - 26 Sep 2011
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2011 - Perugia, Italy
Duration: 12 Sep 201116 Sep 2011
Conference number: 17th
http://www.dmi.unipg.it/cp2011/

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6876 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2011
Abbreviated titleCP 2011
CountryItaly
CityPerugia
Period12/09/1116/09/11
Internet address

Cite this