Solving difficult SAT instances in the presence of symmetry

Research in algorithms for Boolean satisfiability and their efficient implementations [26, 8] has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks from the early 1990s [12] can be solved in seconds on commodity PCs. More recent benchmarks take longer to solve primarily because of their large size, but are still solved in minutes [28]. However, small and difficult SAT instances must exist because Boolean satisfiability is NP-complete. Our work articulates a number of SAT instances that are unusually difficult for their size, including satisfiable instances from global routing and detailed routing for FPGAs [22]. Using an efficient implementation to solve the graph automorphism problem [21, 23, 25], we show that in structured SAT instances difficulty is sometimes associated with large numbers of symmetries. We propose a new, improved construction of symmetry-breaking clauses [11] and apply them to empirically demonstrate very significant speed-ups over curre...

• Type: Conference
• Year: 2002
• Where: DAC
• Authors: Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
• Keywords: Boolean Satisfiability, DAC 2002, Design Automation, Difficult Sat Instances, SAT Instances Difficulty