 |
27 elements available | | | The list of solvers qualified for the SAT Race 2010 is now available.
The result of the SAT Race will be disclosed during the SAT conference, July 11-14 2010, in Edinburgh. |
| |  | |  |
| | |
| | The fifth competition of pseudo-Boolean solvers is organized as a special event of the SAT 2010 conference. Like the previous evaluations and competitions, the goal is to assess the state of the art in the field of pseudo-Boolean solvers.
The 2010 competition is very similar to the 2009 edition, with 2 exceptions:
- non linear objective functions are allowed
- a special track and a new format are dedicated to maximum satisfiability and weighted max-satisfiability on PB constraints
We encourage you to submit solvers and/or benchmarks to the competition by May 9.
All details are available on the competition web site:
http://www.cril.univ-artois.fr/PB10/ |
| | | | |
| | |
|  | |  | | | | | 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
|
| | | | |
| | |
| | | The results of the SAT 2009 competition are now available.
Access to binary and source code of the solvers will be granted in the next few days. |
| | | | |
| | |
| | | | | | | | Date: | 27-Apr-2009 | | Title: | The Second Answer Set Programming Competition
| | Hits: | 443 | | Contributed by: | | |
Both solvers and benchmarks submission for the SAT competition are now open.
Solver submitters are encouraged to register ASAP in order to vote for their preferred
scoring scheme for the competition, or propose their own scoring scheme.
Submission deadline is March 22.
Scoring scheme proposal deadline is March 11.
Preferred scoring scheme vote deadline is March 13 (i.e. before the submission deadline).
Constant vote (if applicable) is March 18.
See the competition web page for details.
[Update] The submission deadline has been postponed to March 22 in order to let the submitters
have all the details of the scoring scheme a few days before the submission.
|
| | | | |
| | |
| | | | | | | | Date: | 03-Mar-2009 | | Title: | Call for Participation: The Second Answer Set Programming Competition
| | Hits: | 499 | | Contributed by: | | | | | | | | | Date: | 04-Feb-2009 | | Title: | The Second Answer Set Programming Competition
| | Hits: | 547 | | Contributed by: | | | | | | | | | 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. |
| | | | |
| | |
| |
The 2009 pseudo-Boolean competition is organized as a special event of the SAT 2009
conference. Like the previous evaluations (PB05, PB06, PB07), the goal is to assess
the state of the art in the field of pseudo-Boolean solvers.
The deadline for submitting benchmarks or solvers is fixed to April 13, 2009.
Other deadlines as well as the evaluation rules are available at
http://www.cril.univ-artois.fr/PB09/
We would particularly appreciate the submission of
- any kind of pseudo-Boolean solvers
- industrial benchmarks
- benchmarks generators
- benchmarks with a wide distribution of their number of clauses,
cardinality constraints and pseudo-Boolean constraints
- benchmarks with non-linear constraints
|
| | | | |
| | |
| |
Special Issue on the 2007 Competitions
Editors: Ewald Speckenmeyer, Chu Min Li, Vasco Manquinho and
Armando Tacchella
Armin Biere.
PicoSAT Essentials.
Volume 4 (2008), pages 75-97.
* Keywords: SAT solver, watched literals, occurrence lists, proof
traces, restarts.
Marijn J.H. Heule and Hans van Maaren.
Parallel SAT Solving using Bit-level Operations.
Volume 4 (2008), pages 99-116.
* Keywords: local search, parallel computing, Boolean Algebra.
Marijn J.H. Heule and Hans van Maaren.
Whose side are you on? Finding solutions in a biased search-tree.
Volume 4 (2008), pages 117-148.
* Keywords: direction heuristics, jumping strategy, look-ahead
SAT solvers.
Duc Nghia Pham, John Thornton, Charles Gretton, and Abdul Sattar.
Combining Adaptive and Dynamic Local Search for Satisfiability.
Volume 4 (2008), pages 149-172.
* Keywords: SAT solver, local search, clause weighting, adaptive
heuristic.
Ivor Spence. tts: A SAT-Solver for Small, Difficult Instances.
Volume 4 (2008), pages 173-190.
* Keywords: SAT-solver, difficult instance, variable ordering,
simulated annealing, clause memoisation.
Knot Pipatsrisawat, Akop Palyan, Mark Chavira, Arthur Choi, and
Adnan Darwiche.
Solving Weighted Max-SAT Problems in a Reduced Search Space:
A Performance Analysis. Volume 4 (2008), pages 191-217.
* Keywords: Max-SAT, constraint relaxation, lower bound computation.
Wanxia Wei, Chu Min Li, and Harry Zhang. A Switching Criterion for
Intensification and Diversification in Local Search for SAT.
Volume 4 (2008), pages 219-237.
* Keywords: SAT, local search, switching criterion, intensification,
diversification, distribution of variable weights.
Federico Heras, Javier Larrosa, Simon de Givry, and Thomas Schiex.
2006 and 2007 Max-SAT Evaluations: Contributed Instances.
Volume 4 (2008), pages 239-250.
* Keywords: Max-SAT problem instances.
|
| | | | |
| | |
| | | | | | | | Date: | 03-Jul-2008 | | Title: | L. Xu, F. Hutter, H. H. Hoos and K. Leyton-Brown (2008) SATzilla: Portfolio-based Algorithm Selection for SAT, JAIR, Volume 32, pages 565-606
| | Hits: | 777 | | Contributed by: | Daniel Le Berre | | Keywords: | Alternative approach, Benchmark, SAT tools, SAT-Solver Competition, SAT-solver, Hybrid solver |
| | | | | | |
| | | It has been widely observed that there is no single "dominant" SAT solver; instead, different solvers perform best on different instances. Rather than following the traditional approach of choosing the best solver for a given class of instances, we advocate making this decision online on a per-instance basis. Building on previous work, we describe SATzilla, an automated approach for constructing per-instance algorithm portfolios for SAT that use so-called empirical hardness models to choose among their constituent solvers. This approach takes as input a distribution of problem instances and a set of component solvers, and constructs a portfolio optimizing a given objective function (such as mean runtime, percent of instances solved, or score in a competition). The excellent performance of SATzilla was independently verified in the 2007 SAT Competition, where our SATzilla07 solvers won three gold, one silver and one bronze medal. In this article, we go well beyond SATzilla07 by making the portfolio construction scalable and completely automated, and improving it by integrating local search solvers as candidate solvers, by predicting performance score instead of runtime, and by using hierarchical hardness models that take into account different types of SAT instances. We demonstrate the effectiveness of these new techniques in extensive experimental results on data sets including instances from the most recent SAT competition. |
| | | | |
| | |
| | |
| | | Carsten Sinz released today the result of the second qualification round of the SAT Race.
As a consequence, 17 solvers are now qualified for the SAT Race sequential track, 6 for the AIG track and 3 for the parallel track.
Final results will be announced during the SAT 2008 conference.
[Update] You can discuss those preliminary results on Gory Details |
| | | | |
| | |
| | | Abstract.
It has been widely observed that there is no “dominant”
SAT solver; instead, different solvers perform best on different instances.
Rather than following the traditional approach of choosing the best
solver for a given class of instances, we advocate making this decision
online on a per-instance basis. Building on previous work, we describe
a per-instance solver portfolio for SAT, SATzilla-07, which uses socalled
empirical hardness models to choose among its constituent solvers.
We leverage new model-building techniques such as censored sampling
and hierarchical hardness models, and demonstrate the effectiveness of
our techniques by building a portfolio of state-of-the-art SAT solvers
and evaluating it on several widely-studied SAT data sets. Overall, we
show that our portfolio significantly outperforms its constituent algorithms
on every data set. Our approach has also proven itself to be
effective in practice: in the 2007 SAT competition, SATzilla-07 won
three gold medals, one silver, and one bronze; it is available online at
http://www.cs.ubc.ca/labs/beta/Projects/SATzilla.
|
| | | | |
| | |
| | | | | | | | Date: | 26-Jun-2007 | | Title: | RSat source code released
| | Hits: | 1142 | | Contributed by: | | | | 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: | 13-Apr-2007 | | Title: | MiniMarch version 1.1 available
| | Hits: | 1407 | | Contributed by: | | | | | | | | | Date: | 13-Apr-2007 | | Title: | MiniMarch version 1.1 available
| | Hits: | 1407 | | Contributed by: | | | Forthcoming:
Special Issue of JSAT on the SAT 2007 Competitions.
Guest Editors: Ewald Speckenmeyer, Chu Min Li, Vasco Manquinho and Armando
Tacchella. |
| | | | |
| | |
| | | | | | | | 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: | 02-Sep-2006 | | Title: | RSat Executables Available
| | Hits: | 1309 | | Contributed by: | | | | 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. |
| | | | |
| | |
| |
First Evaluation of Max-SAT Solvers (MaxSAT-2006)
The First Evaluation of Max-SAT Solvers (MaxSAT-2006) is organized as an affiliated event of
the Ninth International Conference on Theory and Applications of Satisfiability Testing (SAT-2006).
The objective of the evaluation is assessing the state of the art in the field of Max-SAT solvers,
as well as creating a collection of publicly available Max-SAT benchmark instances.
Important dates
Submission of benchmarks April 3rd, 2006
First submission of solvers April 3rd, 2006
Testing and bug fixing April 10th-30th, 2006
Submission of definitive solvers May 5th, 2006
Experimentation May-June-July, 2006
Results of the evaluation August 12th-15th, 2006
Benchmarks and Solvers
In the first evaluation we will focus the attention on exact solvers and unweighted Max-SAT
instances. We plan to allow non-exact solvers and weighted instances in future evaluations.
Benchmark instances should be submitted in DIMACS CNF format, and submitted solvers should be able
to read that format (see the solver requirements). Submissions should be sent by e-mail to
maxsat06@iiia.csic.es.
The benchmarks used in the evaluation will be selected among the instances submitted and will
not be published in advance. Nevertheless, a set of similar benchmark instances will be made
available for testing purposes.
Experimentation
Only one version of the same solver will be accepted. For each instance and solver there will be a
time limit between 15 and 30 minutes, depending on the number of submitted solvers. Assessment of
solvers will be based on the number of successfully solved instances and the time needed to solve
them.
Solvers will run on machines with the following specification:
* Operating System: Rocks Cluster 4.0.0 Linux 2.6.9
* Processor: AMD Opteron 248 Processor, 2 GHz
* Memory: 2 GB
* Cache: 1024 KB
* Compilers: GCC 3.4.3, javac JDK 1.5.0
Organizing Committee
Josep Argelich, University of Lleida, Spain
Chu Min Li, University of Picardie, France
Felip Manya, IIIA-CSIC, Spain
Jordi Planes, University of Lleida, Spain
To reach the organizers, send an e-mail to maxsat06@iiia.csic.es
|
| | | | |
| | |
| | | | | | | | Date: | 04-Mar-2006 | | Title: | JSAT volume 2, special issue on the SAT2005 competition and evaluations is out!
| | Hits: | 1837 | | Contributed by: | Daniel Le Berre | | Keywords: | BMC, DPLL, Intelligent Backtracking, Data structure, Quasigroups, Local Search, Random 3SAT, Complexity, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Satisfiable Problems Generation, SAT tools, branching heuristics, threshold conjecture, phase transition, QBF, pseudo boolean optimization, preprocessors, General Interest, SAT-Solver Competition |
| | | | | | |
| | | The special issue contains papers related to the fourth SAT competition, the third QBF evaluation and the first Pseudo Boolean evaluation. |
| | | | |
| | |
| |
-------------------------------------
Announcement / Call for Participation
***** SAT-Race 2006 *****
(http://www.fmv.jku.at/sat-race-2006)
August 12-15, Seattle, WA, USA
Affiliated with SAT 2006
-------------------------------------
We are pleased to announce a new competitive event for Boolean
SAT Solvers called
SAT-Race 2006
which stands in the tradition of the SAT Competitions and will
take place before and during the SAT 2006 conference held on
August 12-15 as part of the Federated Logic Conference (FLoC)
in Seattle, WA, USA.
Objective
---------
The area of SAT Solving has seen tremendous progress over the
last years. Many problems (e.g. in hardware and software
verification) that seemed to be completely out of reach a decade
ago can now be handled routinely. Besides new algorithms and
better heuristics, refined implementation techniques turned
out to be vital for this success.
To keep up the driving force in improving SAT solvers, we want
to motivate implementors to present their work to a broader
audience and to compare it with that of others.
Design and Organization
-----------------------
Researchers from both academia and industry are invited to
submit their solvers - in either source code or binary format -
to SAT-Race 2006. During SAT-Race all entrants will have to
solve a set of benchmark instances in DIMACS CNF format that
will be drawn randomly from a pool of SAT instances. This pool
will mainly consist of benchmarks from previous SAT Competitions
(Industrial Category), but may be extended with additional
instances of practical relevance. The exact benchmark set will
not be published in advance; a set of similar benchmark instances
will be made available for testing purposes, however.
For each instance and solver there will be a time limit of 15
minutes. We will also organize qualification rounds, where
participation in at least one of them is mandatory to qualify
for the SAT-Race.
Assessment of solvers will be based on the number of
successfully handled instances and the time needed to solve
them.
Details of the modus operandi are published on the web under
http://www.fmv.jku.at/sat-race-2006.
Important Dates
---------------
- March 31, 2006: Deadline for registering solvers.
- April-June 2006: Qualification phase; exact dates of the
qualification rounds will be published on the web.
- June 30, 2006: Deadline for submitting final versions of the
solvers.
- August 15, 2006: Announcement of results on the SAT 2006
conference.
Organizing Committee
--------------------
Chair:
Carsten Sinz (Johannes Kepler University Linz, Austria)
Advisory Panel:
Nina Amla (Cadence Design Systems, USA)
Joao Marques Silva (University of Southampton, UK)
Emmanuel Zarpas (IBM Haifa Research Lab, Israel)
Technical Consultants:
Daniel Le Berre (Universite d'Artois, France)
Laurent Simon (Universite Paris-Sud, France)
|
| | | | |
| | |
© 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
