Publications
Citation information available on Google Scholar.
Journals
A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas
Mark H. Liffiton, Maher Mneimneh, Inês Lynce, Zaher Andraus, João Marques-Silva, and Karem Sakallah
Constraints, 14(4):415-442, 2009. [published online August, 2008]
Mark H. Liffiton, Maher Mneimneh, Inês Lynce, Zaher Andraus, João Marques-Silva, and Karem Sakallah
Constraints, 14(4):415-442, 2009. [published online August, 2008]
(The original publication is available at www.springerlink.com here.)
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints
Mark H. Liffiton and Karem A. Sakallah
Journal of Automated Reasoning, 40(1):1-33, January 2008. [published online September, 2007]
Mark H. Liffiton and Karem A. Sakallah
Journal of Automated Reasoning, 40(1):1-33, January 2008. [published online September, 2007]
(The original publication is available at www.springerlink.com here.)
Conferences
Generalizing Core-Guided Max-SAT
Mark H. Liffiton and Karem A. Sakallah
in Proc. 12th International Conference on Theory and Applications of Satisfiability Testing (SAT-2009), 481-494, June 2009.
Mark H. Liffiton and Karem A. Sakallah
in Proc. 12th International Conference on Theory and Applications of Satisfiability Testing (SAT-2009), 481-494, June 2009.
Reveal: A Formal Verification Tool for Verilog Designs
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-2008), 343-352, November 2008.
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-2008), 343-352, November 2008.
Searching for Autarkies to Trim Unsatisfiable Clause Sets (presentation)
Mark H. Liffiton and Karem A. Sakallah
in Proc. 11th International Conference on Theory and Applications of Satisfiability Testing (SAT-2008), 182-195, May 2008.
Mark H. Liffiton and Karem A. Sakallah
in Proc. 11th International Conference on Theory and Applications of Satisfiability Testing (SAT-2008), 182-195, May 2008.
Improved Design Debugging using Maximum Satisfiability
Sean Safarpour, Mark H. Liffiton, Hratch Mangassarian, Andreas Veneris, and Karem A. Sakallah
in Proc. 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2007), 13-19, November 2007.
Sean Safarpour, Mark H. Liffiton, Hratch Mangassarian, Andreas Veneris, and Karem A. Sakallah
in Proc. 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2007), 13-19, November 2007.
Refinement Strategies for Verification Methods Based on Datapath Abstraction
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 11th Asia and South Pacific Design Automation Conference (ASP-DAC-2006), 19-24, January 2006.
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 11th Asia and South Pacific Design Automation Conference (ASP-DAC-2006), 19-24, January 2006.
Identifying Conflicts in Overconstrained Temporal Problems (presentation)
Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, and Karem A. Sakallah
in Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI-05), 205-211, August 2005.
Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, and Karem A. Sakallah
in Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI-05), 205-211, August 2005.
On Finding All Minimally Unsatisfiable Subformulas (presentation)
Mark H. Liffiton and Karem A. Sakallah
in Proc. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), 173-186, June 2005.
Mark H. Liffiton and Karem A. Sakallah
in Proc. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), 173-186, June 2005.
(For a better (newer, more complete) reference for this work, see the paper in the Journal of Automated Reasoning (2008) above.)
Exploiting Structure in Symmetry Detection for CNF
Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov
in Proc. 41st IEEE/ACM Design Automation Conference (DAC-04), 530-534, June 2004.
Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov
in Proc. 41st IEEE/ACM Design Automation Conference (DAC-04), 530-534, June 2004.
Technical Reports
CEGAR-Based Formal Hardware Verification: A Case Study
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
CSE-TR-531-07, University of Michigan, May 2007.
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
CSE-TR-531-07, University of Michigan, May 2007.
From Max-SAT to Min-UNSAT: Insights and Applications
Mark H. Liffiton, Zaher S. Andraus, and Karem A. Sakallah
CSE-TR-506-05, University of Michigan, February 2005.
Mark H. Liffiton, Zaher S. Andraus, and Karem A. Sakallah
CSE-TR-506-05, University of Michigan, February 2005.