 |
8 elements available |  | |  | | | | | 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: | 275 | | 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
|
| |  | |  |
| | |
| | |
| | | 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: | 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. |
| | | | |
| | |
| |
