Deadline Countdown

Heads up on SAT research

SAT related books

Other SAT related sites

Date: 19-May-2010 Title: Grain-of-Salt, a CNF problem generator for stream ciphers released Hits: 690 Contributed by: Mate Soos Keywords: Satisfiable Problems Generation, SAT tools, null         After longs months of development, this is the first release of the Grain-of-Salt tool that can generate CNFs for any shift register-based stream cipher. Currently, descriptions for ciphers Grain, Trivium, Bivium, HiTag2 and Crypto1 are included. The tool has 22 separate options, some implementing complex algorithms such Karnaugh table minimisation, greedy Monte-Carlo algorithms for best help bit generation, and extended monomial handling. The tool can be used to generate interesting statistics and visualisations if used in conjunction with CryptoMiniSat, but the CNFs work with any CNF-based SAT solver.

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: 1486 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: 21-May-2008 Title: SAT benchmark encoding the key recovery attack of the stream cipher Bivium Hits: 1678 Contributed by: Daniel Le Berre Keywords: Benchmark, SAT application, null, null         SAT solvers can be used to attack cryptographic stream ciphers. In this benchmark, the solution of a cnf file recovers the internal state of the stream cipher "Brivium" - a reduced version of the eSTREAM cipher "Trivium". The benchmark contains instances of varying complexity (this is achieved by guessing more or less variable assignments). The benchmark provides 300 instances of each difficulty and each with the SAT and UNSAT case.