 |
7 elements available |  | |  | | | | | Date: | 03-Feb-2012 | | Title: | SMT Workshop 2012
| | Hits: | 228 | | Contributed by: | Roberto Bruttomesso | | Keywords: | Satisfiability Modulo Theory, SAT/CP Integration, null, null, null, null, null, null, null, null, null, null |
| | | |  |  | |
| |
======================================================================
SMT Workshop 2012
10th International Workshop on Satisfiability Modulo Theories
Affiliated with IJCAR’2012, Manchester, UK
June 30th - July 1st, 2012
Collocated with The Alan Turing Centenary Conference
http://smt2012.loria.fr
---CALL FOR PAPERS---
======================================================================
Background
----------
Determining the satisfiability of first-order formulas modulo
background theories, known as the Satisfiability Modulo Theories (SMT)
problem, has proved to be an enabling technology for verification,
synthesis, test generation, compiler optimization, scheduling, and
other areas. The success of SMT techniques depends on the development
of both domain-specific decision procedures for each background theory
(e.g., linear arithmetic, the theory of arrays, or the theory of
bit-vectors) and combination methods that allow one to obtain more
versatile SMT tools, usually leveraging Boolean satisfiability (SAT)
solvers. These ingredients together make SMT techniques well-suited
for use in larger automated reasoning and verification efforts.
Aims and Scope
--------------
The aim of the workshop is to bring together researchers and users of
SMT tools and techniques. Relevant topics include but are not limited to:
* Decision procedures and theories of interest
* Combinations of decision procedures
* Novel implementation techniques
* Benchmarks and evaluation methodologies
* Applications and case studies
* Theoretical results
Papers on pragmatic aspects of implementing and using SMT tools, as well
as novel applications of SMT, are especially encouraged.
Important dates
---------------
* Submission deadline - April 16th, 2012
* Notification - May 7th, 2012
* Camera ready versions due - May 28th, 2012
* Workshop - June 30th and July 1st, 2012
Paper submission and Proceedings
--------------------------------
Three categories of submissions are invited:
* Extended abstracts: given the informal style of the workshop, we
strongly encourage the submission of preliminary reports of work in
progress. They may range in length from very short (a couple of
pages) to the full 10 pages and they will be judged based on the
expected level of interest for the SMT community. They will be
included in the informal proceedings.
* Original papers: contain original research (simultaneous submissions
are not allowed) and sufficient detail to assess the merits and
relevance of the submission. For papers reporting experimental
results, authors are strongly encouraged to make their data
available.
* Presentation-only papers: describe work recently published or
submitted and will not be included in the proceedings. We see this
as a way to provide additional access to important developments that
SMT Workshop attendees may be unaware of.
Papers in all three categories will be peer-reviewed. Papers should
not exceed 10 pages (Postscript or PDF) and should be in
standard-conforming Postscript or PDF. Technical details may be
included in an appendix to be read at the reviewers' discretion.
Final versions should be prepared in LaTeX using the easychair.cls
class file.
To submit a paper, go to the EasyChair SMT page
http://www.easychair.org/conferences/?conf=smt2012 and follow the
instructions there.
|
| |  | |  |
| | |
| | | These are benchmarks used in [1,2] for analyzing algorithms for high-level minimal unsatisfiable core (MUC) extraction. High-level MUC extraction is an extraction of MUCs in terms of “interesting” propositional constraints supplied by the user application (e.g., the user may want to find MUCs in terms of latches or assumptions only). High-level MUC extraction is very much relevant to real-world applications of MUC extraction [1,2].
The benchmarks were generated by Intel’s abstraction refinement flow, where each high-level constraint represents a latch. Please reference [1] in publications that use these benchmarks.
[1] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction". In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010, Lugano, October 20-23), 2010.
[2] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction: Paper Addendum". http://www.cs.tau.ac.il/research/alexander.nadel/Addendum_to_Boosting_Minimal_Unsatisfiable_Core_Extraction_final.pdf. |
| | | | |
| | |
| | | | | | | | 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: | 1488 | | 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: | 15-Dec-2009 | | Title: | Alexander Nadel, August 2009, “Understanding and Improving a Modern SAT Solver”. PhD thesis, Tel Aviv University.
| | Hits: | 905 | | Contributed by: | Nadel Alexander | | Keywords: | DPLL, Intelligent Backtracking, Learning, branching heuristics, variable ordering heuristic, Resolution proof, null, null, null, null |
| | | | | | |
| | | This work proposes a new framework for understanding a modern SAT solver as well as a number of empirically useful enhancements.
We start with providing a version of the basic backtracking algorithm that explicitly shows the process of resolution refutation construction. Our approach is based on the notion of a parent resolution derivation – a resolution proof for validness of a flip operation. We show how to derive the algorithm of a modern SAT solver from basic backtracking step-by-step.
This resolution-based approach allows us to define new criteria for measuring the practical impact of different schemes for conflict-driven learning by making the notion of search pruning more formal. We show that the 1UIP scheme, enhanced by conflict clause minimization, is better than other known schemes in terms of search pruning. This explains its empirical advantage over other schemes.
We propose an enhancement to the minimized 1UIP scheme, called local conflict clause recording. This technique improves the performance of a modern SAT solver by recording additional conflict clauses. Local conflict clause recording makes the learning less dependent on the variable polarity selection heuristic.
Assignment stack shrinking is a technique whose goal is to shrink the size of the assignment stack and conflict clauses. We demonstrate the empirical usefulness of assignment stack shrinking and analyze its impact on the performance of a modern SAT solver, comparing it to the impact of conflict clause minimization and rapid restarts.
Furthermore, a new practically useful decision heuristic for SAT, called the clause-based heuristic (CBH), is introduced. This heuristic is designed to increase the likelihood that interrelated variables will be chosen in proximity. It maintains a clause list containing both the initial and conflict clauses. The next decision literal is picked from the first unsatisfied clause. We propose various methods for initially organizing the clause list and for moving clauses within it.
Finally, we present an algorithm for minimal unsatisfiable core extraction that is able to find a minimal unsatisfiable core for large real-world formulas. Our method manipulates the resolution refutation, generated by a modern SAT solver, so that in the end all the input clauses, connected to the empty clause, comprise the minimal unsatisfiable core. |
| | | | |
| | |
| | |
| | | The MiniUnsat Minimal Unsatisfiable Subset (MUS) finder software is now available trough the link above.
It implements the algorithm presented at SAT2008 in the paper "Finding Guaranteed MUSes fast" by Hans van Maaren and Siert Wieringa. |
| | | | |
| | |
| |
