Deadline Countdown

Heads up on SAT research

SAT related books

Other SAT related sites

Date: 01-Feb-2009 Title: Get ready for the SAT Solver competition 2009! Hits: 569 Contributed by: Daniel Le Berre Keywords: Benchmark, SAT application, SAT tools, branching heuristics, preprocessors, Preprocessing, symmetry, General Interest, SAT-Based, SAT-Solver Competition, SAT-solver         Details about the different special tracks have been updated. Important dates: March, 1st: solver and benchmarks submission opens March, 13th: solver and benchmarks submission closes. Results will be disclosed during the SAT 2009 conference, at Swansea.

Date: 01-Feb-2009 Title: Handbook of Satisfiability, Volume 185 Frontiers in Artificial Intelligence and Applications, Edited by: A. Biere, M. Heule, H. Van Maaren and T. Walsh, February 2009, 980 pp., hardcover ISBN: 978-1-58603-929-5 Hits: 601 Contributed by: Daniel Le Berre Keywords: BMC, DPLL, Intelligent Backtracking, Data structure, Local Search, Random 3SAT, Complexity, Structure of problems, Benchmark, SAT application, Instance simplification, Learning, SAT tools, branching heuristics, phase transition, binary clause reasoning, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, Preprocessing, symmetry, General Interest, SAT-Based, Lookahead, SAT-solver         “Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas. Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field.” Edmund Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award)

Date: 19-Jul-2008 Title: ReVivAl Source Code Available Hits: 836 Contributed by: Cédric Piette Keywords: Instance simplification, SAT tools, Preprocessing         ReViVal is a new preprocessing technique developped by Cédric Piette, Youssef Hamadi and Lakhdar Saïs. ReVivAl is going to be presented in a few days at ECAI'08. The source code of version v0.16 is now available at http://www.cril.fr/~piette/revival The main idea of this preprocessing is to perform particular forms of resolution (through Unit Propagation) for efficiently producing sub-clauses. It can also use different schemes of learning to add relevant clauses. The vivification algorithm ReViVal is based on is designed to be fully integrated within a SAT solver, taking advantage of most recent techniques and data structures implemented for SAT. The proposed implementation of ReVivAl is based on Minisat.

Date: 21-Jun-2007 Title: New place to discuss about the design of SAT solvers: SAT Gory details Hits: 1271 Contributed by: Daniel Le Berre Keywords: Data structure, SAT tools, programming language, Preprocessing, Unit Propagation, SAT-Based, SAT-Solver Competition, SAT-solver         That web site is dedicated to SAT solvers designers willing to share the details of their SAT solvers. It is the expected place to discuss data structures, platform specific tuning, heuristics, etc. It is also the place to comment the source code of the SAT solvers that participated to the SAT competition. Only registered users can post a comment or launch a new thread. Please contact daniel at satlive dot org to register to that site.

Date: 26-Nov-2006 Title: Special issue of JSAT on CFV Hits: 2111 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: 12-Oct-2006 Title: SAT 2007 Call For Paper: deadline for submission is January 19, 2007 Hits: 1529 Contributed by: Daniel Le Berre Keywords: Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, Data structure, Quasigroups, Local Search, Random 3SAT, Complexity, Randomization, Verification, Alternative approach, QBF, Structure of problems, Benchmark, SAT application, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, SAT tools, branching heuristics, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, Preprocessing, Unit Propagation, symmetry, General Interest, call for papers, SAT-Based, Lookahead, Stochastic Satisfiability, SAT-Solver Competition, SAT/CP         SAT 2007 Call for Papers 10th International Conference on Theory and Applications of Satisfiability Testing May 28 - 31, Lisbon, Portugal http://sat07.ecs.soton.ac.uk The International Conference on Theory and Applications of Satisfiability Testing is the primary annual meeting for researchers studying the propositional satisfiability problem (SAT). SAT'07 is the tenth SAT conference. SAT'07 features the SAT competition, the QBF competition, the Pseudo-Boolean evaluation, and the MAX-SAT evaluation. SCOPE Many hard combinatorial problems can be encoded into SAT. Therefore improvements on heuristics on the practical, as well as theoretical insights into SAT apply to a large range of real-world problems. More specifically, many important practical verification problems can be rephrased as SAT problems. This applies to verification problems in hardware and software. Thus SAT is becoming one of the most important core technologies to verify secure and dependable systems. The topics of the conference span practical and theoretical research on SAT and its applications and include but are not limited to proof systems, proof complexity, search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, simplifiers, tools, case studies and empirical results. SAT is interpreted in a rather broad sense: besides propositional satisfiability, it includes the domain of quantified boolean formulae (QBF), constraints programming techniques (CSP) for word-level problems and their propositional encoding and particularly satisfiability modulo theories (SMT). SUBMISSION Submissions should contain original material and can either be regular research papers up to 14 pages or short papers up to 6 pages. Double submissions including submissions as short and long papers will be rejected. Submissions should use the Springer LNCS style. All appendices, tables, figures and the bibliography must fit into the page limit. Submissions deviating from these requirements may be rejected without review. All accepted papers including short papers will be published in the proceedings of the conference. The conference proceedings will be published within Springer LNCS series. The submission page is http://www.easychair.org/SAT2007. Papers have to be submitted electronically as PDF files. Paper submissions are due by January 19. PROGRAM CHAIRS Joao Marques-Silva, University of Southampton, UK Karem Sakallah, University of Michigan, USA LOCAL CHAIR Ines Lynce, Technical University of Lisbon, Portugal IMPORTANT DATES January 19, Paper Submission March 2, Author Notification March 16, Final Version More information on the conference web site.

