T-79.194 Tietojenkäsittelyteorian seminaari
Kevät 2003

Seminaariesitelmän aiheita

"Kokeellinen" suoritustapa

• zchaff
  Ks. esim. DAC2001 ja ICCAD 2001 paperit [link]
  
• berkmin
• OKsolver
• satz
• 2clseq
  Ks. esim. AAAI-2002 ja SAT-2002 paperit [link]
  
• Walksat
• unitwalk
  Ks. esim. CP'01 paperi [link]
  
• sp
  Ks. esim. Preprint 2002 [link]
  

"Kirjallinen" suoritustapa

• [DGH+02]: Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon Kleinberg, Christos Papadimitriou, Prabhakar Raghavan, and Uwe Schöning, Deterministic $ (2-2/(k+1))^n$ algorithm for $k$-SAT based on local search. Theoretical Computer Science 289 (2002) 69-83. [link]
• [Sch99]: Uwe Schöning, A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems, Proc. of the 40th Annual Symposium on Foundations of Computer Science, October 17 - 18, 1999 New York, New York, Pages: 410-414 [link] +
  T. Hofmeister, U. Schöning, R. Schuler, O. Watanabe, A probabilistic 3-SAT algorithm further improved'', Proceedings 19th Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 2285, 2002, pages: 192-202 [link]
• [PPSZ98]: Paturi, R.; Pudlik, P.; Saks, M.E.; Zane, F., An improved exponential-time algorithm for k-SAT, Proc. of the 39th Annual Symposium on Foundations of Computer Science, 1998, Pages: 628-637. [link] +
  Paturi, R., Pudlak, P., Zane, F., Satisfiability Coding Lemma, Proc. of the 38th Annual Symposium on Foundations of Computer Science, 1997, pages: 566-574. [link]
• [WvM00]: Joost P. Warners, Hans van Maaren, Solving satisfiability problems using elliptic approximations - effective branching rules, Discrete Applied Mathematics 107 (2000), 241-259.
• [Hir00]: E. A. Hirsch, New Worst-Case Upper Bounds for SAT. Journal of Automated Reasoning 24(4): 397-420, 2000. [link]
• [Gol02]: Proving Unsatisfiability of CNFs Locally, Journal of Automated Reasoning 28 (2002) 4, 417-434. [ps]
• [SW97]: Y. Shang and B. W. Wah, A Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems Journal of Global Optimization, Kluwer Academic Publishers, vol. 12, no. 1, Jan. 1998, pp. 61-99. [link]
• [VG99]: A. Van Gelder, Autarky pruning in propositional model elimination reduces failure redundancy, Journal of Automated Reasoning, 23 (1999) 2, 137-193.
• [Dar01]: A. Darwiche, Decomposable negation normal form, Journal of the ACM 48 (2001) 4, 608-647 (Ei lukua 5).
• [SS00]: M. Sheeran and Gunnar Stålmarck, A tutorial on Stålmarck's proof procedure for propositional logic, Formal Methods in System Design 16 (2000), 23-58.
• [RR00]: E. Thomas Richards, Barry Richards, Nonsystematic Search and No-Good Learning, Journal of Automated Reasoning 24 (2002) 4, 483-533.
• [RD00]: I. Rish and R. Dechter, Resolution versus Search: Two Strategies for SAT, Journal of Automated Reasoning 24 (2000) 1-2, 225-275.
• [ARMS02]: Fadi A. Aloul, Arathi Ramani, Igor L. Markov, and Karem A. Sakallah, Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry, CSE-TR-463-02, University of Michigan, September 2002. [pdf]
• [ARMS02-2] F.A.Aloul, A.Ramani, I.L.Markov and K.A.Sakallah, Generic ILP versus 0-1 Specialized ILP: An Update, CSE-TR-461-02, University of Michigan, August 2002. [pdf]