Invited Paper: Satisfiability Testing: Recent Developments and Challenge Problems (at LICS 2000)

Authors: Bart Selman

Abstract

Recently, there has been much progress in the area of prepositional reasoning and search. Current techniques can handle problem instances with thousands of variables and up to a million clauses. This has led to new applications in areas such as planning, scheduling, protocol verification, and software testing. Much of the recent progress has resulted from a better understanding of the computational characteristics of the satisfiability problem. In particular, by exploiting connections between combinatorial problems and models from statistical physics, we now have methods that enable a much finer-grained characterization of computational complexity than the standard worst-case complexity measures. These findings provide insights into new algorithmic strategies based on randomization and distributed algorithm portfolios. I will survey the recent progress in this area and I will discuss the current state-of-the-art in propositional reasoning focusing on a series of challenge problems concerning propositional encodings, compilation techniques, approximate reasoning, robustness, and scalability.

BibTeX

  @InProceedings{Selman-SatisfiabilityTesti,
    author = 	 {Bart Selman},
    title = 	 {Satisfiability Testing: Recent Developments and Challenge Problems},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {178},
    location =   {Santa Barbara, CA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }