We proposae that a new "System Description" category be added to JSAT,
to supplement regular papers and Research Notes.
Our proposal is modeled after the "System Description" category in IJCAR
(formerly CADE), which has been ongoing for many years.

PROPOSAL DETAILS

The idea of the "System Description" category is that it
will be refereed papers that describe the internals of a SAT solver
without the usual requirements for a full paper.

The criterion of experimental evaluation will be relaxed, especially if
the paper can mention performance in a recognized competition.

The criterion of citing every paper written on clause learning
will be relaxed, but relevant cites predating the work will
still be expected.  Detailed comparisons will not.

Each paper will have an "as of" date clearly stated in the
abstract and the first sentence or so of the body.

The author is NOT required to address subsequent results!

The special criteria for this type of paper will be stated
to the referees, and referee reports that ask for
inappropriate changes will not be allowed to kill papers.

The system description category could be limited to 4 pages. This is the
page limit of CADE's system description.

People willing to use more space would be free to submit either a
research note or a regular JSAT paper (with the usual reviewing criteria).

MOTIVATION

According to google scholar, the two most cited papers of JSAT are
Minisat+ and picosat papers (resp. 132 and 55 citations).
http://scholar.google.fr/scholar?hl=3Dfr&q=3D&as_publication=3DJournal+on+Satisfiability%2C+Boolean+Modeling+and&btnG=3DRechercher&lr=3D&as_ylo=3D&as_vis=3D0

It clearly shows that there is an interest on system descriptions.

Generally, our view is that an author cannot be responsible for
citing every document that appears on somebody's personal page.

It took a lot of time for decision-stack shrinking in Jerusat,
clause-minimization in Minisat, etc., to be published.

As a consequence, most of those features have been used and references
were either done to the solver's source code or to the solver's
description.
Note that most information about solver competitions is on
personal pages, or the competitive event web pages.
So the 2-page descriptions for solvers found there cannot be considered
refereed research,and it is not really appropriate to require authors to
cite such casual documents (which may well be inaccurate, not having
been reviewed at all).

Having a new system description category would encourage people to
submit descriptions of their solvers to JSAT, thus allowing competitive
events to have archived system descriptions.