SAT Live!

Pragmatics of SAT a workshop of the SAT conference within the Federated Logic Conference (FLoC) 2010 July 10, 2010 - Edinburgh, Scotland, UK The aim of the pragmatics of SAT workshop is to allow researchers concerned with the design of efficient SAT solvers or SAT encodings to meet and discuss about their latest results. The workshop is also the place for users of SAT technology to present their applications. This workshop follows the spirit of Pragmatics of Decision Procedures in Automated Reasoning organized at FLoC 2006. Topics Main areas of interest include, but are not restricted to: * techniques for debugging or certifying solvers * visualisation of benchmarks structure * monitoring solver behaviour * evaluation of solvers * efficient data structures * domain specific encodings * taking into account multi-core technology * domain specific heuristics * new application of sat technology * system/library description Submission There are two possible type of submissions for the workshop. The papers are supposed to be submitted electronically through EasyChair as a PDF file using the LNCS style (the same as the SAT conference). http://www.easychair.org/conferences/?conf=pos10 * Regular papers (up to 14 pages). Accepted papers will be published in the CEUR-WS electronic proceedings. * System descriptions (up to 6 pages). Accepted papers will be published in the JSAT journal, in the new system description category. The final format of the paper will be different: system descriptions will be published as a 4 page JSAT style while regular paper will use a specific workshop style. Authors should provide enough information and/or data for reviewers to confirm any performance claims. This includes links to a runnable system, access to benchmarks, reference to a public performance results, etc. The system description category especially targets the authors of the systems that enter the SAT 2010 conference competitive events (SAT Race 2010, PB 2010, MAXSAT 2010, QBFEVAL 2010, ...). The aim of this workshop is to push forward peer-reviewed published system descriptions as a means to spread technical information regarding the design of solvers. System descriptions are expected to describe briefly but precisely the main features of the system, in a specific version. Regular papers provide more space to describe in detail a full system or application, provide experimental results, etc. Important dates * Submission deadline: March 26, 2010. * Authors notification: April 23, 2010. * Final version due: May 15, 2010. * The workshop will take place on July 10th, 2010. Tutorial by Youssef Hamadi: From Parallel SAT to Distributed SAT This tutorial will present an overview of parallelism in SAT. It will start with a presentation of classical divide and conquer techniques, discuss their ancient origin and compare them to more recent portfolio-based algorithms. It will then present the impact of clause-sharing on their performances and discuss various strategies used to control the communication overhead. A particular technique used to control the classical diversification/intensification tradeoff will also be presented. Finally, perspectives will be given which will relate the current parallel SAT technologies to the expected evolution of computational platforms, leading to distributed SAT solving scenarios. Programme Committee * Josep Argelich * Armin Biere * Youssef Hamadi * Daniel Le Berre * Olivier Roussel * Carsten Sinz * Armando Tacchella * Allen Van Gelder

Context and scientific objectives: SAT (decide if a Boolean formula, typically in conjunctive normal form, admits a valuation which makes it true?) is a fundamental problem in complexity theory with very large practical benefits. Modern SAT solvers can now handle propositional satisfiability problems with hundreds of thousands of variables or more. However, many practical instances remain difficult to all the available SAT solvers. Consequently, new approaches are clearly needed to solve these challenging industrial problems. In this context and with the light of the next generation of computer architectures, the design of parallel satisfiability solvers becomes a fundamental issue. The aim of this PhD is to provide new theoretical and practical advances for parallel satisfiability solving. Laboratory: CRIL - CNRS UMR 8188, Université d'Artois, Lens, France Supervision: Pr. Lakhdar Sais, CRIL, Lens, France Dr. Youssef Hamadi, Microsoft Research, Cambridge, UK Application: please send : CV, motivation letter, recommendation letters to : sais@cril.fr

Bit-parallel Learning from Generic Assignments We present a technique to learn new clauses from a set of assignments, which is inspired by the learning rules of Stalmarck’s proof procedure. Central in the proposed learning method is the concept of generic assignments – a set of 2n assignments that covers all possible truth values on n Boolean variables. Given a 2n bit computer, one can store generic assignments of that size efficiently. Further, such assignments can be extended with unit propagation in parallel. We show that various learning rules can be applied in parallel as well. BitFall is a SAT-solver based on these ideas. It is complete and uses breadth-first search – similar as the HeerHugo solver. We offer some first experimental results of BitFall on hard random 3-SAT formulas. Our algorithm seems to work surprisingly well on unsatisfiable instances. Applying Extended Resolution and Forced Patterns on Random 3-SAT instances In this study we aim to improve the runtime of the state-of-the-art March SAT solver. We apply a technique known as extended resolution on uniform random 3-SAT formulae; we add additional clauses, derived from the original formula, trying to guide the solver into the direction of a viable solution. Depending on a heuristic which we introduce, we add certain patterns to the formula to aid the solver. This method will be tested both unforced and forced: the unforced method lets the solver choose whether to include the additional clauses or not, in forced solving the patterns are used anyway. The latter might turn a satisfiable problem into an unsatisfiable one, however results still are very promising: a speed up of about 18% on the average. Also, at the end of this document some valuable insights into new studies can be found, which may lead to even more substantial improvements.

