Deadline Countdown

Heads up on SAT research

SAT related books

Other SAT related sites

Date: 16-Jul-2010 Title: Parallel SAT Solving on Peer-to-Peer Desktop Grids Hits: 191 Contributed by: Sven Schulz Keywords: SAT tools, Distributed Computing, distributed parallel dynamic learning, Divide-and-Conquer Algorithms, null, null         An article on "Parallel SAT Solving on Peer-to-Peer Desktop Grids" has been published in the Journal of Grid Computing (Springer). Abstract "Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domain-specific problems inherent to one of the most challenging environments for parallel computing - Peer-to-Peer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as well as non-uniform communication costs. This is achieved through a sophisticated distributed task pool execution model, problem size reduction through multi-stage SAT formula preprocessing, context-aware memory management, and adaptive topology-aware distributed dynamic learning. Despite the demanding conditions prevailing in Desktop Grids, Satciety achieves considerable speedups compared to state-of-the-art sequential SAT solvers."

Date: 19-Feb-2010 Title: Pragmatics of SAT, a workshop of the SAT conference within the Federated Logic Conference (FLoC) - July 10, 2010 - Edinburgh, Scotland, UK Hits: 276 Contributed by: Daniel Le Berre Keywords: Structure of problems, Benchmark, SAT application, SAT tools, branching heuristics, Dynamic restarts, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, symmetry, General Interest, Boolean functions, SAT-Based, Linear Constraints, Stochastic Satisfiability, SAT-Solver Competition, Satisfiability Modulo Theory, bioinformatics, SAT-solver, Hybrid solver, Pseudo-Boolean Solving, null, null, null, null, null         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

Date: 04-Feb-2010 Title: Parallel Satisfiability Solving: SAT and beyond SAT, Parallel Solving on New Architectures Hits: 254 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-Nov-2009 Title: Parallel Satisfiability Solving: SAT and beyond SAT, Parallel Solving on New Architectures Hits: 316 Contributed by: Daniel Le Berre Keywords: Alternative approach, Distributed Computing, distributed parallel dynamic learning         ==================================================================== 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 ==================================================================== 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, Université de Reims Champagne-Ardennes, France Email: michael.krajecki@univ-reims.fr Lakhdar Sais, CRIL, Université d'Artois, France Email: sais@cril.univ-artois.fr Gilles Dequen, MIS, Université de Picardie, France Email: gilles.dequen@u-picardie.fr For more details, see the official CFP.

Date: 21-Jun-2009 Title: MSR PhD Scholarship on Parallel SAT Solving Hits: 400 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, null         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

Date: 05-Jun-2009 Title: JSAT special issue on // SAT solving available! Hits: 482 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, SAT-solver, null         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.

Date: 14-Mar-2009 Title: MSR PhD Scholarship on Parallel SAT Solving Hits: 507 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, New research position, SAT-solver         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 Saïs, CRIL, Lens, France Dr. Youssef Hamadi, Microsoft Research, Cambridge, UK Application : please send : CV, motivation letter, recommendation letters to : sais@cril.fr

Date: 01-Mar-2009 Title: CFP: Workshop on Parallel Satisfiability Solving: SAT and beyond SAT, Parallel Solving on New Architectures (WPSS’09) Hits: 515 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, null         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

Date: 04-Feb-2009 Title: LION 3 Tutorial: From SAT to Parallel SAT Solving, Youssef Hamadi, Microsoft Research Cambridge, UK Hits: 551 Contributed by: Daniel Le Berre Keywords: DPLL, SAT tools, Distributed Computing, distributed parallel dynamic learning, null         The Learning and Intelligent OptimizatioN (LION 3) conference was held on Jan 14-18, 2009, in Trento, Italy. Many of the presentations given there are available in pdf from the LION 3 web page. Youssef Hamadi gave a tutorial about // SAT solving, including a review of existing approaches for // SAT solving and a description of the internals of the SAT Race 2008 winner in the parallel track, ManySAT.

Date: 16-Sep-2008 Title: CFP: JSAT Special Issue on Parallel SAT Solving Hits: 713 Contributed by: Youssef Hamadi Keywords: Distributed Computing, message-passing algorithm, distributed parallel dynamic learning, call for papers, null         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.

Date: 29-Apr-2008 Title: Search in ManyCore 1.0 Hits: 689 Contributed by: Daniel Le Berre Keywords: Alternative approach, Distributed Computing, distributed parallel dynamic learning         In conjunction with, International Conference on Principles and Practice of Constraint Programming (CP'08), International Conference on Automated Planning and Scheduling (ICAPS'08), International Conference on Knowledge Representation and Reasoning(KR'08), 12th International Workshop on Non-monotonic Reasoning (NMR'08) . September 15, 2008. Sydney, Australia. Organizers Youssef Hamadi and Pascal Van Hentenryck. Workshop description 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. The previous technological shift represents an important challenge for many computer sciences fields whose best algorithms have to be rethought for manycore-based parallelization. The goal of this workshop is to provide a forum which will consider the consequences of the previous shift for constraint-based combinatorial search. The scope is not restricted to constraint programming or constraint satisfaction, and the organizers would particularly welcome contributions related to Automated Planning or to any other related domain. In order to encourage the systematic and principled exploration of manycore based parallel search, this event will welcome works on all the aspects of parallel search. Typical topics include, but are not restricted to: · Parallel search · Hybrid parallel search · Knowledge sharing in search · Determinism in parallel search Attendance At least one author of each accepted submission must attend the workshop. Presentation and submission format Half-day workshop. Full papers of no more than 15 pages formatted using the LNCS style, http://www.springer.de/comp/lncs/authors.html. Short papers (at least 3 pages or 3,000 words) addressing an important problem for further research or describing an interesting lesson learned. Papers must be addressed in pdf to youssefh at microsoft dot com. Important dates Submission deadline: June 23th Notification of acceptance: July 28th Camera-ready copy deadline: August 4th Workshop: September 15th Program committee · Tanj Bennett, Microsoft, Redmond, USA · Youssef Hamadi, Microsoft Research , Cambridge, UK · Pascal Van Hentenryck, Brown University, Brown, USA · Simon Kasif, Boston University, Boston, USA · Richard Korf, UCLA, Los Angeles, USA · Vipin Kumar, University of Minnesota, Minneapolis, USA · Bertrand Mazure, CRIL-CNRS, Lens, France · Yehuda Naveh, IBM Research, Haifa, Israel · Lakhdar Sais, CRIL-CNRS, Lens, France · Tobias Schubert, Albert-Ludwigs-University of Freiburg, Freiburg, Germany Contact information Youssef Hamadi. Email: youssefh at microsoft dot com

