Karem A. Sakallah - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

Empirical Study of the Anatomy of Modern Sat SolversHadi Katebi, Karem A. Sakallah, João P. Marques Silva. sat 2011: 343-356 [doi]

Generating Data Race Witnesses by an SMT-Based AnalysisMahmoud Said, Chao Wang, Zijiang Yang, Karem A. Sakallah. NFM 2011: 313-327 [doi]

Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. ProceedingsKarem A. Sakallah, Laurent Simon, editors, Volume 6695 of Lecture Notes in Computer Science, Springer, 2011. [doi]

2010

Incorporating user control in automated interactive scheduling systemsJina Huh, Martha E. Pollack, Hadi Katebi, Karem A. Sakallah, Ned Kirsch. ACMdis 2010: 306-309 [doi]

Symmetry and Satisfiability: An UpdateHadi Katebi, Karem A. Sakallah, Igor L. Markov. sat 2010: 113-127 [doi]

2009

Dynamic symmetry-breaking for Boolean satisfiabilityFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. AMAI, 57(1):59-73, 2009. [doi]

Generalizing Core-Guided Max-SATMark H. Liffiton, Karem A. Sakallah. sat 2009: 481-494 [doi]

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulasMark H. Liffiton, Maher N. Mneimneh, InÃªs Lynce, Zaher S. Andraus, JoÃ£o Marques-Silva, Karem A. Sakallah. constraints, 14(4):415-442, 2009. [doi]

Symmetry and SatisfiabilityKarem A. Sakallah. In Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh, editors, Handbook of Satisfiability. Volume 185 of Frontiers in Artificial Intelligence and Applications, pages 289-338, IOS Press, 2009. [doi]

2008

2007

Symmetry breaking for pseudo-Boolean formulasFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. jea, 12, 2007. [doi]

Solution and Optimization of Systems of Pseudo-Boolean ConstraintsFadi A. Aloul, Arathi Ramani, Karem A. Sakallah, Igor L. Markov. TC, 56(10):1415-1424, 2007. [doi]

Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, ProceedingsJoão Marques-Silva, Karem A. Sakallah, editors, Volume 4501 of Lecture Notes in Computer Science, Springer, 2007.

Report on the SAT 2007 Conference on Theory and Applications of Satisfiability TestingJoão Marques-Silva, Karem A. Sakallah, Inês Lynce. aim, 28(4):135-136, 2007. [doi]

Improved Design Debugging Using Maximum SatisfiabilitySean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah. FMCAD 2007: 13-19 [doi]

2006

Efficient Symmetry Breaking for Boolean SatisfiabilityFadi A. Aloul, Karem A. Sakallah, Igor L. Markov. TC, 55(5):549-558, 2006. [doi]

Refinement strategies for verification methods based on datapath abstractionZaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah. aspdac 2006: 19-24 [doi]

Breaking Instance-Independent Symmetries In Exact Graph ColoringArathi Ramani, Igor L. Markov, Karem A. Sakallah, Fadi A. Aloul. jair, 26:289-322, 2006. [doi]

SMT(::::CLU::::): a step toward scalability in system verificationHossein M. Sheini, Karem A. Sakallah. iccad 2006: 844-851 [doi]

From Propositional Satisfiability to Satisfiability Modulo TheoriesHossein M. Sheini, Karem A. Sakallah. sat 2006: 1-9 [doi]

A Progressive Simplifier for Satisfiability Modulo TheoriesHossein M. Sheini, Karem A. Sakallah. sat 2006: 184-197 [doi]

Pueblo: A Hybrid Pseudo-Boolean SAT SolverHossein M. Sheini, Karem A. Sakallah. jsat, 2(1-4):165-189, 2006. [doi]

Ario: A Linear Integer Arithmetic Logic SolverHossein M. Sheini, Karem A. Sakallah. FMCAD 2006: 47-48 [doi]

2005

Dynamic symmetry-breaking for improved Boolean optimizationFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. aspdac 2005: 445-450 [doi]

On Finding All Minimally Unsatisfiable SubformulasMark H. Liffiton, Karem A. Sakallah. sat 2005: 173-186 [doi]

Identifying Conflicts in Overconstrained Temporal ProblemsMark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, Karem A. Sakallah. IJCAI 2005: 205-211 [doi]

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable FormulasMaher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João P. Marques Silva, Karem A. Sakallah. sat 2005: 467-474 [doi]

Principles of Sequential-Equivalence VerificationMaher N. Mneimneh, Karem A. Sakallah. dt, 22(3):248-257, 2005. [doi]

Pueblo: A Modern Pseudo-Boolean SAT SolverHossein M. Sheini, Karem A. Sakallah. date 2005: 684-685 [doi]

A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic LogicHossein M. Sheini, Karem A. Sakallah. sat 2005: 241-256 [doi]