Call for papers WPSS A workshop on Parallel Satisfiability Solving: SAT and beyond SAT, Parallel Solving on New Architectures as part of the HPCS'09 Conference June 21 - 24, 2009 Leipzig, Germany Submission Deadline: March 22, 2009 During the last decade, the fundamental Satisfiability Problem (SAT) has been extensively studied. This interest of the community significantly grows because of its conceptual simplicity and its ability to describe a wide set of various problems, including hardware verification, planning, automated reasoning, and others. Consequently, there is an increasing demand for high performance SAT-solving algorithms in industry. In spite of the actual trend in processor development, which is moving from single-core to multi-core CPU, there exist few parallel solving approaches dedicated to SAT problems using shared memory architectures. This workshop will focus on SAT and beyond SAT solving techniques exploiting parallelism in emerging massively multi-threaded and multi-core architectures. Recently, Global Processing Units (GPUs) have evolved to address programming of general-purpose computations. We will particularly focus on the use of general-purpose GPUs and coprocessor computing techniques to overcome traditional barriers to parallelization. We invite papers in this emerging discipline which includes, but not limited to, the following areas of interest. - Satisfiability Solving Using Shared Memory - General-Purpose Computation on GPUs (GPGPU) for SAT - Reconfigurable Computing and FPGA for SAT - Parallel SAT, MaxSAT, #SAT and QBF pre-processing Important Dates: - Paper Submissions: March 22, 2009 - Acceptance Notification: April 10, 2009 - Camera Ready Papers and Registration Due: April 24, 2009 Workshop Organizers: - Michael Krajecki, CReSTIC, Univ. de Reims Champagne-Ardennes, France : michael.krajecki@univ-reims.fr - Lakhdar Sais, CRIL, Univ. d'Artois, France : sais@cril.univ-artois.fr - Gilles Dequen, MIS, Univ. de Picardie, France : gilles.dequen@u-picardie.fr Workshop Program Committee: All submitted papers will be rigorously reviewed by the special session technical program committee members. - François Bodin, IRISA, Rennes, France - Youssef Hamadi, Microsoft Research Cambridge, U.K. - Tobias Schubert, Albert-Ludwigs-University of Freiburg, Germany - Bertrand Le Cun, Université de Versailles Saint-Quentin en Yvelines, France - Carsten Sinz, University of Karlsruhe, Germany

Journal on Satisfiability, Boolean Modeling and Computation ISSN 1574-0617 Special Issue on Parallel SAT Solving Call for Papers Deadline for paper submission: November 30th, 2008 Guest Editor Youssef Hamadi, Microsoft Research youssefh at microsoft dot com. General Information Recent years have shown a major architectural shift in computer hardware. The traditional efficiency gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall and performance improvements have to be found elsewhere. The new direction is to add more computing units (cores) to a chip in order to raise its computational power. The products resulting from this multi-core strategy are now on every desktop and yet the horizon is wide open since the number of cores is expected to grow exponentially. This technological shift represents an important challenge for many computer sciences fields whose best algorithms have to be rethought for multi-core-based parallelization. The goal of this special issue is to officially acknowledge this evolution, and to present recent advanced in the parallel processing of SAT problems. Topics We welcome the submission of works related to the parallel processing (shared-memory and/or message-passing based) of SAT, MAX-SAT and QBF problems. Submission This special issue welcomes original high-quality contributions that have been neither published in nor submitted to any journals. All submissions should be written in terms understandable by general readers of the journal. All submissions will be refereed according to JSAT standards, as described at JSAT web page. Submissions should be written in LaTeX and formatted with JSAT LaTeX style file according to JSAT's author guidelines, and should not exceed 20 pages. Submissions should be emailed to youssefh at microsoft dot com within the deadline marked above. About JSAT JSAT is a peer-reviewed journal which is freely distributed electronically and published in print by IOS Press. The scope of JSAT is propositional reasoning, modeling and computation, and related topics. JSAT publishes high-quality original research papers and survey papers which evidently contribute to deeper insight on a SAT-related topic.

Guest Editor

Youssef Hamadi, Microsoft Research - youssefh at microsoft dot com.

General Information

Recent years have shown a major architectural shift in computer hardware. The traditional efficiency gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall and performance improvements have to be found elsewhere. The new direction is to add more computing units (cores) to a chip in order to raise its computational power. The products resulting from this multi-core strategy are now on every desktop and yet the horizon is wide open since the number of cores is expected to grow exponentially. This technological shift represents an important challenge for many computer sciences fields whose best algorithms have to be rethought for multi-core-based parallelization. The goal of this special issue is to officially acknowledge this evolution, and to present recent advanced in the parallel processing of SAT problems.

Topics

We welcome the submission of works related to the parallel processing (shared-memory and/or message-passing based) of SAT, MAX-SAT and QBF problems.

Submission

This special issue welcomes original high-quality contributions that have been neither published in nor submitted to any journals. All submissions should be written in terms understandable by general readers of the journal. All submissions will be refereed according to JSAT standards, as described at JSAT web page. Submissions should be written in LaTeX and formatted with JSAT LaTeX style file according to JSAT's author guidelines, and should not exceed 20 pages. Submissions should be emailed to "youssefh at microsoft dot com" within the deadline marked above.

About JSAT

JSAT is a peer-reviewed journal which is freely distributed electronically and published in print by IOS Press. The scope of JSAT is propositional reasoning, modeling and computation, and related topics. JSAT publishes high-quality original research papers and survey papers which evidently contribute to deeper insight on a SAT-related topic.