Heuristiken zur Lösung von SAT- und QSAT-Problemen - Wintersemester 04/05

Themenliste

1. SAT-Themen

   
   
   
   
   1. DP-, DPLL- und Stålmarck-Algorithmus
      
      
      
      • DAVIS, M., G. LOGEMANN, D. LOVELAND:
        
        A machine program for theorem proving.
        
        Communications of the ACM, 5:394-397, 1962.
      
      
      
      • DAVIS, M. H. PUTNAM:
        
        A Computing Procedure for Quantification Theory.
        
        Journal of the ACM, 7(3):201-215, 1960.
      
      
      
      • SHEERAN, MARY GUNNAR STÃ…LMARCK:
        
        A tutorial on Stålmarck's proof procedure for propositional logic.
        
        GOPALAKRISHNAN, G. P. WINDLEY: Proceedings 2nd Intl. Conf. on Formal Methods in
        Computer-Aided Design, FMCAD 1998, Palo Alto, CA, USA, 4-6 Nov 1998, 82-99. Springer-Verlag,
        Berlin, 1998.
      
      
   
   
   
   2. GRASP und Lernen von Klauseln
      
      
      
      • MARQUES-SILVA, J.P. K.A. SAKALLAH:
        
        Conflict analysis in search algorithms for propositional satisfiability.
        
        IEEE International Conference on Tools with Artificial Intelligence, 1996.
      
      
      
      • SILVA, J. P. M. K. A. SAKALLAH:
        
        Grasp-a new search algorithm for satisfiability.
        
        CSE-TR-292-96, The University of Michigan, April 1996.
      
      
      
      • ZHANG, L., C. MADIGAN, M. MOSKEWICZ, S. MALIK:
        
        Efficient Conflict Driven Learning in a Boolean Satisfiability Solver.
        
        Int'l Conf. on CAD, San Jose, CA, November 2001.
      
      
   
   
   
   3. Chaff, BerkMin und effiziente Daten-Strukturen
      
      
      
      • BAPTISTA, L., I. LYNCE, J. MARQUES-SILVA:
        
        Complete search restart strategies for satisfiability.
        
        IJCAI 2001 Workshop on Stochastic SearchAlgorithms (IJCAI-SSA), August 2001.
      
      
      
      • GOLDBERG, E. Y. NOVIKOV: BerkMin:
        
        A Fast and Robust SAT-Solver.
        
        Design, Automation, and Test in Europe (DATE 2002), 142-149, March 2002.
      
      
      
      • LYNCE, I. J. MARQUES-SILVA:
        
        Efficient data structures for fast sat solvers
        
        2001
      
      
      
      • MOSKEWICZ, M.W., C.F. MADIGAN, Y. ZHAO, L. ZHANG, S. MALIK:
        
        Chaff: Engeneering an efficient SAT solver.
        
        Design Automation Conf., 2001.
      
      
      
      • ZHANG, LINTAO SHARAD MALIK:
        
        The quest for efficient boolean satisfiability solvers.
        
        Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002), 2002.
      
      
   
   
   
   4. MiniSAT und SATIRE
      
      
      
      • EEN, NIKLAS NIKLAS SÖRENSSON:
        
        An extensible sat-solver.
        
        SAT 2003, Chalmers University of Technology, Sweden, 2003.
      
      
      
      • WHITTEMORE, J., J. KIM, K. SAKALLAH:
        
        SATIRE: A New Incremental Satisfiability Engine.
        
        Design Automation Conference, 542-545, June 2001.
      
      
   
   
   
   5. Kühlmann et al.
      
      
      
      • KÃœHLMANN, A., V. PARUTHI, F. KROHM, M.K. M.K. GANAI:
        
        Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification.
        
        IEEE Trans. on CAD, 2002.
      
      
   
   
   
   6. CirCUs
      
      
      
      • JIN, HOONSANG, MOHAMMAD AWEDH, FABIO SOMENZI:
        
        CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking,
        
        LNCS 3114, 519-522. Springer-Verlag Heidelberg, July 2004.
      
      
      
      • JIN, HOONSANG FABIO SOMENZI:
        
        CirCUs: Hybrid satifiability solver.
        
        The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004. University of Colorado at Boulder, 2004.
      
      
   
   
   
   7. Verification
      
      
      
      • GOLDBERG, E., M. PRASAD, R. BRAYTON:
        
        Using SAT for combinational equivalence checking.
        
        Int'l Workshop on Logic Synth., 185-191, 2000.
      
      
      
      • MARQUES-SILVA, J.P. L. SILVA:
        
        Algorithms for satisfiability in combinational circuits based on backtrack search and recursive learning.
        
        Int'l Workshop on Logic Synth., 227-241, 1999.
      
      
   
   
   
   8. Bounded Model Checking
      
      
      
      • BIERE, A., A. CIMATTI, E.M. CLARKE, M. FUJITA, Y. ZHU:
        
        Symbolic model checking using SAT procedures instead of BDDs.
        
        Design Automation Conf., 1999.
      
      
      
      • BIERE, A., A. CIMATTI, E. CLARKE, O. STRICHMAN, Y. ZHU:
        
        Bounded model checking.
        
        Advances in Computers, 58, 2003.
      
      
      
      • BIERE, A., A. CIMATTI, E. CLARKE, Y. ZHU:
        
        Symbolic model checking without BDDs.
        
        Tools and Algorithms for the Constuction and Analysis of Systems 1579 LNCS. Springer Verlag, 1999.
      
      
      
      • CLARKE, EDMUND M., ARMIN BIERE, RICHARD RAIMI, YUNSHAN ZHU:
        
        Bounded model checking using satisfiability solving.
        
        Formal Methods in System Design, 19(1):7-34, 2001.
      
      
   
   
   




