Biographical Sketch, John Franco
Department of Computer Science
University of Cincinnati
Cincinnati, Ohio 45221-0030

Email:     franco@gauss.ececs.uc.edu
Curriculum:     Computer Science
Status:     Geier Professor of Computer Science
Gender:     Male

Research Focus:
       Professor Franco has worked in the area of Satisfiability since 1978. His Ph.D. thesis showed that a previously analyzed variant of the Davis-Putnam-Loveland-Logemann procedure (the main method for solving Satisfiability problems) does not have acceptable performance on the average. Later work proved that performance can be improved enormously by eliminating variables from small components first. Several of his papers focused on additional ways to do this. In 1999 Prof. Franco became principal investigator on a DoD project to build a SAT solver, merging ideas from his work and members of the technical staff of the DoD. That work lead to the development of a new type of Satisfiability solver which attempts to make more use of domain-specific information than conventional solvers.

Selected Relevant Research Contributions and Awards:
    Editorial Boards and Program Committees
   
    1.    Workshop Co-Organizer, 1st, 2nd, 3rd Workshops on Satisfiability, Sienna, Italy (1996), Paderborn, Germany (1998), Renessee, The Netherlands (2000).
    2.    Program Committee and Chair, 5th International Symposium on the Theory and Applications of Satisfiability Testing, Cincinnati, Ohio (2002).
    3.    Program Committee, 6th and 7th Conference on the Theory and Applications of Satisfiability Testing, St. Marguerita, Italy (2003), and Vancouver, Canada (2004).
    4.    Steering Committee, 8th and 9th Conference on the Theory and Applications of Satisfiability Testing, St. Andrews, Scotland (2005), and Seattle, Washington (2006).
    5.    Theory editor, Encyclopedia of Computer Science and Engineering, Wiley (to appear in 2007).
    6.    Associate editor, Journal on Satisfiability, Boolean Modeling, and Computation, University of Delft, IOS Press, ISSN: 1574-0617
    7.    Assistant editor, Annals of Mathematics and Artificial Intelligence, SpringerLink, ISSN: 1012-2443
    8.    Guest editor, "Satisfiability Testing," Annals of Mathematics and Artificial Intelligence 43(1), 2005, SpringerLink, ISSN: 1012-2443
    9.    Program Committee, 6th, 7th, 8th, 9th International Symposium on Math and Artificial Intelligence, Ft. Lauderdale, Florida (2000, 2002, 2004, 2006).
 
    Refereed Publications
   
    1.    "Extending existential quantification in conjunctions of BDDs," with S. Weaver and J.S. Schlipf.  Journal of Satisfiability, Boolean Modeling, and Computation 1:89-110, IOS Press, 2006.
    2.    "Resolution tunnels for improved SAT solver performance," with M. Kouril.  In Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science 3569:143-158, Springer, 2005.
    3.    "Typical case complexity of Satisfiability algorithms and the threshold phenomenon."  Discrete Applied Mathematics 153:89-123, Elsevier, 2005.
    4.    "A sharp threshold for the renameable Horn and q-Horn properties," with H. Daudè and N. Creignou.   Discrete Applied Mathematics 153:48-57, Elsevier, 2005.
    5.    "Function-complete look-ahead in support of efficient SAT search heuristics," with M. Kouril, J.S. Schlipf, S. Weaver, M. Dransfield, and W.M. Vanfleet.  Journal of Universal Computer Science 10:1655-1692, 2004.
    6.    "SBSAT: a state-based, BDD-based Satisfiability solver," with M. Kouril, J.S. Schlipf, J. Ward, S. Weaver, M. Dransfield, and W.M. Vanfleet.  In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science 2919:398-410, Springer, 2003.
    7.    "A perspective on certain polynomial time classes of Satisfiability," with A. Van Gelder.  Discrete Applied Mathematics 125:177-214, Elsevier, 2003.
    8.    "Results related to threshold phenomena research in Satisfiability: lower bounds."  Theoretical Computer Science 265:147-157, Elsevier, 2001.
    9.    "Algorithms for the Satisfiability problem: a survey," with J. Gu, P.W. Purdom, and B. Wah.  DIMACS Series on Discrete Mathematics and Theoretical Computer Science 35:19-151, American Mathematical Society, 1997.
    10.    "On finding solutions to extended Horn sets," with J. Schlipf, F. Annexstein, and R. Swaminathan.  Information Processing Letters 54:133-137, North-Holland, 1995.
    11.    "Elimination of infrequent variables improves average case performance of Satisfiability algorithms."  SIAM Journal on Computing 20:1119-1127, SIAM, 1991.
    12.    "Probabilistic analysis of a generalization of the unit-clause literal selection heuristic for the k-satisfiability problem," with M.T. Chao.  Information Sciences 51:289-314, Elsevier, 1990.
    13.    "Probabilistic analysis of two heuristics for the 3-Satisfiability problem," with M.T. Chao.  SIAM Journal on Computing 15:1106-1118, SIAM, 1986.
    14.    "Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem," with M. Paull.  Discrete Applied Mathematics 5:77-87, Elsevier, 1983.
 
    Patent
   
    1.    "Method and system for non-linear state based satisfiability," with W.M. Vanfleet, M. Dransfield, J.S. Schlipf, US Patent 6,912,700 (June 28, 2005).
 
    Awards
   
    1.    "Satisfiability Algorithm Research and Development to Enhance Formal Verification Tools," with John Schlipf. Department of Defense, MDA904-02-C-1162, 10/1/01-9/30/04, $561,000.
    2.    "Satisfiability Algorithm Research and Development to Enhance Formal Verification Tools," with John Schlipf. Department of Defense, MDA904-99-C-4547, 7/1/99-9/30/01, $493,000.
    3.    "Complexity of Algorithms for Problems in Propositional Logic," with John Schlipf, Office of Naval Research, N00014-94-1-0382, 1/1/94-3/31/97, $260,000.