Solving difficult SAT instances in the presence of symmetry

Research in algorithms for Boolean satisfiability and their implementations has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks can be solved in seconds on commodity PCs. More recent benchmarks take longer to solve because of their large size, but are still solved in mi...

Full description

Saved in:
Bibliographic Details
Main Authors: Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.
Format: Conference Proceeding
Language:English
Subjects:
Application software
Computer science
Design automation
Field programmable gate arrays
Graph theory
Microprocessors
Pathology
Personal communication networks
Polynomials
Routing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Research in algorithms for Boolean satisfiability and their implementations has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks can be solved in seconds on commodity PCs. More recent benchmarks take longer to solve because of their large size, but are still solved in minutes. Yet, small and difficult SAT instances must exist because Boolean satisfiability is NP-complete. We propose an improved construction of symmetry-breaking clauses and apply it to achieve significant speed-ups over current state-of-the-art in Boolean satisfiability. Our techniques are formulated as preprocessing and can be applied to any SAT solver without changing its source code. We also show that considerations of symmetry may lead to more efficient reductions to SAT in the routing domain. Our work articulates SAT instances that are unusually difficult for their size, including satisfiable instances derived from routing problems. Using an efficient implementation to solve the graph automorphism problem, we show that in structured SAT instances difficulty may be associated with large numbers of symmetries.
ISSN:0738-100X
DOI:10.1109/DAC.2002.1012719