Date: 22-Aug-2006 Title: SAT Race 2006 results available! Hits: 1326 Contributed by: Daniel Le Berre Keywords: SAT application, SAT tools, Preprocessing, SAT-Solver Competition, SAT-solver         The outcome of the SAT Race 2006 was announced during SAT 2006 last week. The detailed results, the description of the solvers, and additional information are available from the SAT Race's web site.

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: 02-Aug-2005 Title: SAT 2005 Competition detailed results Hits: 2559 Contributed by: Daniel Le Berre Keywords: BMC, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Repository, Random 3SAT, Randomization, Verification, Structure of problems, EDA, Benchmark, SAT application, Randomised Algorithms, Instance simplification, Learning, SAT tools, branching heuristics, Dynamic restarts, Preprocessing, Unit Propagation         All the data concerning the SAT 2005 competition is now publicly available (including benchmarks access). Watch out the competition blog for new additions on that web site.

Date: 08-Jul-2005 Title: MiniSAT and SatELite source code available! Hits: 2734 Contributed by: Daniel Le Berre Keywords: BMC, DPLL, Intelligent Backtracking, Data structure, Verification, EDA, SAT application, Instance simplification, SAT tools, pseudo boolean optimization, preprocessors, Preprocessing         From the authors, Niklas Eén and Niklas Sörenson: On the page you will find binaries, sources, documentation and projects related to MiniSat, including the Pseudo-boolean solver MiniSat+ and the CNF minimizer/preprocessor SatELite. Together with SatELite, MiniSat recently won the three industrial categories of the SAT 2005 competition with a reassuring marginal to the other solvers.

Date: 03-Mar-2005 Title: HaifaSat1.0 released Hits: 2293 Contributed by: Roman Gershman Keywords: BMC, DPLL, SAT application, Instance simplification, branching heuristics, binary clause reasoning, variable ordering heuristic, Preprocessing         HaifaSat is a Chaff-like SAT solver featuring a novel decision heuristic (CMTF), a new resolution-based score system (RBS), an advanced resolution scheme, clause minimization and effective preprocessing using a Hyper-Resolution rule. For more details, refer to this short description. HaifaSat was developed in Haifa/Technion by Roman Gershman under the supervision of Dr. Ofer Strichman.

Date: 04-Aug-2004 Title: quantor-2004.01.25 Hits: 2213 Contributed by:       Date: 31-Dec-2003 Title: Revised Version of "Effective Preprocessing with Hyper-Resolution and Equality Reduction" Hits: 2231 Contributed by: Fahiem Bacchus Keywords: DPLL, Equivalency Reasoning, Instance simplification, binary clause reasoning, Preprocessing         A revised version of "Effective Preprocessing with Hyper-Resolution and Equality Reduction", by F. Bachus and J. Winter is now on-line. This version will appear in the LNCS volume containing revised papers from SAT-2003. The revised version contains a more complete description of the algorithms used in the hypre preprocessor. Sample empirical results from the paper BMC2-b6 (from the SAT2002 competition): 2cls+eq: 11,193 sec. Zchaff: >20,000 sec. Berkmin (5.61) 3,426 sec. hypre solves in 214 sec. IBM-Hard (3 problems) Berkmin (5.61) 38,997 sec. failing to solve 1 problem Zchaff 47,581 sec. failing to solve 2 problems failures charged 20,000 sec. With hypre hypre takes 1,767 sec. preprocessing time Berkmin takes 3,560 sec. to solve preprocessed problems (no failures) Zchaff takes 28,920 sec. to solve preprocessed problems (no failures)             Date: 19-Nov-2003 Title: Converting the negation of a CNF to another CNF Hits: 2196 Contributed by: Anonymous Keywords: Alternative approach, Preprocessing         I just wrote about an idea on how to convert the negation of a CNF to another CNF, over in algorithm-forge. If perhaps someone is interested in a discussion please visit http://groups.yahoo.com/group/algorithm-forge/message/2420 Klaus D. Witzel kwitzel@marzili.com             Date: 07-Sep-2003 Title: Probing-Based Preprocessing Techniques for Propositional Satisfiability, by Ines Lynce and Joao Marques-Silva, 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2003), Nov. 2003 Hits: 1863 Contributed by: Inês Lynce Keywords: Preprocessing, Unit Propagation         Preprocessing is an often used approach for solving hard instances of propositional satisfiability (SAT). Preprocessing can be used for reducing the number of variables and for drastically modifying the set of clauses, either by eliminating irrelevant clauses or by inferring new clauses. Over the years, a large number of formula manipulation techniques has been proposed, that in some situations have allowed solving instances not otherwise solvable with state-of-the-art SAT solvers. This paper proposes probing-based preprocessing, an integrated approach for preprocessing propositional formulas, that for the first time integrates in a single algorithm most of the existing formula manipulation techniques. Moreover, the new unified framework can be used to develop new techniques. Preliminary experimental results illustrate that probing-based preprocessing can be effectively used as a preprocessing tool in state-of-the-art SAT solvers.         © 2000-2001 Business & Technology Research Laboratory. © 2001-2005 Centre de Recherche en Informatique de Lens. Hosted by Innovation and Technology Research Lab. Please send any comment to daniel@satlive.org.