Date: 04-Feb-2010 Title: Parallel Satisfiability Solving: SAT and beyond SAT, Parallel Solving on New Architectures Hits: 21 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, General Interest, call for papers         ==================================================================== SECOND CALL FOR PAPER ==================================================================== Call for papers WPSS'2010 A workshop on Parallel Satisfiability Solving: SAT and beyond SAT, Parallel Solving on New Architectures as part of the HPCS'10 Conference Le CENTRE DE CONGRES de CAEN Caen, Normandy, France June 28 -- July 2, 2010 http://cisedu.us/cis/hpcs/10/main/callForPapers.jsp ==================================================================== Submission Deadline: February 15, 2010 SCOPE AND OBJECTIVES 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. To date, the parallel SAT solving remains a challenging problem. In spite of the actual trend in processor development, which is moving from single-core to multi-core CPU, there exist few parallel solving works dedicated to the SAT problem. This workshop will focus on SAT and beyond SAT solving techniques exploiting parallelism within a context of High Performance Computing including massively parallel architectures such as Global Processing Units (GPUs) and Field-Programmable Gate Arrays (FPGAs). We invite papers in this emerging discipline which includes, but not limited to, the following areas of interest. - High Performance Computing for SAT, Max-SAT #SAT and QBF solving. - General-Purpose Computation on GPUs (GPGPU) for SAT* - Reconfigurable Computing and FPGA for SAT* - Parallel SAT* Pre-processing - Portfolios and/or Hybridized Algorithms within a Parallel Context IMPORTANT DATES Paper Submissions: ------------------------------------------- February 15, 2010 Acceptance Notification: ------------------------------------- March 15, 2010 Camera Ready Papers and Registration Due: -------------------- April 15, 2010 WORKSHOP ORGANIZERS Michael Krajecki, CReSTIC, Universite de Reims Champagne-Ardennes, France Email: michael.krajecki@univ-reims.fr Lakhdar Sais, CRIL, Universite d'Artois, France Email: sais@cril.univ-artois.fr Gilles Dequen, MIS, Universite de Picardie, France Email: gilles.dequen@u-picardie.fr International Program Committee: All submitted papers will be reviewed by the workshop technical program committee members following similar criteria used in HPCS. - Francois Bodin, IRISA, Rennes, France - Clementin Tayou Djamegni, University of Dschang, Cameroon - Youssef Hamadi, Microsoft Research Cambridge, U.K. - Marijn Heule, TU Delft, The Netherlands - Bertrand Le Cun, Universite de Versailles Saint-Quentin en Yvelines, France - Tobias Schubert, Albert-Ludwigs-University of Freiburg, Germany - Carsten Sinz, University of Karlsruhe, Germany - Peter Stuckey, University of Melbourne, Australia If you have any questions about paper submission or the workshop, please contact the Workshop organizers at the above addresses.

Date: 26-Jan-2010 Title: C. Domshlak, J. Hoffmann and A. Sabharwal (2009) "Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings", Volume 36, pages 415-469 Hits: 54 Contributed by: Daniel Le Berre Keywords: SAT application         Planning as satisfiability, as implemented in, for instance, the SATPLAN tool, is a highly competitive method for finding parallel step-optimal plans. A bottleneck in this approach is to *prove the absence* of plans of a certain length. Specifically, if the optimal plan has N steps, then it is typically very costly to prove that there is no plan of length N-1. We pursue the idea of leading this proof within solution length preserving abstractions (over-approximations) of the original planning task. This is promising because the abstraction may have a much smaller state space; related methods are highly successful in model checking. In particular, we design a novel abstraction technique based on which one can, in several widely used planning benchmarks, construct abstractions that have exponentially smaller state spaces while preserving the length of an optimal plan. Surprisingly, the idea turns out to appear quite hopeless in the context of planning as satisfiability. Evaluating our idea empirically, we run experiments on almost all benchmarks of the international planning competitions up to IPC 2004, and find that even hand-made abstractions do not tend to improve the performance of SATPLAN. Exploring these findings from a theoretical point of view, we identify an interesting phenomenon that may cause this behavior. We compare various planning-graph based CNF encodings F of the original planning task with the CNF encodings F_abs of the abstracted planning task. We prove that, in many cases, the shortest resolution refutation for F_abs can never be shorter than that for F. This suggests a fundamental weakness of the approach, and motivates further investigation of the interplay between declarative transition-systems, over-approximating abstractions, and SAT encodings.

