Year |
Citation |
Score |
2013 |
Katebi H, Sakallah KA, Markov IL. Generalized Boolean symmetries through nested partition refinement Ieee/Acm International Conference On Computer-Aided Design, Digest of Technical Papers, Iccad. 763-770. DOI: 10.1109/ICCAD.2013.6691200 |
0.316 |
|
2011 |
Sakallah KA, Marques-Silva J. Anatomy and Empirical Evaluation of Modern SAT Solvers Bulletin of the European Association For Theoretical Computer Science. 1: 96-121. DOI: 10.14288/1.0043924 |
0.391 |
|
2011 |
Katebi H, Sakallah KA, Marques-Silva JP. Empirical study of the anatomy of modern sat solvers Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6695: 343-356. DOI: 10.1007/978-3-642-21581-0_27 |
0.32 |
|
2009 |
Liffiton M, Mneimneh M, Lynce I, Andraus Z, Marques-Silva J, Sakallah K. A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas Constraints - An International Journal. 14: 415-442. DOI: 10.1007/S10601-008-9058-8 |
0.759 |
|
2009 |
Aloul FA, Ramani A, Markov IL, Sakallah KA. Dynamic symmetry-breaking for Boolean satisfiability Annals of Mathematics and Artificial Intelligence. 57: 59-73. DOI: 10.1007/S10472-010-9173-2 |
0.71 |
|
2009 |
Liffiton MH, Sakallah KA. Generalizing core-guided Max-SAT Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5584: 481-494. DOI: 10.1007/978-3-642-02777-2_44 |
0.806 |
|
2008 |
Aloul FA, Ramani A, Markov IL, Sakallah KA. Symmetry breaking for pseudo-Boolean formulas Journal of Experimental Algorithmics. 12. DOI: 10.1145/1227161.1278375 |
0.687 |
|
2008 |
Liffiton MH, Sakallah KA. Algorithms for computing minimal unsatisfiable subsets of constraints Journal of Automated Reasoning. 40: 1-33. DOI: 10.1007/S10817-007-9084-Z |
0.806 |
|
2008 |
Andraus ZS, Liffiton MH, Sakallah KA. Reveal: A formal verification tool for verilog designs Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5330: 343-352. DOI: 10.1007/978-3-540-89439-1_25 |
0.737 |
|
2007 |
Aloul FA, Ramani A, Sakallah KA, Markov IL. Solution and optimization of systems of pseudo-Boolean constraints Ieee Transactions On Computers. 56: 1415-1424. DOI: 10.1109/Tc.2007.1075 |
0.729 |
|
2007 |
Safarpour S, Mangassarian H, Veneris A, Liffiton MH, Sakallah KA. Improved design debugging using maximum satisfiability Proceedings - Formal Methods in Computer Aided Design, Fmcad 2007. 13-19. DOI: 10.1109/FAMCAD.2007.26 |
0.791 |
|
2006 |
Sheini HM, Sakallah KA. Pueblo: A Hybrid Pseudo-Boolean SAT Solver Journal On Satisfiability, Boolean Modeling and Computation. 2: 165-189. DOI: 10.3233/Sat190020 |
0.796 |
|
2006 |
Ramani A, Markov IL, Sakallah KA, Aloul FA. Breaking instance-independent symmetries in exact graph coloring Journal of Artificial Intelligence Research. 26: 289-322. DOI: 10.1613/Jair.1637 |
0.723 |
|
2006 |
Sheini HM, Sakallah KA. SMT(CLU): A step toward scalability in system verification Ieee/Acm International Conference On Computer-Aided Design, Digest of Technical Papers, Iccad. 844-851. DOI: 10.1109/ICCAD.2006.320088 |
0.8 |
|
2006 |
Sheini HM, Sakallah KA. Ario: A linear integer arithmetic logic solver Proceedings of Formal Methods in Computer Aided Design, Fmcad 2006. 47-48. DOI: 10.1109/FMCAD.2006.7 |
0.794 |
|
2006 |
Sheini HM, Sakallah KA. A progressive simplifier for satisfiability modulo theories Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4121: 184-197. |
0.754 |
|
2006 |
Sheini HM, Sakallah KA. From propositional satisfiability to satisfiability modulo theories Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4121: 1-9. |
0.757 |
|
2006 |
Ramani A, Markov IL, Sakallah KA, Aloul FA. Breaking instance-independent symmetries in exact graph coloring Journal of Artificial Intelligence Research. 26: 289-322. |
0.701 |
|
2006 |
Andraus ZS, Liffiton MH, Sakallah KA. Refinement strategies for verification methods based on datapath abstraction Proceedings of the Asia and South Pacific Design Automation Conference, Asp-Dac. 2006: 19-24. |
0.764 |
|
2005 |
Mneimneh MN, Sakallah KA. Principles of sequential-equivalence verification Ieee Design and Test of Computers. 22: 248-257. DOI: 10.1109/Mdt.2005.68 |
0.802 |
|
2005 |
Sheini HM, Sakallah KA. Pueblo: A modern Pseudo-Boolean SAT solver Proceedings -Design, Automation and Test in Europe, Date '05. 683-684. DOI: 10.1109/DATE.2005.246 |
0.762 |
|
2005 |
Sheini HM, Peintrier B, Sakallah KA, Pollack ME. On solving soft temporal constraints using SAT techniques Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3709: 607-621. DOI: 10.1007/11564751_45 |
0.815 |
|
2005 |
Aloulj FA, Ramani A, Markov IL, Sakallah KA. Dynamic symmetry-breaking for improved Boolean optimization Proceedings of the Asia and South Pacific Design Automation Conference, Asp-Dac. 1: 445-450. |
0.303 |
|
2005 |
Liffiton MH, Sakallah KA. On finding all minimally unsatisfiable subformulas Lecture Notes in Computer Science. 3569: 173-186. |
0.811 |
|
2005 |
Liffiton MH, Moffitt MD, Pollack ME, Sakallah KA. Identifying conflicts in overconstrained temporal problems Ijcai International Joint Conference On Artificial Intelligence. 205-211. |
0.803 |
|
2005 |
Sheini HM, Sakallah KA. A SAT-based decision procedure for mixed logical/integer linear problems Lecture Notes in Computer Science. 3524: 320-335. |
0.781 |
|
2005 |
Sheini HM, Sakallah KA. A scalable method for solving satisfiability of integer linear arithmetic logic Lecture Notes in Computer Science. 3569: 241-256. |
0.783 |
|
2004 |
Nam GJ, Aloul F, Sakallah KA, Rutenbar RA. A comparative study of two Boolean formulations of FPGA detailed routing constraints Ieee Transactions On Computers. 53: 688-696. DOI: 10.1109/Tc.2004.1 |
0.699 |
|
2004 |
Andraus ZS, Sakallah KA. Automatic abstraction and verification of verilog models Proceedings - Design Automation Conference. 218-223. |
0.764 |
|
2004 |
Aloul FA, Markov IL, Sakallah KA. MINCE: A static global variable-ordering heuristic for SAT search and BDD manipulation Journal of Universal Computer Science. 10: 1562-1596. |
0.71 |
|
2004 |
Aloul FA, Ramani A, Markov IL, Sakallah KA. ShatterPB: Symmetry-breaking for pseudo-Boolean formulas Proceedings of the Asia and South Pacific Design Automation Conference, Asp-Dac. 884-887. |
0.681 |
|
2004 |
Mneimneh MN, Sakallah KA, Moondanos J. Preserving synchronizing sequences of sequential circuits after retiming Proceedings of the Asia and South Pacific Design Automation Conference, Asp-Dac. 579-584. |
0.743 |
|
2004 |
Darga PT, Liffiton MH, Sakallah KA, Markov IL. Exploiting structure in symmetry detection for CNF Proceedings - Design Automation Conference. 530-534. |
0.806 |
|
2004 |
Oh Y, Mneimneh MN, Andraus ZS, Sakallah KA, Markov IL. AMUSE: A minimally-unsatisfiable subformula extractor Proceedings - Design Automation Conference. 518-523. |
0.731 |
|
2003 |
Riepe MA, Sakallah KA. Transistor placement for noncomplementary digital VLSI cell synthesis Acm Transactions On Design Automation of Electronic Systems. 8: 81-107. DOI: 10.1145/606603.606608 |
0.353 |
|
2003 |
Aloul FA, Ramani A, Markov IL, Sakallah KA. Solving difficult instances of Boolean satisfiability in the presence of symmetry Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 22: 1117-1137. DOI: 10.1109/Tcad.2003.816218 |
0.711 |
|
2003 |
Aloul FA, Sakallah KA, Markov IL. Efficient symmetry breaking for Boolean satisfiability Ijcai International Joint Conference On Artificial Intelligence. 271-276. DOI: 10.1109/Tc.2006.75 |
0.683 |
|
2003 |
Aloul FA, Markov IL, Sakallah KA. Shatter: Efficient symmetry-breaking for Boolean satisfiability Proceedings - Design Automation Conference. 836-839. |
0.66 |
|
2003 |
Aloul FA, Markov IL, Sakallah KA. FORCE: A fast & easy-to-implement variable-ordering heuristic Proceedings of the Ieee Great Lakes Symposium On Vlsi. 116-119. |
0.647 |
|
2002 |
Kravets VN, Sakallah KA. Resynthesis of multi-level circuits under tight constraints using symbolic optimization Ieee/Acm International Conference On Computer-Aided Design, Digest of Technical Papers. 687-693. DOI: 10.1145/774572.774673 |
0.781 |
|
2002 |
Aloul FA, Ramani A, Markov IL, Sakallah KA. Generic ILP versus specialized 0-1 ILP: An update Ieee/Acm International Conference On Computer-Aided Design, Digest of Technical Papers. 450-457. DOI: 10.1145/774572.774638 |
0.62 |
|
2002 |
Guerra E Silva L, Marques-Silva J, Silveira LM, Sakallah KA. Satisfiability models and algorithms for circuit delay computation Acm Transactions On Design Automation of Electronic Systems. 7: 137-158. DOI: 10.1145/504914.504920 |
0.398 |
|
2002 |
Aloul FA, Sierawski BD, Sakallah KA. Satometer: How much have we searched? Proceedings - Design Automation Conference. 737-742. DOI: 10.1109/TCAD.2003.814960 |
0.627 |
|
2002 |
Aloul FA, Sierawski BD, Sakallah KA. Satometer: How much have we searched? Proceedings - Design Automation Conference. 737-742. DOI: 10.1109/Tcad.2003.814960 |
0.654 |
|
2002 |
Xu H, Rutenbar RA, Sakallah K. Sub-SAT: A formulation for relaxed Boolean satisfiability with applications in routing Proceedings of the International Symposium On Physical Design. 182-187. DOI: 10.1109/Tcad.2003.811450 |
0.415 |
|
2002 |
Nam GJ, Sakallah KA, Rutenbar RA. A new FPGA detailed routing approach via search-based Boolean satisfiability Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 21: 674-684. DOI: 10.1109/Tcad.2002.1004311 |
0.386 |
|
2002 |
Aloul FA, Mneimneh MN, Sakallah KA. Search-based SAT using zero-suppressed BDDs Proceedings -Design, Automation and Test in Europe, Date. 1082. DOI: 10.1109/DATE.2002.998438 |
0.795 |
|
2002 |
Aloul FA, Hassoun S, Sakallah KA, Blaauw D. Robust SAT-based search algorithm for leakage power reduction Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2451: 167-177. |
0.687 |
|
2002 |
Aloul FA, Ramani A, Markov IL, Sakallah KA. Solving difficult SAT instances in the presence of symmetry Proceedings - Design Automation Conference. 731-736. |
0.704 |
|
2002 |
Aloul FA, Markov IL, Sakallah KA. Improving the efficiency of circuit-to-BDD conversion by gate and input ordering Proceedings - Ieee International Conference On Computer Design: Vlsi in Computers and Processors. 64-69. |
0.66 |
|
2001 |
Yalcin H, Mortazavi M, Palermo R, Bamji C, Sakallah KA, Hayes JP. Fast and accurate timing characterization using functional information Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 20: 315-331. DOI: 10.1109/43.908474 |
0.323 |
|
2001 |
Aloul FA, Markov IL, Sakallah KA. Faster SAT and smaller BDDS via common function structure Ieee/Acm International Conference On Computer-Aided Design, Digest of Technical Papers. 443-448. |
0.591 |
|
2000 |
Aloul FA, Marques-Silva JP, Sakallah KA. An experimental study of satisfiability search heuristics Proceedings -Design, Automation and Test in Europe, Date. 745. DOI: 10.1109/DATE.2000.840878 |
0.632 |
|
1999 |
Marques-Silva JP, Sakallah KA. GRASP: A search algorithm for propositional satisfiability Ieee Transactions On Computers. 48: 506-521. DOI: 10.1109/12.769433 |
0.437 |
|
1999 |
Kim J, Silva JPM, Sakallah K. Satisfiability-Based Functional Delay Fault Testing Ieee Transactions On Very Large Scale Integration Systems. 362-372. DOI: 10.1007/978-0-387-35498-9_32 |
0.485 |
|
1998 |
Riepe MA, Sakallah KA. The edge-based design rule model revisited Acm Transactions On Design Automation of Electronic Systems. 3: 463-486. DOI: 10.1145/293625.293633 |
0.346 |
|
1997 |
Yook JG, Chandramouli V, Katehi LPB, Sakallah KA, Arabi TR, Schreyer TA. Computation of switching noise in printed circuit boards Ieee Transactions On Components Packaging and Manufacturing Technology Part A. 20: 64-74. DOI: 10.1109/95.558546 |
0.322 |
|
1997 |
Chandramouli V, Sakallah KA. Selection of Voltage Thresholds for Delay Measurement Analog Integrated Circuits and Signal Processing. 14: 9-28. DOI: 10.1023/A:1008274123958 |
0.335 |
|
1996 |
Riepe MA, Marques Silva JP, Sakallah KA, Brown RB. Ravel-XL: A hardware accelerator for assigned-delay compiled-code logic gate simulation Ieee Transactions On Very Large Scale Integration (Vlsi) Systems. 4: 113-129. DOI: 10.1109/92.486085 |
0.334 |
|
1995 |
Burks TM, Sakallah KA, Mudge TN. Critical Paths in Circuits with Level-Sensitive Latches Ieee Transactions On Very Large Scale Integration (Vlsi) Systems. 3: 273-291. DOI: 10.1109/92.386227 |
0.391 |
|
1995 |
Chang CH, Davidson ES, Sakallah KA. Maximum Rate Single-Phase Clocking of a Closed Pipeline including Wave Pipelining, Stoppability, and Startability Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 14: 1526-1545. DOI: 10.1109/43.476583 |
0.363 |
|
1995 |
Kayssi AI, Sakallah KA. Timing models for gallium arsenide direct-coupled FET logic circuits Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 14: 384-393. DOI: 10.1109/43.365129 |
0.318 |
|
1993 |
Kayssi AI, Sakallah KA, Mudge TN. The Impact of Signal Transition Time on Path Delay Computation Ieee Transactions On Circuits and Systems Ii: Analog and Digital Signal Processing. 40: 302-309. DOI: 10.1109/82.227370 |
0.321 |
|
1993 |
Sakallah KA, Mudge TN, Burks TM, Davidson ES. Synchronization of Pipelines Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 12: 1132-1146. DOI: 10.1109/43.238606 |
0.314 |
|
1992 |
Sakallah KA, Mudge TN, Olukotun OA. Analysis and Design of Latch-Controlled Synchronous Digital Circuits Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 11: 322-333. DOI: 10.1109/43.124419 |
0.407 |
|
1991 |
Olukotun OA, Brown RB, Lomax RJ, Mudge TN, Sakallah KA. Multilevel Optimization in the Design of a High-Performance GaAs Microcomputer Ieee Journal of Solid-State Circuits. 26: 763-767. DOI: 10.1109/4.78246 |
0.339 |
|
1991 |
Mudge TN, Brown RB, Birmingham WP, Dykstra JA, Kayssi AI, Lomax RJ, Olukotun OA, Sakallah KA, Milano RA. The Design of a Microsupercomputer Computer. 24: 56-64. DOI: 10.1109/2.67194 |
0.324 |
|
Show low-probability matches. |