3 elements available
|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.|| |
| || |
| || |
|Title:||Pragmatics of SAT, a workshop of the SAT conference within the Federated Logic Conference (FLoC) - July 10, 2010 - Edinburgh, Scotland, UK|
|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,
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.
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
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).
* 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
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
Regular papers provide more space to describe in detail a full system
or application, provide experimental results, etc.
* 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
* Josep Argelich
* Armin Biere
* Youssef Hamadi
* Daniel Le Berre
* Olivier Roussel
* Carsten Sinz
* Armando Tacchella
* Allen Van Gelder
| || |
|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.|| |
| || |
© 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 firstname.lastname@example.org.