Integration of supercubing and learning in a SAT solver

ABSTRACT

Learning is an essential pruning technique in modern SAT solvers, but it exploits a relatively small amount of information that can be deduced from the conflicts. Recently a new pruning technique called supercubing was proposed [1]. Supercubing can exploit functional symmetries that are abundant in industrial SAT instances. We point out the significant difficulties of integrating supercubing with learning and propose solutions. Our experimental solver is the first supercubing-based solver with performance comparable to leading edge solvers.

REFERENCES

• 1: E. Goldberg , M. Prasad , R. Brayton, Using Problem Symmetry in Search Based Satisfiability Algorithms, Proceedings of the conference on Design, automation and test in Europe, p.134, March 04-08, 2002
• 2: G. Nam , K. Sakallah , R. Rutenbar, A boolean satisfiability-based incremental rerouting approach with application to FPGAs, Proceedings of the conference on Design, automation and test in Europe, p.560-565, March 2001, Munich, Germany
• 3: P. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Combinational test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(9):1167--1176, Sept 1996.
• 4: Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378469]
• 5: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 6: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 7: Lawrence Ryan. Efficient algortihtms for clause-learning SAT solvers. Master's thesis, Simon Fraser University, 2004.
• 8: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 9: Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, Solving difficult SAT instances in the presence of symmetry, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514102]
• 10: Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Shatter: efficient symmetry-breaking for boolean satisfiability, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776042]
• 11: Paul T. Darga , Mark H. Liffiton , Karem A. Sakallah , Igor L. Markov, Exploiting structure in symmetry detection for CNF, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996712]
• 12: Mukul Ranjan Prasad. Propositional Satisfiability Algorithms in EDA Applications. PhD thesis, University of California at Berkeley, 2001.
• 13: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 14: João P. Marques Silva, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms, Proceedings of the 9th Portuguese Conference on Artificial Intelligence: Progress in Artificial Intelligence, p.62-74, September 21-24, 1999
• 15: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]