 |
37 elements available | | | Call for papers for CROCS at CP-10, the 3rd International Workshop on Constraint Reasoning and Optimization for Computational Sustainability, to be held on September 6, 2010 in St Andrews, Scotland, in conjunction with the CP-10 conference.
For submission and other details, please see http://www.computational-sustainability.org/crocs-at-cp10 |
| |  | |  |
| | |
| | | CALL FOR PARTICIPATION (feel free to distribute; apologies for multiple copies)
A Workshop on Tractability will take place on July 5-6, 2010 at Microsoft Research, Cambridge, UK.
(visiting us is easy!)
This workshop will bring together distinguished researchers to discuss their viewpoints on the question: What makes some difficult (e.g. NP-hard) problems tractable in practice? It will provide a place for interactions between experts on a variety of approaches to this question, including both theoreticians and practitioners.
The workshop consists of an exciting set of invited talks, and will leave ample space for discussions.
Participation is free of charge and interested students and researchers are welcome to attend. Registration is necessary: please write to "msrcevnt" followed by “at microsoft” and ending with “dot com” to inform us that you wish to attend. Please indicate your:
- Full name
- Company or University
- Country of residence
- Email address
|
| | | | |
| | |
| | The International Conference on Principles and Practice of Constraint Programming is the annual conference on all aspects of computing with constraints, including: theory, algorithms, applications, environments, languages, models and systems.
This year it will be held in St Andrews, Scotland from 6-10th September 2010.
Submission for tutorial and workshop proposals, as well as submission of technical and application papers is currently open. PhD students are invited to apply for the Doctoral Programme.
See the website for details. |
| | | | |
| | |
| |
SymCon'09 First Call for Papers
The Ninth International Workshop on Symmetry and Constraint Satisfaction Problems
To be held at the Fifteenth International Conference on Principles and Practice of Constraint Programming (CP 2009)
Lisbon, Portugal, September 20, 2009
Submission deadline: Monday, 29 June 2009
Notification of acceptance: Friday, 31 July 2009
Camera ready deadline: Friday, 14 August 2009
Workshop: Sunday, 20th September 2009
***For more information, please see the Call for Papers at: http://alexf04.maclisp.org/symcon09.html
Workshop topics include, but are not limited to:
- Symmetry definition: semantic symmetry, syntactic symmetry, constraint symmetry, solution symmetry
- Automatic symmetry detection: static approaches and dynamic approaches
- Global symmetry detection and elimination
- Dynamic symmetry detection and elimination
- Combining symmetry breaking techniques
- Exploiting weak forms of symmetries like "dominance" and "almost-symmetries"
- Case studies of problems that exhibit interesting symmetries
- Application of computational group theory techniques to symmetry breaking
- Heuristics that use information about symmetry to guide search - Elimination and avoidance of symmetry by re-modelling
- Dynamic avoidance of symmetric states during search
- Complexity analysis of symmetry breaking techniques
- Application of CSPs to symmetry and related algebraic problems - Comparing symmetry breaking techniques in constraint
programming with techniques for dealing with symmetry in other search domains
- Symmetry in CNF formulas and OBF formulas
- Symmetry in finite model search in first order logic
- Novel exploitation of symmetry in varied search domains of interest to the CP community
***For more information, please see the Call for Papers at: http://alexf04.maclisp.org/symcon09.html
|
| | | | |
| | |
| |
Last Call for Papers
Bit-Precise Reasoning 2009 (BPR'09)
Second International Workshop
June 26, Grenoble, France,
Affiliated to CAV'09
http://fmv.jku.at/bpr09
Important Dates
8. May Abstract Submission
15. May Paper Submission
22. May Author Notification
12. June Final Version
Chairs
Armin Biere, JKU, Austria
Priyank Kalla, Univ. of Utah, USA
Program Comittee
Nina Amla, Cadence, USA
Domagoj Babic, Consultant, USA
Clark Barrett, New York Univ., USA
Per Bjesse, Synopsys, USA
Jim Grundy, Intel, USA
Michael Hsiao, Virginia Tech, USA
Daniel Kröning, Univ. of Oxford, UK
Leonardo de Moura, Microsoft, USA
Karen Yorav, IBM, Israel
History
The first workshop on Bit-Precise Reasoning (BPR'08) took
place in Princeton in 2008 and was also affiliated to CAV.
Overview
Bit-precise reasoning (BPR) is a new and promising trend in
automated theorem proving. Traditionally, many theorem provers
approximate bit-vector arithmetic by unbounded integers
or even floating-point. Such approximations fail to model
the boundary behavior of bit-vector arithmetic (overflows
and underflows) accurately. In addition, reasoning about
non-linear operators over unbounded integers is particularly
problematic (undecidable). Recent advances in bit-vector
arithmetic decision procedures indicate that BPR could
become a practical method capable of handling both boundary
conditions and nonlinear operators precisely.
Scope
The primary goal of the BPR Workshop is to bring together both
researchers and users of BPR technology and provide them with
a forum for presenting and discussing not only new theoretical
ideas, but also implementation and evaluation techniques that,
due to either their premature state or their experimental
nature, are unlikely to be accepted for publication in larger
conferences.
Submission
We have two types of papers. Original papers, which will
also be part of the formal proceedings, should contain
original research and sufficient detail to asses the
merits of the submission. On the other hand, we also allow
presentation-only papers, that should describe work recently
published or submitted to some other event. We see this as
a way to provide additional access to important developments
that BPR attendees may be unaware of.
Submission can only be accepted in PDF and should be prepared
using LaTeX with LNCS format using standard margins and
fonts. There is a page limit of 12 pages. Please submit your
paper via EasyChair using the link provided at fmv.jku.at/bpr09.
|
| | | | |
| | |
|  | |  | | | | | Date: | 03-Mar-2009 | | Title: | Call for Participation: The Second Answer Set Programming Competition
| | Hits: | 499 | | Contributed by: | | | | FznTini is a general constraint solver purely based on SAT. It solves constraint satisfaction and optimization problems written in FlatZinc (not involving floating point numbers) via Booleanization and calls to the Tinisat SAT solver. It can also print Booleanizations of constraint models in DIMACS CNF, to be solved by independent SAT solvers (convenient way to generate SAT benchmarks). Constraint modeling languages that have translations to FlatZinc, such as MiniZinc, are automatically supported as well. |
| | | | |
| | |
| |
held in conjunction with CP'2008, Sydney, Australia, Sept 14, 2008.
Overview:
Constraint Programming is a very successful paradigm to express combinatoral
problems for which it provides both a representation language and powerful
solving techniques. Modeling uncertainty in data and/or the presence of an
adversary can be done by introducing universally quantified and/or stochastic
variables. They are used to encode possible alternative that have to be all
taken into account to provide a robust solution. Possible applications are
games, robust scheduling, conformant planning or model checking for the discrete
case. For continuous variables, it includes control design, verification of
safety and performance conditions of a system in engineering or determination of
values of design variables compatible with all values of some uncertain physical
data.
The first workshop on Quantification in Constraint Programming has been held in
conjuction with CP'2005 in Sitges, Spain. Since then, there has been an
increasing attention to this topic in the areas of QBF, QCSP and continuous
constraints. The aim of this workshop is to collect papers describing novel and
ongoing works in the field, and to foster discussions and cross-fertilization
between different approaches.
Scope:
This workshop is open to all aspects related to quantification in Constraint
Programming and SAT. The aim of the workshop is to present ongoing work and to
exchange ideas on modeling and solving quantified problems. Topics that may be
addressed in papers for consideration for inclusion in this workshop include,
but are not limited to:
- Search and propagation algorithm
- Modeling issues with quantified languages
- Complexity results
- Quantified global constraints
- Quantified languages design and compilation
- Strategy extraction and representation
- Over-constrained quantified problems, explanations
- First-order constraints
- Quantification in CHR
- Uncertainty handling
- Stochastic constraint programming
- Implementation issues
- Other types of variables, non-backtrackable variables where domain prunings are not undone
on backtracking
- Applications and benchmarks of Quantified Constraints, QBF and Stochastic CSP
Submissions:
The workshop is open to all members of the CP community. Submitted papers can
be up to 15 pages in length, describing work on one or more of the topics
relevant to the workshop. Alternatively, a shorter paper (maximum 5 pages) can
be submitted, presenting a research statement or perspective on topics relevant
to the workshop. All submissions will be reviewed and accepted papers will be
published in the workshop proceedings. At least one author must attend the
workshop. The proceedings will be available electronically on the workshop web
page and in hardcopy at CP 2008.
We encourage authors to submit papers electronically in pdf format. Papers
should be formatted using the Lecture Notes in Computer Science (LNCS) style.
All submissions should include the author's name(s), affiliation, complete
mailing address, and email address. Workshop papers will be published in
workshop notes as well as on the Web.
Please send your submission by email to the workshop organizers,
using the subject line "QiCP'2008 submission": enrico@dist.unige.it, arnaud.lallouet@univ-orleans.fr, rueher@essi.fr
Important Dates:
Paper submission : July 11, 2008
Notification : July 30, 2008
Final version : August 20, 2008
Organizing Committee:
Enrico Giunchiglia, University of Genova, Italy.
Arnaud Lallouet, University of Orléans, France.
Michel Rueher, University of Nice, France.
|
| | | | |
| | |
| | | | | | | | Date: | 29-Apr-2008 | | Title: | SofT'08 - 9th Workshop on Preferences and Soft Constraints
| | Hits: | 954 | | Contributed by: | | | | | | | | | Date: | 14-Apr-2008 | | Title: | CFV'08 --- Fifth International Workshop on Constraints in Formal Verification
| | Hits: | 862 | | Contributed by: | Miroslav Velev | | Keywords: | Verification, EDA, Benchmark, SAT application, Equivalency Reasoning, Satisfiable Problems Generation, SAT tools, CSP, Logic, branching heuristics, call for papers |
| | | |  |  | |
| | | Call for Papers:
CFV'08 --- Fifth International Workshop on Constraints in Formal Verification,
a satellite event of IJCAR'08.
Invited are papers on application of SAT to formal verification and constraint solving.
Abstract submission deadline: May 15.
Paper submission deadline: May 22.
Workshop dates: August 10-11, 2008.
Location: Sydney, Australia. |
| | | | |
| | |
| |
LaSh08 - WORKSHOP ON LOGIC AND SEARCH
Computation of structures from declarative descriptions
Call For Papers
Leuven, Belgium, November 6-7, 2008
http://www.cs.kuleuven.be/~dtai/LaSh08
................................................................
IMPORTANT DATES:
Submission: August 15, 2008
Notification: September 15, 2008
Workshop: November 6-7, 2008
|
| | | | |
| | |
| | | | | | | | Date: | 03-Dec-2007 | | Title: | Call For Participation: SAT Race 2008
| | Hits: | 1337 | | Contributed by: | Daniel Le Berre | | Keywords: | BMC, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Verification, Alternative approach, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, SAT tools, CSP, binary clause reasoning, SAT-solver, null |
| | | | | | |
| |
----------------------------------------------------------------
Announcement / Call for Participation
*************************
***** SAT-Race 2008 *****
*************************
(http://www-sr.informatik.uni-tuebingen.de/sat-race-2008)
May 12-15, Guangzhou, P. R. China
Affiliated with the SAT 2008 conference.
----------------------------------------------------------------
SAT-Race 2008 is a competitive event for solvers of the Boolean
Satisfiability (SAT) problem. It is organized as a satellite event
to the Eleventh International Conference on Theory and Applications
of Satisfiability Testing (SAT'08) and stands in the tradition
of the yearly SAT Competitions that have been held since 2002
and the first SAT-Race held in 2006 in Seattle. In contrast
to the SAT Competitions, the focus of SAT-Race is on industrial
benchmarks only. Moreover, the time to solve each instance is
limited to 15 minutes.
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 2008. 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) and the SAT-Race 2006 pool, 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.
There will also be two special tracks for:
* Parallel SAT Solvers (SMP, Multi-Threaded) and
* Structural SAT Solvers taking And-Inverter-Graphs (AIGs)
as input.
Details of the modus operandi and about the special tracks
are published on the web under
http://www-sr.informatik.uni-tuebingen.de/sat-race-2008.
Important Dates
---------------
- January 15, 2008: Deadline for registering solvers.
- February-March 2008: Qualification phase; exact dates of the
qualification rounds will be published on the web.
- March 31, 2008: Deadline for submitting final versions of
solvers.
- May 12-15, 2008: Announcement of results on the SAT 2008
conference.
Organizing Committee
--------------------
Chair
Carsten Sinz (Universitaet Tuebingen, Germany)
Advisory Panel
Nina Amla (Cadence Design Systems, USA)
Toni Jussila (OneSpin Solutions, Germany)
Daniel Le Berre (Universite d'Artois, France)
Panagiotis Manolios (Georgia Institute of Technology, USA)
Lintao Zhang (Microsoft Research, USA)
|
| | | | |
| | |
| |
Call for Papers
Constraints Journal
Special Issue on Quantified CSPs and QBF
Guest Editors
Enrico Giunchiglia, Universita di Genova, Italy
Kostas Stergiou, University of the Aegean , Greece
Introduction
CSPs and SAT are frameworks that have been successfully used to model and solve a wide variety of
combinatorial problems. However, there are problems from areas such as contingent planning,
adversarial game playing, control design, and model checking that cannot be expressed within these
frameworks. Typically, such problems involve decisions or events that are beyond the control of the
problem solving agent and thus cannot be modelled using standard (existentially quantified)
variables. Quantified CSPs and QBF, which are the extensions of CSPs and SAT that allow for
universally quantified variables, make it possible to model and reason with such problems, as well
as other PSPACE-complete problems that contain “bounded uncertainty”. As a result, these frameworks
have been attracting significant interest in recent years. The main advances have been achieved in
the area of QBF where numerous solvers have been implemented and real problems of considerable size
have been tackled. There is also a significant body of work on quantified numerical constraints,
while recently research works on QCSPs with discrete finite domains have started to emerge. With
this special issue of Constraints, we aim to group together and reflect the state of the art in
these rapidly developing areas of research.
Topics of Interest
This special issue is concerned with all aspects of research in QCSPs and QBF. Topics of interest
include (but are not limited to):
* Solvers for QCSPs or QBF
* Search and propagation techniques
* Quantified numerical constraints
* Complexity results
* Modelling uncertainty using quantified constraints
* Combining/integrating different frameworks and algorithms
* Real-world applications
Paper Submission
Researchers are invited to submit original papers that make a significant contribution to the field
to konsterg@aegean.gr. (Note that the usual on-line submission procedure for the Constraints journal
will not be followed initially for the Special Issue). All submissions should be in .pdf format and
follow Constraints Journal guidelines. Papers of at most 30 journal pages are preferred.
When submitting, please use the subject "Constraints Special Issue Paper Submission" and clearly
specify the e-mail address and phone number of the corresponding author. Receipt of papers will be
acknowledged. Submissions will be reviewed by at least two reviewers. All accepted papers will meet
the usual high-quality standards of the Constraints Journal.
Authors intending to submit should send an expression of interest (including a provisional title,
list of authors and a tentative abstract) to konsterg@aegean.gr by June 1st , 2007 .
Important Dates
Expression of interest: June 1st, 2007
Submission of papers: September 15th, 2007
Notification of acceptance: December 15th, 2007
Final versions of accepted papers: February 15th, 2008
Important Links
* Special issue home page:
http://www.icsd.aegean.gr/lecturers/konsterg/ConstraintsSpecialIssue.html
* Constraints journal home page:
http://ai.uwaterloo.ca/~vanbeek/Constraints/constraints.html
* Guidelines for authors:
http://ai.uwaterloo.ca/~vanbeek/Constraints/Instructions_for_Authors.html
|
| | | | |
| | |
| | | | | | | | Date: | 05-Apr-2007 | | Title: | CFV'07 Call for Papers
| | Hits: | 1496 | | Contributed by: | Miroslav Velev | | Keywords: | Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, Data structure, Local Search, BDD, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Instance simplification, Learning, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, QBF, Dynamic restarts, variable ordering heuristic, preprocessors, call for papers, conference information, Boolean functions, Linear Constraints, SAT Hardware, Satisfiability Modulo Theory, Constraint Programming, SAT/CP |
| | | | | | |
| | | The Fourth Workshop on Constraints in Formal Verification will take place in Bremen, Germany, on July 16, 2007, as a satellite event of CADE-21.
The submission deadline is May 15, 2007:
http://www.miroslav-velev.com/cfv07.html |
| | | | |
| | |
| | | | | | | | 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 |
| | | | |
| | |
| | From the event web page:
In a constraint satisfaction problem, the goal is to find an assignment of values to a given set of variables so that certain specified constraints are satisfied. Constraint satisfaction problems were introduced in the 1970s to model computational problems encountered in picture processing. It was quickly realized, however, that constraint satisfaction gives rise to a powerful general framework in which a wide variety of combinatorial problems can be expressed. As a matter of fact, it has been asserted that "Constraint satisfaction has a unitary theoretical model with myriad practical applications" (A. Mackworth, Foreword to Constraint Processing by Rina Dechter, 2003). Thus, nowadays constraint satisfaction problems (CSPs) are ubiquitous in many different areas of computer science, from artificial intelligence and database systems to circuit design, network optimization, and theory of programming languages. Consequently, it is important to analyze and pinpoint the computational complexity of certain algorithmic tasks related to constraint satisfaction. These include determining if a CSP has a solution (and, if so, finding such a solution), counting the number of solutions of a CSP, enumerating all solutions of a CSP, and finding the biggest number of constraints that can be simultaneously satisfied, if a CSP is unsatisfiable. Complexity-theoretic results about these tasks may have direct impact on, for instance, the design and processing of database query languages, or strategies in data-mining, or the design and implementation of planners.
During the past two decades, an impressive array of diverse techniques from mathematical fields, such as propositional logic, model theory, Boolean function theory, universal algebra and combinatorics, have been used to analyze the computational complexity of algorithmic tasks related to CSPs. Although significant progress has been made on several fronts, some of the central questions remain unsolved so far; perhaps the most prominent of these is to obtain a complete classification of the complexity of CSPs over an arbitrary, but fixed, finite domain. One of the main aims of the Dagstuhl Seminar is to bring together researchers from all areas of activity in constraint satisfaction, so that they can communicate state-of-the-art advances and embark on a systematic interaction that will enhance the synergy between the different areas. This will provide a unique opportunity to focus attention on a number of important research problems in the complexity of constraints, including the following:
- Islands of tractability of uniform CSP [...]
- Complexity classifications for non-uniform CSP [...]
- Quantified Constraint Satisfaction [...]
- Study of complexity classes through the lens of Boolean CSP [...]
|
| | | | |
| | |
| | | | | | | | Date: | 11-Sep-2006 | | Title: | The CP 2006 Workshop on the Integration of SAT and CP techniques proceedings available online
| | Hits: | 1396 | | Contributed by: | Daniel Le Berre | | Keywords: | DPLL, DP, Intelligent Backtracking, Local Search, Random 3SAT, Complexity, MAC, FC, Alternative approach, Structure of problems, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Learning, SAT tools, CSP, branching heuristics, phase transition, binary clause reasoning, Dynamic restarts, pseudo boolean optimization, variable ordering heuristic, preprocessors, Unit Propagation, SAT-Based, Lookahead |
| | | | | | |
| | From the workshop web site:
SAT and CP techniques are two problem solving technologies which share many similarities, and there is considerable interest in cross-fertilising these two areas. The techniques used in SAT (propagation, activity-based heuristics, conflict analysis, restarts...) constitute a very successful combination which makes modern DPLL solvers robust enough to solve large real-life instances without the heavy tuning usually required by CP tools. Whether such techniques can help the CP community develop more robust and easier-to-use tools is an exciting question. One limitation of SAT, on the other hand, is that not all problems are effectively expressed in a Boolean format. This makes CP an appealing candidate for many applications, like software verification, where SAT is traditionally used but more expressive types of constraints would be more natural. The goal of this workshop is to boost the discussions between the SAT and CP communities by encouraging submissions at the border of these two areas.
|
| | | | |
| | |
| | |
| | | | | | | | 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. |
| | | | |
| | |
| | | | | | | | Date: | 09-Dec-2005 | | Title: | Mathematics for Satisfiability, Victor Marek notes on Satisfiability
| | Hits: | 2286 | | Contributed by: | Daniel Le Berre | | Keywords: | Deduction Rules, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Random 3SAT, Complexity, Computational logic, Structure of problems, SAT application, Randomised Algorithms, Learning, CSP, Linear Programming |
| | | | | | |
| | |
| | | A release of SAT4J for Java 5 is now available.
That release follows the participation of SAT4J this year to the Fourth SAT Competition, the First Pseudo Boolean Evaluation and the First CSP competition.
It contains various bugfixes, coding and algorithmic improvements for SAT, true pseudo boolean constraints reasoning using cutting planes and CSP to SAT translators.
SAT4J is an open source library released under the GNU LGPL license, so it can be freely used into both academic and industrial software. |
| | | | |
| | |
| | From the workshop web site:
This workshop can be of interest to researchers working in all aspects of quantification in constraint programming and related areas such as SAT. The workshop's aim is to present a forum for researchers interested in quantification, and coming from diverse backgrounds (e.g. constraint satisfaction, SAT, logic, linear programming), to present results, exchange ideas and discuss future directions. Topics of interest include (but are not limited to):
- complexity results
- problem modelling
- search and propagation algorithms
- combining/integrating different frameworks and algorithms
- benchmark generation and evaluation methodology
- real-world applications of quantified constraints
|
| | | | |
| | |
| | |
| | | The 3rd International Workshop on Constraints in Formal Verification (CFV), associated with the 20th International Conference on Automated Deduction (CADE-20), will be held on July 23, 2005, in Tallinn, Estonia, and has a submission deadline of June 5.
Papers on applying SAT/CSP to formal verification are welcome. |
| | | | |
| | |
| | | | | | | | Date: | 29-Sep-2004 | | Title: | Logic Summer School 2004 The Australian National University
| | Hits: | 2036 | | Contributed by: | | | | Recently, we have added more forced satisfiable instances of Model RB. Now there are 8 groups of SAT benchmarks, ranging from 450 variables (relatively easy to solve) to 1534 variables (appearing very hard to solve based on the experimental results of ours and some other researchers). |
| | | | |
| | |
| | | All benchmarks were generated using the method proposed in the paper entitled "Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances". There are totally 15 satisfiable CNF instances, all of which are expressed in the DIMACS format. |
| | | | |
| | |
| | | The authors present an interesting comparison between pseudo boolean solvers such as OPBDP or PBS,
mixed integer programming (Ilog CPLEX), Weighted CSP and dedicated solvers for solving MAX-SAT. |
| | | | |
| | |
| | | Abstract: This paper analyzes the resolution complexity of two random CSP models, i.e. Model RB/RD for which we can establish the existence of phase transitions and identify the threshold points exactly. By encoding CSPs into CNF formulas, this paper proves that almost all instances of Model RB/RD have no tree-like resolution proofs of less than exponential size. Thus, we not only introduce new families of CNF formulas hard for resolution, which is a central task of Proof-Complexity theory, but also propose a model with both many hard instances and exact phase transitions. Finally, conclusions and future work are presented, as well as a discussion of the main difference between Model RB/RD and some other models with exact phase transitions. |
| | | | |
| | |
| | | This paper introduces a random CSP model, called Model RB,
which is proved to have exact phase transitions from
satisfiability to unsatisfiability. Unlike other models
with hard instances in phase transitions, e.g. 3-SAT, the
phase transition points of Model RB can be determined
exactly. So we know exactly where the hardest instances
in Model RB are located. Also different from other
NP-complete problems with exact phase transitions, e.g.
1-in-k SAT and Hamiltonian Cycle problem, the exact phase
transition points of Model RB are obtained not by the
analysis of algorithms but by the asymptotic analysis of
the first and the second moment of the number of solutions.
In most cases, if a problem has exact phase transitions
obtained by the analysis of algorithms, then it also means
that the problem is easy to solve or easy on average.
Further comments: Recently, I have obtained some theoretical
results about the hardness of Model RB (have not been
organized into papers but will be available soon). By
encoding CSPs into CNF formulas I proved that the CNF
encodings of Model RB are hard for resolution. This means
that Model RB is an interesting model for study because it
not only has exact phase transitions but also can generate
hard problems to solve. Moreover, I proved that for Model RB,
the method of generating formulas in the phase transition
region that are forced to have at least one satisfying
assignment T will not cause a biased sampling towards
formulas with many satisfying assignments around T. This
result indicates that by encoding the CSPs in the phase
transition region of Model RB which are forced to have at
least one satisfying assignment into CNF formulas, we might
get a new method to generate random hard satisfiable SAT
instances. Anyone interested can test this idea
experimentally or do further studies(either experimental or
theoretical) on Model RB. If you have any comments or results
about Model RB, please contact me by kexu@nlsde.buaa.edu.cn. |
| | | | |
| | |
| | | To study the structure of solutions for
random k-SAT and random CSPs, this paper
introduces the concept of average similarity
degree to characterize how solutions are
similar to each other. It is proved that
under certain conditions, as r (i.e. the
ratio of constraints to variables) increases,
the limit of average similarity degree when
the number of variables approaches infinity
exhibits phase transitions at a threshold
point, shifting from a smaller value to a
larger value abruptly. For random k-SAT this
phenomenon will occur when k>4 . It is further
shown that this threshold point is also a
singular point with respect to r in the
asymptotic estimate of the second moment of
the number of solutions. Finally, we discuss
how this work is helpful to understand the
hardness of solving random instances and a
possible application of it to the design of
search algorithms. |
| | | | |
| | |
| | | | | | | | Date: | 13-Mar-2002 | | Title: | SAT papers are invited to the Journal of Universal Computer Science (J.UCS).
| | Hits: | 2637 | | 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 |
| | | | | | |
| | |
| | | solution of the last open quasigroup existence
problem of the spectrum QG2 (i.e. QG2(10)) with
a new model generator "qgs" |
| | | | |
| | |
|
|
|
|
|
|
|
|
|
| |
