First Birthday
Daniel Le Berre
So there are useful SAT related materials available on the web. But how to access them? One solution is to bookmark the personal web pages of all researchers working on SAT, and take a look every now and them to see if some new information is available. Another way is to construct a web page (a site) dedicated to SAT, that will concentrate the information about that subject. But still, someone needs to go through all the SAT related pages every now and then to maintain and keep up-to-date that page.
This could be a solution if you know who is working on the subject. Now suppose that a new community is getting interested in SAT (model checking community, for instance). People from that community can begin to publish new results about SAT but you won't notice them because you may not be aware of that pool of web pages from that community. Suppose also that some people are mainly interested in SAT as users: they typically want to know what the recent SAT solvers are, the most recent techniques, etc. They may not be aware of who is working in that area.
What does it mean? A ``portal" for SAT related research should be open, that is should allow anybody from any community to point out a particular work or tool related to SAT. If anybody can contribute to the site, it is unlikely that the information will be clustered in only one community. Furthermore, by sharing the update with other people, the effort to do it is minimized. These are the ideas I had in mind when I conceived of SAT Live!.
But some web sites about SAT already exist. Let us briefly mention two of them.
SATLIB contains collections of benchmarks, solvers, an annotated bibliography, a list of people, links and conferences related to SAT.
The collection of benchmarks is certainly the origin of the success of SATLIB: benchmarks do not evolve, and there are usually not a profusion of new ones every year, so it is easy to maintain an up-to-date collection of benchmarks. By centralizing the access to some benchmarks and providing a detailed information about them, SATLIB certainly did (and still do) a great job for the SAT community.
The collection of SAT solvers is somewhat more difficult to maintain: new versions of the solvers can appear (which add new features or correct bugs), and new solvers will appear. Usually, the best way to obtain up-to-date information about these solvers it to take a look to the author's web page (which means that you must be aware of their existence). However, by keeping older versions of the solvers online, one can use exactly the version of a solver described in a paper. SATLIB SAT solvers collection is also very useful in that regard.
The annotated bibliography is a pretty good idea. It contains a lot of SAT related papers published in major conferences or journals. All the references have a link to an electronic version of the paper. So it is easy to get the ones you do not know about. Lastly, the keywords help to situate each paper.
If there is one criticism that can be made about SATLIB, it is the infrequent updates of the site: 14 updates in 3 years is not a lot! One reason the update is infrequent is related to the design of the site. The site is based on static web pages that must be updated by their webmaster.
Laurent Simon [SC01] dedicated one entire site to that subject more than one year ago with SAT-Ex. It uses dynamic HTML to display experimental results from various complete SAT solvers stored in a database. The great thing with SAT-Ex is the way you manage the information. One can display the results of solvers from a group of benchmarks to a single instance. Furthermore, new solvers and benchmarks can be added to the database. (Chaff[MMZ$^+$01] have been added on SAT-Ex a few days after its availability for instance). It is a great tool to compare complete SAT solvers. SAT-Ex currently contains 23 SAT solvers and 1303 benchmarks. It allows to point out challenging instances, namely the benchmarks not solved by any solver, or the ones solved by only one or two solvers (which also emphasizes these solvers). Furthermore, all the information displayed on the site can be freely downloaded and processed for customized needs. (Note that the last version of the site, 2.0, allows a lot of customization online).
It is interesting to take a look to the most visited links through SAT Live!. The first one is the web page of the new Chaff solver (more than 200 hits in 3 months), the second a paper concerning SAT-based software verification (almost 200 hits in 10 months) and the last one is a link to SAT20001 workshop online proceedings (almost 150 hits in more than one month).
How to contribute?
You can either post a link anonymously, in which case there is no particular requirement, or not, in which case you must subscribe to SAT Live! first. (Please note that subscribing does not mean you will appear on the people page or receive email notifications: you can set your preferences.) In the first case, just type anonymous instead of your email. Then you need to classify your link, and provide a title, a URL and a comment about the link. You must check that the information you provided displays correctly using the preview button. When everything is fine, you can go to the next step to choose some keywords for your link. It should appear on the home page automatically after that.
Another way to get an idea of who is using SAT Live! is to take a look at the statistics of the site (freely available to anybody). One can check that the number of hits is growing since the beginning of the year (the stats for January and February are no longer appearing because I lost the logs due to a misconfiguration of the server logs rotation). One can recognize among the organizations accessing to the site some well known from the Electronic Design Automation community.
One can also take a look at the referrer pages to see where people are coming from. A lot of people are coming from search engine results on queries such as ``SAT" or ``Chaff", which means that SAT Live! is well known from these search engines. Else people are mainly coming from web pages of SAT researchers referring the site.
Few discussions ran on the forums: I tried twice to launch a thread about a common API for SAT solvers but only a few people participated and nothing really happened. However, this thread was reopened shortly after SAT2001 by someone from Compaq, providing useful information about the expectation of people working with SAT solvers in hardware verification.
I hope that the new features that will be available soon on the forum will encourage people to use it.
One day, I got the idea to share the bibtex file using Concurrent Version System (CVS), a tool widely used for distributed programming projects. It means that you need a CVS client to participate to that project. It is therefore a bit more technical than filling a form in a web page but some tools (like emacs) can help.
How does it work?
There are two bibtex files maintained in the SATBIB project: confs.bib and satbib.bib. The first one groups proceedings references of major conferences not dedicated to SAT (IJCAI, AAAI, etc.). The second one contains SAT related references using crossreferences to the conference proceedings appearing in confs.bib. You can download the latest version of these files from the SATBIB web page. If you want to contribute references to these files, you need to setup a CVS client as described in the SATBIB web page.
The SAT community is certainly smaller than the Agent one, but I think that the same kind of result could be obtain if people working around SAT were promoting their work through SAT Live!.
Why SAT Live! ? Well, the main reason is that it exists and can be used for that purpose ;-=). Another one is that you are sure that at least the people subscribed to the site will be aware of your work, plus all the visitors not subscribed. As already pointed out, search engines a pretty aware of SAT Live! existence so your work is also likely to be caught by the search engines.
For people still not convinced by the importance of the web to spread scientific information, a study from ResearchIndex shows that papers available on the web are more highly cited. Another good reason to use SAT Live! to promote your work is that both ResearchIndex and BDLP are using it as a source of new documents (you can check that on the stats).
I use an open source forum tool called Jive for the forum feature. One of the annoying thing with the current forum is that people cannot have an email notification of the discussions running on the forums. This feature will be available in the version 2.0 of the tool. I will update the SAT Live! forum when it will be available.
Another thing is the design of the site. I tried to do my possible to make the site looking attractive and user friendly, but I think it can be much better. One student from the Design department of the University of Newcastle kindly proposed to help me to improve SAT Live! in that way.
SAT Live! is a web site dedicated to SAT that can be updated by anybody in a pure anarchical way. It's main aim is to be a portal to SAT related research, where both users and researchers can meet. It is open to anybody: academics as well as industrials or hobbyists, from any background. It should be considered as a tool to promote SAT related work.
SAT Live! is currently more used as a source of information than as a mean to share information. It looks like a site cannot belong to a community but to someone. For instance, a few people still ask me to add a link to their site or paper, or to add them on the people page: they can do that by themselves! I take the responsability to maintain this site online, to provide a tool. The content of the site itself mainly depends on SAT Live! users.
Because I am currently the main contributor of the site (67 persons are currently subscribed to the site, but few of them are contributing links), the current picture of SAT research drawn by SAT Live! is a bit biased: it denotes much more my own interests concerning that problem than what's really going on. For instance, I think that the work in Theoretical Computer Science and most of the work concerning incomplete methods for SAT are not currently well represented in SAT Live!. A few people from various background contributing links related to their own interests could fix that.
I think that the major contribution of SAT Live! so far is to reach researchers from both SAT and Model Checking background. I am pretty happy of the recent link concerning the special issue on SAT at the Microprocessor Test and Verification (MTV'02) conference. It shows that SAT-based tools are currently considered seriously.
Finally, I mentioned that a few companies from EDA are currently looking at SAT Live!. They are welcome to participate to the site, by providing more information about the type of problem they want to solve, providing some benchmarks, or participating to standardization efforts.
I tried to explain in this paper the main reasons that pushed me to create this site. I would be happy to have your feedback about it on SAT Live!forum.
Symbolic Model Checking without BDDs.
In Proceedings of Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), number 1579 in LNCS, 1999.
SATLIB: An Online Resource for Research on SAT.
In Ian Gent, Hans van Maaren, and Toby Walsh, editors, SAT20000: Highlights of Satisfiability Research in the year 2000, Frontiers in Artificial Intelligence and Applications, pages 283-292. Kluwer Academic, 2000.
Pushing the envelope : Planning, propositional logic, and stochastic search.
In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI'96), pages 1194-1201, 1996.
Chaff: Engineering an Efficient SAT Solver.
In Proceedings of the 38th Design Automation Conference (DAC'01), June 2001.
SATEx: a web-based framework for SAT experimentation.
In Henry Kautz and Bart Selman, editors, Electronic Notes in Discrete Mathematics, volume 9. Elsevier Science Publishers, June 2001.
http://www.lri.fr/ simon/satex/satex.php3.