Date: 25-Jan-2010 Title: M. Pradella, S. Crespi Reghizzi, A SAT-based parser and completer for pictures specified by tiling, Pattern Recognition, Vol 41, pp 555-566, 2008 Hits: 49 Contributed by: Daniel Le Berre Keywords: SAT application         Abstract Pictures or patterns have been formally specified by different methods such as grammars. An alternative approach is based on Tiling Systems (TS) (Wang tiles are an analogous and equivalent formalism), whereby the picture is obtained by first covering it with a specified set of two by two tiles, then by performing a pixel by pixel mapping. TS are a powerful technique: the corresponding pictures can be recognized by non-deterministic cellular au- tomata, which are more powerful then the four ways automata. The difficulty to write such specifications for non elementary pictures, and the NP-complete computational complexity of TS picture recognition have so far blocked any attempt to application. We have imple- mented a recognizer and generator for TS pictures in a very attractive, unconventional way, by transforming the tiling problem into a SAT (Boolean Satisfiability) one, then using an efficient off-the-shelf SAT-solver. The prototype is fast enough to experiment on reasonably sized samples, and has the bonus of being able to complete or extrapolate a partial or noisy picture. The tool is invaluable to assist in writing picture specification. A series of examples shows how to specify patterns using TS.

Date: 25-Jan-2010 Title: LoCoCo 2010 -- Workshop on Logics for Component Configuration Hits: 28 Contributed by: Inęs Lynce Keywords: Computational logic, Benchmark, SAT application, null         Workshop of SAT at FLoC 2010, Edinburgh, Scotland, July 10, 2010 First Call for Papers Scope: ====== Modern software distributions are based on the notion of components, which denote units of independent development and deployment. Components provide the necessary flexibility when organizing a complex software distribution, but also are a challenge when it comes to selecting components from a large repository of possible choices, and configuring these components according to user needs, resource constraints, and interdependencies with other components. Representing and solving configuration problems is a hot topic of great importance for many application domains. Some well-known examples of complex systems of components in the world of Free and Open Source software are the different distributions for GNU/Linux, BSD, or Eclipse plugins. Understanding and solving these questions is an attractive research topic since the problems to be solved are complex and interesting for researchers working on solving techniques, and on the other hand have the potential of high impact on the way the software we all use everyday is developed and deployed. Not only adequate logical formalisms to represent a configuration problem are required, but also sophisticated reasoning technologies to deal with large amounts of data. Further relevant aspects include diagnosis of failed configuration settings and an intelligent behavior dealing with user preferences. This workshop will focus on logic-based methods for specifying and solving complex configuration problems for software components. The goal of the workshop is to bring together both researchers and practitioners active in the area of component configuration of software systems, using different modeling and solving techniques, such as constraint and logic programming, description logics, satisfiability and its extensions. The workshop will be an opportunity to discuss common and complementary solutions for solving component configuration. Invited Talk ============ An invited talk will be given by Carsten Sinz (University of Karlsruhe). MISC 2010 ========= The first Mancoosi International Solver Competition will be held in conjunction with the LoCoCo workshop. Important Dates =============== Friday, March 26 Submission deadline Friday, April 23 Notification about acceptance Friday, May 21 Final paper due Saturday, July 10 Workshop Submission and Publication ========================== We welcome submissions of various types of presentations related to the topics of the workshop, such as - full research papers - abstracts of ongoing work - tutorial overview papers - summaries of research projects - system descriptions, if possible including system demonstration at the workshop. These must provide the means to download and evaluate the system, with preference to distribution under an open source licence. Program Committee ================= Daniel Le Berre (Universite d'Artois, France) Roberto Di Cosmo (Universite Paris-Diderot, France) Georg Gottlob (Oxford University, UK) Pascal van Hentenryck (Brown University, USA) Matti Jarvisalo (University of Helsinki, Finland) Ines Lynce (INESC-ID, Lisbon, Portugal), co-chair Toni Mancini (Sapienza Universita di Roma, Italy) Albert Oliveras (Technical University of Catalonia, Barcelona, Spain) Christian Schulte (KTH, Stockholm, Sweden) Ralf Treinen (Universite Paris-Diderot, France), co-chair Nic Wilson (UCC, Cork, Irland)

Date: 25-Jan-2010 Title: SAT 2010 - Final Call for Papers Hits: 34 Contributed by: Stefan Szeider Keywords: call for papers         SAT 2010 - Final Call for Papers 13th International Conference on Theory and Applications of Satisfiability Testing Edinburgh, Scotland, UK Part of FLoC 2010 Abstract Submission: February 1, 2010 Paper Submission: February 8, 2010 Author Notification: March 15, 2010 Final Version: April 5, 2010 Conference: July 11 - July 14, 2010 For submission details see the conference web-site: http://ie.technion.ac.il/SAT10

Date: 13-Jan-2010 Title: Internships at Microsoft Research, Cambridge Hits: 71 Contributed by: lucas bordeaux Keywords: General Interest         The Microsoft Research Constraint Reasoning Group is offering several three-month internship positions. Jobs are open to PhD students and to post-doctoral researchers with a primary interest in search and optimization. We welcome in particular applicants that have complementary interests in: Online Stochastic Optimization Graphical models Problem decomposition Automated planning Monte-Carlo techniques The goal of these internships is to conduct fundamental research driven by long term Microsoft applications. More information about the MSRC internship program can be found here. Interested applicants have to register here. Work location: Cambridge, United Kingdom. Duration: 12 weeks. Required availability: Summer, fall 2010. Contact: {romatees, lucasb} at Microsoft dot com Thanks for forwarding to interested parties.

Date: 27-Dec-2009 Title: SAT 2010 - Second Call for Papers Hits: 102 Contributed by: Stefan Szeider Keywords: null         SAT 2010 - Second Call for Papers 13th International Conference on Theory and Applications of Satisfiability Testing Edinburgh, Scotland, UK Part of FLoC 2010 Abstract Submission: February 1, 2010 Paper Submission: February 8, 2010 Author Notification: March 15, 2010 Final Version: April 5, 2010 Conference: July 11 - July 14, 2010 For submission details see the conference web-site: http://ie.technion.ac.il/SAT10

Date: 17-Dec-2009 Title: Tarmo: A Framework for Parallelized Bounded Model Checking Hits: 130 Contributed by: Siert Wieringa Keywords: BMC, Verification, null, null, null         The following paper and the software described in it is now available online: Siert Wieringa, Matti Niemenmaa and Keijo Heljanko, Tarmo: A Framework for Parallelized Bounded Model Checking, In Lubos Brim and Jaco van de Pol, editors, Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC09), volume 14 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 62-76, 2009. Our Tarmo framework is an approach to parallelizing BMC by parallel SAT solving of the sequence of incrementally encoded SAT instances that follow from a single BMC task. The satisfiability of an instance in such a sequence corresponds to the existence of a counterexample of a specific length. The available Tarmo software implements our generic shared clause database architecture which allows sharing clauses between SAT solver processes that are working on possibly different instances from one such sequence.

