
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov, "Efficient Symmetry Breaking for Boolean Satisfiability," IEEE Transactions on Computers, vol. 55, no. 5, pp. 549558, May, 2006.  
BibTex  x  
@article{ 10.1109/TC.2006.75, author = {Fadi A. Aloul and Karem A. Sakallah and Igor L. Markov}, title = {Efficient Symmetry Breaking for Boolean Satisfiability}, journal ={IEEE Transactions on Computers}, volume = {55}, number = {5}, issn = {00189340}, year = {2006}, pages = {549558}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2006.75}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Efficient Symmetry Breaking for Boolean Satisfiability IS  5 SN  00189340 SP549 EP558 EPD  549558 A1  Fadi A. Aloul, A1  Karem A. Sakallah, A1  Igor L. Markov, PY  2006 KW  Backtrack Search KW  clause learning KW  conjunctive normal form (CNF) KW  graph automorphism KW  satisfiability (SAT) KW  symmetries. VL  55 JA  IEEE Transactions on Computers ER   
[1] F. Aloul, A. Ramani, I.L. Markov, and K. Sakallah, “Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetries,” IEEE Trans. Computer Aided Design, vol. 22, no. 9, pp. 11171137, 2003.
[2] F. Aloul, A. Ramani, I.L. Markov, and K. Sakallah, “Generic ILP versus Specialized 01 ILP,” Proc. Int'l Conf. ComputerAided Design (ICCAD), pp. 450457, 2002.
[3] R. Bayardo Jr. and R. Schrag, “Using CSP LookBack Techniques to Solve Real World SAT Instances,” Proc. Nat'l Conf. Artificial Intelligence, pp. 203208, 1997.
[4] A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures instead of BDDs,” Proc. Design Automation Conf. (DAC), pp. 317320, 1999.
[5] J. Crawford, M. Ginsberg, E. Luks, and A. Roy, “SymmetryBreaking Predicates for Search Problems,” Proc. Int'l Conf. Principles of Knowledge Representation and Reasoning, pp. 148159, 1996.
[6] P. Darga, M.H. Liffiton, K.A. Sakallah, and I.L. Markov, “Exploiting Structure in Symmetry Generation for CNF,” Proc. Design Automation Conf. (DAC), pp. 530534, 2004.
[7] DIMACS Challenge benchmarks, ftp://Dimacs.rutgers.EDU/pub/challenge/sat/ benchmarkscnf, 1996.
[8] N. Een and N. Sorensson, “An Extensible SATSolver,” Theory and Applications of Satisfiability Testing, pp. 502518, 2003.
[9] J.B. Fraleigh, A First Course in Abstract Algebra, sixth ed. Reading, Mass.: Addison Wesley Longman, 2000.
[10] E. Goldberg and Y. Novikov, “BerkMin: A Fast and Robust SATSolver,” Proc. Design, Automation, and Test in Europe Conf. (DATE), pp. 142149, 2002.
[11] T. Larrabee, “Test Pattern Generation Using Boolean Satisfiability,” IEEE Trans. Computer Aided Design, vol. 11, no. 1, pp. 415, 1992.
[12] B. McKay, “Practical Graph Isomorphism,” Congressus Numerantium, vol. 30, pp. 4587, 1981, http://cs.anu.edu.au/bdmnauty/.
[13] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. Design Automation Conf. (DAC), pp. 530535, 2001.
[14] G. Nam, F. Aloul, K. Sakallah, and R. Rutenbar, “A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints,” Proc. Int'l Symp. Physical Design (ISPD), pp. 222227, 2001.
[15] S. Prestwich, “Supersymmetric Modeling for Local Search,” Proc. Workshop Symmetry and CSPs (SymCon), 2002.
[16] SAT 2002 Competition, http://www.satlive.org/SATCompetition submittedbenchs.html , 2002.
[17] B. Selman, H. Kautz, and B. Cohen, “Noise Strategies for Improving Local Search,” Proc. Nat'l Conf. Artificial Intelligence, pp. 337343, 1994.
[18] J. Silva and K. Sakallah, “GRASP: A New Search Algorithm for Satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506521, May 1999.
[19] E. Spitznagel, “Review of Mathematical Software, GAP,” Notices Am. Math. Soc., vol. 41, no. 7, pp. 780782, 1994.
[20] P. Stephan, R. Brayton, and A. SangiovanniVincentelli, “Combinational Test Generation Using Satisfiability,” IEEE Trans. ComputerAided Design, vol. 15, no. 9, pp. 11671175, 1996.
[21] A. Urquhart, “Hard Examples for Resolution,” J. ACM, vol. 34, no. 1, pp. 209219, 1987.
[22] M.N. Velev and R.E. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,” Proc. Design Automation Conf. (DAC), pp. 226231, 2001.
[23] H. Zhang, “SATO: An Efficient Propositional Prover,” Proc. Int'l Conf. Automated Deduction, pp. 272275, 1997.