Guest Editors Conclusion

This special issue comprises six papers devoted to SAT solving and three papers devoted to MAXSAT solving. With two exception, the papers contain detailed information about some of the best solvers from the 5th SAT solver competition and from the 2nd MAX-SAT solver competition, which took place as side event of the 10th International Conference on Theory and Applications of Satisfiability Testing SAT 2007, in Lisboa/ Portugal. The paper by Heras, et al. deals with the contributed instances for the MAX-SAT evaluations and the paper by Argelich, et al. reports on the First and Second MAX-SAT evaluations in 2006 and 2007. The first paper PicoSAT Essentials presents three nice concepts: optimized compact data structures for watching literals, a new restart strategy, and an efficient proof encoding. Experiments demonstrate, that this low level optimization saves memory and speeds up the SAT solver considerably. The second paper Parallel SAT Solving using Bit-level Operations describes a technique for speeding up local search SAT solvers by using multi-bit Boolean operations, leveraging that k-bit CPUs can do k-bit Boolean operations in one time step. Modifying the state-of-the-art local search SAT solver Unit Walk according to this technic yields a much faster implementation than the original one. The third paper Whose side are you on? Finding solutions in a biased search-tree uses so called direction heuristics for selecting good assignments to the decision variables in order to guide the search into those parts of the search tree that are more likely to contain solutions. The SAT solver march ks, based on this idea was the winner of the crafted category during the SAT 2007 competition.