Date: 15-Dec-2009 Title: Alexander Nadel, August 2009, “Understanding and Improving a Modern SAT Solver”. PhD thesis, Tel Aviv University. Hits: 198 Contributed by: Nadel Alexander Keywords: DPLL, Intelligent Backtracking, Learning, branching heuristics, variable ordering heuristic, Resolution proof, null, null, null, null         This work proposes a new framework for understanding a modern SAT solver as well as a number of empirically useful enhancements. We start with providing a version of the basic backtracking algorithm that explicitly shows the process of resolution refutation construction. Our approach is based on the notion of a parent resolution derivation – a resolution proof for validness of a flip operation. We show how to derive the algorithm of a modern SAT solver from basic backtracking step-by-step. This resolution-based approach allows us to define new criteria for measuring the practical impact of different schemes for conflict-driven learning by making the notion of search pruning more formal. We show that the 1UIP scheme, enhanced by conflict clause minimization, is better than other known schemes in terms of search pruning. This explains its empirical advantage over other schemes. We propose an enhancement to the minimized 1UIP scheme, called local conflict clause recording. This technique improves the performance of a modern SAT solver by recording additional conflict clauses. Local conflict clause recording makes the learning less dependent on the variable polarity selection heuristic. Assignment stack shrinking is a technique whose goal is to shrink the size of the assignment stack and conflict clauses. We demonstrate the empirical usefulness of assignment stack shrinking and analyze its impact on the performance of a modern SAT solver, comparing it to the impact of conflict clause minimization and rapid restarts. Furthermore, a new practically useful decision heuristic for SAT, called the clause-based heuristic (CBH), is introduced. This heuristic is designed to increase the likelihood that interrelated variables will be chosen in proximity. It maintains a clause list containing both the initial and conflict clauses. The next decision literal is picked from the first unsatisfied clause. We propose various methods for initially organizing the clause list and for moving clauses within it. Finally, we present an algorithm for minimal unsatisfiable core extraction that is able to find a minimal unsatisfiable core for large real-world formulas. Our method manipulates the resolution refutation, generated by a modern SAT solver, so that in the end all the input clauses, connected to the empty clause, comprise the minimal unsatisfiable core.

Date: 06-Dec-2009 Title: ManySAT 1.1 Hits: 153 Contributed by: Youssef Hamadi Keywords: null         Dear all, The ManySAT source code is now online here. If you use it in your research or in any application, please send us a small email, and we will put you in our list of known users. We hope that this new resource will benefit to the whole SAT community! Bests, Said, Lakhdar, and Youssef