A SAT-Based Decision Procedure for Mixed Logical/Integer Linear ProblemsHossein M. Sheini, Karem A. Sakallah. cpaior 2005: 320-335 [doi]

On Solving Soft Temporal Constraints Using SAT TechniquesHossein M. Sheini, Bart Peintner, Karem A. Sakallah, Martha E. Pollack. cp 2005: 607-621 [doi]

2004

ShatterPB: symmetry-breaking for pseudo-Boolean formulasFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. aspdac 2004: 883-886 [doi]

MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD ManipulationFadi A. Aloul, Igor L. Markov, Karem A. Sakallah. jucs, 10(12):1562-1596, 2004. [doi]

Automatic abstraction and verification of verilog modelsZaher S. Andraus, Karem A. Sakallah. dac 2004: 218-223 [doi]

Exploiting structure in symmetry detection for CNFPaul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov. dac 2004: 530-534 [doi]

Preserving synchronizing sequences of sequential circuits after retimingMaher N. Mneimneh, Karem A. Sakallah, John Moondanos. aspdac 2004: 579-584 [doi]

A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing ConstraintsGi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar. TC, 53(6):688-696, 2004. [doi]

AMUSE: a minimally-unsatisfiable subformula extractorYoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, Igor L. Markov. dac 2004: 518-523 [doi]

Breaking Instance-Independent Symmetries in Exact Graph ColoringArathi Ramani, Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah. date 2004: 324-331 [doi]

2003

Solving difficult instances of Boolean satisfiability in the presence of symmetryFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. tcad, 22(9):1117-1137, 2003. [doi]

Shatter: efficient symmetry-breaking for boolean satisfiabilityFadi A. Aloul, Igor L. Markov, Karem A. Sakallah. dac 2003: 836-839 [doi]

FORCE: a fast and easy-to-implement variable-ordering heuristicFadi A. Aloul, Igor L. Markov, Karem A. Sakallah. glvlsi 2003: 116-119 [doi]

Efficient Symmetry Breaking for Boolean SatisfiabilityFadi A. Aloul, Karem A. Sakallah, Igor L. Markov. IJCAI 2003: 271-276

Satometer: how much have we searched?Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah. tcad, 22(8):995-1004, 2003. [doi]

Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and SolutionMaher N. Mneimneh, Karem A. Sakallah. sat 2004: 411-425 [doi]

Transistor placement for noncomplementary digital VLSI cell synthesisMichael A. Riepe, Karem A. Sakallah. todaes, 8(1):81-107, 2003. [doi]

sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routingHui Xu, Rob A. Rutenbar, Karem A. Sakallah. tcad, 22(6):814-820, 2003. [doi]

2002

Efficient Gate and Input Ordering for Circuit-to-BDD ConversionFadi A. Aloul, Igor L. Markov, Karem A. Sakallah. iwls 2002: 137-142

Generic ILP versus specialized 0-1 ILP: an updateFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. iccad 2002: 450-457 [doi]

Solving difficult SAT instances in the presence of symmetryFadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. dac 2002: 731-736 [doi]

Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input OrderingFadi A. Aloul, Igor L. Markov, Karem A. Sakallah. iccd 2002: 64-69 [doi]

Satometer: how much have we searched?Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah. dac 2002: 737-742 [doi]

Robust SAT-Based Search Algorithm for Leakage Power ReductionFadi A. Aloul, Soha Hassoun, Karem A. Sakallah, David Blaauw. patmos 2002: 167-177 [doi]

ZBDD-Based Backtrack Search SAT SolverFadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah. iwls 2002: 131-136

Search-Based SAT Using Zero-Suppressed BDDsFadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah. date 2002: 1082 [doi]

Satisfiability models and algorithms for circuit delay computationLuís Guerra e Silva, João P. Marques Silva, Luis Miguel Silveira, Karem A. Sakallah. todaes, 7(1):137-158, 2002. [doi]

Resynthesis of multi-level circuits under tight constraints using symbolic optimizationVictor N. Kravets, Karem A. Sakallah. iccad 2002: 687-693 [doi]

Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric SearchGi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar. fpl 2002: 360-369 [doi]

A new FPGA detailed routing approach via search-based BooleansatisfiabilityGi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar. tcad, 21(6):674-684, 2002. [doi]

Majority-Based Decomposition of Carry Logic in Binary AddersLeyla Nazhandali, Karem A. Sakallah. iwls 2002: 179-184

sub-SAT: a formulation for relaxed boolean satisfiability with applications in routingHui Xu, Rob A. Rutenbar, Karem A. Sakallah. ispd 2002: 182-187 [doi]

2001

Faster SAT and Smaller BDDs via Common Function StructureFadi A. Aloul, Igor L. Markov, Karem A. Sakallah. iccad 2001: 443-448 [doi]