Date: 26-Nov-2006 Title: Special issue of JSAT on CFV Hits: 2112 Contributed by: Miroslav Velev Keywords: Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, MAC, FC, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, QBF, Dynamic restarts, resolution complexity, message-passing algorithm, Linear Programming, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, Preprocessing, Unit Propagation, symmetry, General Interest, Cellular Automata, Cellection Framework, call for papers, semidefinite programming, conference information, Genetic Algorithm, Boolean functions, SAT-Based, Linear Constraints, SAT Hardware, Lookahead, Generative SAT library, multi-value, Stochastic Satisfiability, Divide-and-Conquer Algorithms, Non-monotonic reasoning, implicativity, stable set of points, stable set of clusters, Satisfiability Modulo Theory, Constraint Programming, genetic programming, SAT/CP, bioinformatics, resolution determinization, SAT-solver, SAT/CP Integration, Hybrid solver, Visualisation, Pseudo-Boolean Solving, Resolution proof         Dear Colleague, We would like to invite you to submit a paper to the special issue of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT) on the topic of application of constraints to formal verification (CFV). The submission deadline is January 10, 2007. Topics include, but are not limited to, the following: - application of constraint solvers to hardware verification; - application of constraint solvers to software verification; - dedicated solvers for formal verification problems; - tuning SAT for formal verification and testing; - challenging formal verification problems. The submissions have to be in the JSAT format: http://www.isa.ewi.tudelft.nl/Jsat/ and have to be e-mailed to: mvelev@gmail.com If possible, please confirm your intent to submit a paper. We look forward to your submission, Miroslav Velev and Joao Marques-Silva Editors of the special issue of JSAT on CFV

Date: 09-May-2006 Title: Fourth International Workshop on Constraints in Formal Verification (CFV'06) Hits: 1909 Contributed by: Miroslav Velev Keywords: Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, QBF, Dynamic restarts, resolution complexity, message-passing algorithm, Linear Programming, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, Preprocessing, Unit Propagation, symmetry, General Interest, call for papers, Boolean functions, SAT-Based, Linear Constraints, SAT Hardware         Fourth International Workshop on Constraints in Formal Verification. Affiliated with International Joint Conference on Automated Reasoning 2006 Federated Logic Conference, Seattle, U.S.A., August 22, 2006. The main goals of the Constraints in Formal Verification workshop are to bring together researchers from the CSP/SAT and the formal verification communities, to describe new applications of constraint technology to formal verification, to disseminate new challenging problem instances, and to propose new dedicated algorithms for hard formal verification problems. This workshop will be of interest to researchers from academia and industry, working in constraints or in formal verification and interested in the application of constraints in formal verification. The scope of the workshop includes topics related with the application of constraint technology in formal verification, namely: -application of constraint solvers to hardware verification; -application of constraint solvers to software verification; -dedicated solvers for formal verification problems; -challenging formal verification problems. Submissions can include one of the following: -A workshop paper of up to 15 pages in LNCS format; -A short paper of up to 4 pages, in LNCS format, describing an industrial experience. Important Dates: -Paper submission deadline June 5th; -Notification of acceptance July 5th; -Camera-ready version deadline July 20th; -Workshop Date August 22nd.

Date: 24-Sep-2005 Title: ySAT - Parallel Multithreaded Satisfiability Solver: Design and Implementation Hits: 2206 Contributed by: Yulik Feldman Keywords: DPLL, SAT application, SAT tools, Distributed Computing, distributed parallel dynamic learning         This work describes the design and implementation of a highly optimized, multithreaded algorithm for the propositional satisfiability problem. The algorithm is based on the Davis-Logemann-Loveland sequential algorithm, but includes many of the optimization techniques introduced in recent years. The document provides experimental results for the execution of the parallel algorithm on a variety of multiprocessor machines with shared memory architecture. In particular, the overwhelming effect of parallel execution on the performance of processor cache is studied.

Date: 29-Jul-2003 Title: W. Blochinger, C. Sinz, and W. Küchlin. Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing, 29(7):969-994, 2003. Hits: 1719 Contributed by: Wolfgang Blochinger Keywords: DPLL, distributed parallel dynamic learning         We address the parallelization and distributed execution of an algorithm from the area of symbolic computation: propositional satisfiability (SAT) checking with dynamic learning. Our parallel programming models are strict multithreading for the core SAT checking procedure, complemented by mobile agents realizing a distributed dynamic learning process. Individual threads treat dynamically created subproblems, while mobile agents collect and distribute pertinent knowledge obtained during the learning process. The parallel algorithm runs on top of our parallel system platform DOTS (Distributed Object-Oriented Threads System), which provides support for our parallel programming models in highly heterogeneous distributed systems. We present performance measurements evaluating the performance gains by our approach in different application domains with practical significance. (Preprint version available on request)