JSAT Addendum

JSAT Addendum covers information which is not yet suitable to be published by a Journal but still could mean a valuable contribution to the community. One could think of test data, claims, conjectures or preliminary results. JSAT Addendum also welcomes prepublications of papers submitted and/or accepted elsewhere. Authors using this option are considered responsible for alerting the EiC as soon as copyright conflicts emerge. In this case the contribution will be altered into a link to the Journal involved. JSAT Addendum is not a discussion forum.

Contributions to JSAT Addendum should not be referred to as JSAT journal papers.
However, contributions to JSAT Addendum will be screened by the editorial board as well, just to rule out invalid and useless information.

One may submit to JSAT Addendum by sending an email containing the material to the editor in chief. Contributors are asked to provide a title, a short list of key phrases ( plain text ) together with a pdf file covering their contribution, or to communicate the URL covering their contribution. In the latter case it is the contributors responsibility to maintain this link. Please check the JSAT Addendum Contents page to see how your contribution will be exposed. Please restrict to three or four lines only in your description. 

Information posted will be regularly screened on functionality and relevance: Contributors will be frequently asked to provide relevant data in cases of a follow up.

Contributions are indexed by date of submission ( year/month/day ).

JSAT Addendum Contents

2009-07-25. Magnus Bjork.
Successful SAT Encoding Techniques (PDF). This article identifies good practices for SAT encodings by analysing interviews with a number of well known SAT experts. The purpose is both to determine the confidence in different encoding strategies, by analysing whether there is consensus among the experts or not, as well as bringing out hidden knowledge to SAT users.
There is consensus that encoding techniques usually have a dramatic impact on the efficiency of the SAT solver, that it often takes much work to find a good encoding, and that the size of an encoding is only very loosely related to the hardness of finding a solution. Topics where the interviewers disagree include the feasibility of including artihmetics in SAT problems and whether to formulate problems as clauses or circuits.
This article describes a number of strategies that are good in different situations, such as different ways to represent numbers and how to use incrementality.

2007-10-16. Oliver Kullmann.
Constraint satisfaction problems in clausal form: Autarkies, deficiency and minimal unsatisfiability (PDF). This paper updates the 2005-04-08 JSAT Addendum contribution.
Abstract: The theory of autarkies, deficiency, irredundant and minimally unsatisfiable clause-sets as well as of hitting and multihitting clause-sets is generalised to non-boolean clause-sets. Applications and open problems are discussed. The text provides a full picture of the phenomena which are related to the notion of deficiency, and of the basic properties of irredundant (generalised) clause-sets and their cores.

2007-08-31. Miguel Anjos.
An Extended Semidefinite Relaxation for Satisfiability (PDF). This paper proposes a new semidefinite programming relaxation for the satisfiability problem. This relaxation is an extension of previous relaxations arising from the paradigm of partial semidefinite liftings for 0/1 optimization problems. We show that the proposed relaxation is exact for the important class of Tseitin instances, meaning that a Tseitin instance is unsatisfiable if and only if the corresponding semidefinite programming relaxation is infeasible.

2007-07-08. Hans Van Maaren et al.
Sums of Squares, Satisfiability and Maximum Satisfiability (PDF). This paper updates the 2005-07-05 JSAT Addendum contribution.

2005-08-05. Marijn Heule et al.
New lower bounds to Van der Waerden numbers (URL). Using a combination of symmetry reasoning, satisfiability solving and number theory, seven improved lower bounds to Van der Waerden numbers were established.

2005-07-05. Linda van Norden et al.
Sums of Squares, Satisfiability and Maximum Satisfiability (PDF). This paper updates the 2004-09-30 JSAT Addendum contribution. It contains detailed proofs, a new randomized rounding procedure and small size experimental data.

2005-07-05. Miguel Anjos.
An Explicit Semidefinite Characterization of Satisfiability for Tseitin Instances. Tseitin instances are known to be hard for many proof systems. The semidefinite programming characterization introduced is of dimension linear in the size of the instance, thus providing an explicit certificate of satisfiability or unsatisfiability in polynomial-time.
**Published in 2006:
M.F. Anjos. An Explicit Semidefinite Characterization of Satisfiability for Tseitin Instances on Toroidal Grid Graphs. Annals of Mathematics and Artificial Intelligence, Vol. 47 (3-4), 2006, 1-14.

2005-04-08. Oliver Kullmann.
Conjunctive normal forms with non-boolean variables, autarkies and hypergraph colouring (PDF). Key words: generalised satisfiability problems, no-goods, deficiency, autarkies, hypergraph colouring.

2004-11-11. Alexander Nadel.
Backtrack search algorithms for propositional satisfiability: Review and innovations (PDF). Master thesis, Hebrew University of Jerusalem, November 2002. It contains an overview of backtrack search SAT research and a description of the ideas behind Jerusat.

2004-09-30. Linda van Norden et al.
Sums of Squares, Satisfiability and Maximum Satisfiability (PDF). Key phrases: Hilbert's Positivstellensatz/ polynomials/ improvements on Goemans and Williamson and Feige and Goemans upper bounds for max 2-SAT/ Algebraic classification of Satisfiability.