2. QSAT-Themen

   
   
   
   
   1. Evaluate (Cadoli et al.)
      
      
      
      • CADOLI, M., A. GIOVANARDI, M. SCHAERF:
        
        Experimental analysis of the computational cost of evaluating quantified boolean formulae.
        
        Lecture Notes In Artificial Intelligence, 1321:207-218, 1997.
      
      
      
      • CADOLI, MARCO, MARCO SCHAERF, ANDREA GIOVANARDI, MASSIMO GIOVANARDI:
        
        An algorithm to evaluate quantified boolean formulae and its experimental evaluation.
        
        08-99, Dipartimento di Informatica e Sistemica, Universita di Roma La Sapienza, Italy, Universita di Roma La Sapienza, Italy, March 1999.
      
      
      
      • CADOLI, MARCO, MARCO SCHAERF, ANDREA GIOVANARDI, MASSIMO GIOVANARDI:
        
        An algorithm to evaluate quantified boolean formulae and its experimental evaluation
        
        Journal of Automated Reasoning, 28(2):101?142, 2002.
      
      
   
   
   
   2. Jussi Rintanen (Freiburg)
      
      
      
      • GENT WALSH: Beyond NP:
        
        The QSAT phase transition.
        
        AAAI: 16th National Conference on Artificial Intelligence. AAAI / MIT Press, 1999.
      
      
      
      • RINTANEN, JUSSI:
        
        Improvements to the evaluation of quantified boolean formulae.
        
        IJCAI, 1192-1197, 1999.
      
      
      
      • RINTANEN, JUSSI:
        
        Partial implicit unfolding in the davis-putnam procedure for quantified boolean formulae.
        
        NIEUWENHUIS, R. A. VORONKOV (): International Conference on Logic for Programming,
        Artificial Intelligence and Reasoning (LPAR01), 2250 Lecture Notes in Computer Science, 362-376.
        Springer-Verlag, 2001.
      
      
   
   
   
   3. QuBE
      
      
      
      • GIUNCHIGLIA, ENRICO, MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        An analysis of backjumping and trivial truth in quantified boolean formulas satisfiability.
        
        Proc. 7 Congresso dell'Associazione Italiana per l'Intelligenza Artificiale, 2175 LNAI, Bari, September 2001.
      
      
      
      • GIUNCHIGLIA, ENRICO, MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        Backjumping for quantified boolean logic satisfiability.
        
        Proc. 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, Washington, USA, August 2001.
      
      
      
      • GIUNCHIGLIA, ENRICO, MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        Qube: A system for deciding quantified boolean formulas satisfiability.
        
        Proc. International Joint Conference on Automated Reasoning (IJCAR), 2083 LNAI, Siena, June 2001.
      
      
      
      • GIUNCHIGLIA, ENRICO, MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        Backjumping for quantified boolean logic satisfiability.
        
        Artificial Intelligence, 145(1-2):99-120, 2003.
      
      
   
   
   
   4. QuBE++
      
      
      
      • GENT, I., E. GIUNCHIGLIA, M. NARIZZANO, A. ROWLEY, A. TACCHELLA:
        
        Watched data structures for qbf solvers.
        
        LNCS: Theory and Applications of Satisfiability Testing, Selected Papers, 2919, 2003.
      
      
      
      • GIUNCHIGLIA, ENRICO, MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        Learning for quantified boolean logic satisfiability.
        
        Proc. 18th National Conference on Artificial Intelligence (AAAI), LNAI. AAAI.org, July 2002.
      
      
      
      • GIUNCHIGLIA, ENRICO,MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        Monotone literals and learning in qbf reasoning.
        
        Proc. 10th International Conference on Principles and Practice of Constraint
        Programming (CP?04), Toronto Marriott Downtown Eaton Centre, Canada, September 2004.
      
      
      
      • GIUNCHIGLIA, ENRICO, MASSIMO NARIZZANO, ARMANDO TACCHELLA:
        
        Qube++: an efficient qbf solver.
        
        Proc. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004), Austin, Texas, USA, November 2004.
      
      
      
      • ROWLEY, ANDREW G D:
        
        Watching clauses in quantified boolean formulae.
        
        APES-Group (Algorithms, Problems, and Empirical Studies), 2003.
      
      
   
   
   
   5. Gruppe Sharad Malik (Princeton)
      
      
      
      • RANJAN, DARSH, DAIJUE TANG, SHARAD MALIK:
        
        A comparative study of 2qbf algorithms.
        
        Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing
        (SAT2004), May 2004.
      
      
      
      • TANG, DAIJUE, YINLEI YU, DARSH RANJAN, SHARAD MALIK:
        
        Analysis of search based algorithms for satisfiability of quantified boolean formulas arising from circuit state space diameter problems.
        
        Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing
        (SAT2004), May 2004.
      
      
      
      • ZHANG, LINTAO SHARAD MALIK:
        
        Conflict driven learning in a quantified boolean satisfiability solver.
        
        Proceedings of International Conference on Computer Aided Design (ICCAD2002). ICCAD, November 2002.
      
      
      
      • ZHANG, LINTAO SHARAD MALIK:
        
        Towards symmetric treatment of conflicts and satisfaction in quantified boolean satisfiability solver.
        
        Proceedings of 8th International Conference on Principles and Practice of Constraint Programming (CP2002). Ithaca, NY, September 2002.
      
      
      
      
      
   6. SAT/QSAT-Solver Gruppe Armin Biere (ETH Zürich) / Stochasic Local Search
      für QBF (walkqsat)
      
      
      
      • BIERE, ARMIN:
        
        The evolution from limmat to nanosat.
        
        444, ETH Zürich, April 2004.
      
      
      
      • BIERE, ARMIN:
        
        Resolve and expand.
        
        Proceedings of 7th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2004), May 2004.
      
      
      
      • GENT, IAN P., HOLGER H. HOOS, ANDREW G. D. ROWLEY, KEVIN SMYTH:
        
        Using stochastic local search to solve quantified boolean formulae.
        
        Principles and Practice of Constraint Programming CP 2003, 2003.