Scalable Hybrid Verification of Complex MicroprocessorsMaher N. Mneimneh, Fadi A. Aloul, Christopher T. Weaver, Saugata Chatterjee, Karem A. Sakallah, Todd M. Austin. dac 2001: 41-46 [doi]

A comparative study of two Boolean formulations of FPGA detailed routing constraintsGi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar. ispd 2001: 222-227 [doi]

A boolean satisfiability-based incremental rerouting approach with application to FPGAsGi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar. date 2001: 560-565 [doi]

SATIRE: A New Incremental Satisfiability EngineJesse Whittemore, Joonyoung Kim, Karem A. Sakallah. dac 2001: 542-545 [doi]

An Advanced Timing Characterization Method Using Mode DependencyHakan Yalcin, Robert Palermo, Mohammad Mortazavi, Cyrus Bamji, Karem A. Sakallah, John P. Hayes. dac 2001: 657-660 [doi]

Fast and accurate timing characterization using functionalinformationHakan Yalcin, Mohammad Mortazavi, Robert Palermo, Cyrus Bamji, Karem A. Sakallah, John P. Hayes. tcad, 20(2):315-331, 2001. [doi]

2000

On Applying Incremental Satisfiability to Delay Fault TestingJoonyoung Kim, Jesse Whittemore, Karem A. Sakallah, João P. Marques Silva. date 2000: 380-384 [doi]

On Solving Stack-Based Incremental Satisfiability ProblemsJoonyoung Kim, Jesse Whittemore, Karem A. Sakallah. iccd 2000: 379-382 [doi]

Generalized Symmetries in Boolean FunctionsVictor N. Kravets, Karem A. Sakallah. iccad 2000: 526-532

Constructive Library-Aware Synthesis Using SymmetriesVictor N. Kravets, Karem A. Sakallah. date 2000: 208 [doi]

An Experimental Study of Satisfiability Search HeuristicsKarem A. Sakallah, Fadi A. Aloul, João P. Marques Silva. date 2000: 745 [doi]

Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design AutomationJoão P. Marques Silva, Karem A. Sakallah. cav 2000: 3

Boolean satisfiability in electronic design automationJoão P. Marques Silva, Karem A. Sakallah. dac 2000: 675-680 [doi]

1999

Timing verification of sequential dynamic circuitsDavid Van Campenhout, Trevor N. Mudge, Karem A. Sakallah. tcad, 18(5):645-658, 1999. [doi]

Satisfiability-Based Functional Delay Fault TestingJoonyoung Kim, João P. Marques Silva, Karem A. Sakallah. ifip10-5 2000: 362-372

Satisfiability-Based Detailed FPGA RoutingGi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar. vlsid 1999: 574-577 [doi]

Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs vis Search-Based Boolean SATGi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar. fpga 1999: 167-175 [doi]

Transistor level micro-placement and routing for two-dimensional digital VLSI cell synthesisMichael A. Riepe, Karem A. Sakallah. ispd 1999: 74-81 [doi]

GRAPS: A Search Algorithm for Propositional SatisfiabilityJoão P. Marques Silva, Karem A. Sakallah. TC, 48(5):506-521, 1999.

Functional Timing Analysis for IP CharacterizationHakan Yalcin, Mohammad Mortazavi, Robert Palermo, Cyrus Bamji, Karem A. Sakallah. dac 1999: 731-736 [doi]

1998

1997

Signal Delay in Coupled, Distributed RC Lines in the Presence of Temporal ProximityV. Chandramouli, Karem A. Sakallah, Ayman I. Kayssi. arvlsi 1997: 32-46 [doi]

Robust Search Algorithms for Test Pattern GenerationJoão P. Marques Silva, Karem A. Sakallah. ftcs 1997: 152-161

1996

Timing verification of sequential domino circuitsDavid Van Campenhout, Trevor N. Mudge, Karem A. Sakallah. iccad 1996: 127-132 [doi]

Modeling the Effects of Temporal Proximity of Input Transitions on Gate Propagation Delay and Transition TimeV. Chandramouli, Karem A. Sakallah. dac 1996: 617-622 [doi]

Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulationMichael A. Riepe, João P. Marques Silva, Karem A. Sakallah, Richard B. Brown. tvlsi, 4(1):113-129, 1996. [doi]

GRASP - a new search algorithm for satisfiabilityJoão P. Marques Silva, Karem A. Sakallah. iccad 1996: 220-227 [doi]

Conflict Analysis in Search Algorithms for SatisfiabilityJoão P. Marques Silva, Karem A. Sakallah. ictai 1996: 467-469

An approximate timing analysis method for datapath circuitsHakan Yalcin, John P. Hayes, Karem A. Sakallah. iccad 1996: 114-118 [doi]

1995

Critical paths in circuits with level-sensitive latchesTimothy M. Burks, Karem A. Sakallah, Trevor N. Mudge. tvlsi, 3(2):273-291, 1995. [doi]

PreviousNext