 |
24 elements available | | An article on "Parallel SAT Solving on Peer-to-Peer Desktop Grids" has been published in the Journal of Grid Computing (Springer).
Abstract
"Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domain-specific problems inherent to one of the most challenging environments for parallel computing - Peer-to-Peer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as well as non-uniform communication costs. This is achieved through a sophisticated distributed task pool execution model, problem size reduction through multi-stage SAT formula preprocessing, context-aware memory management, and adaptive topology-aware distributed dynamic learning. Despite the demanding conditions prevailing in Desktop Grids, Satciety achieves considerable speedups compared to state-of-the-art sequential SAT solvers." |
| |  | |  |
| | |
| |
====================================================================
SECOND CALL FOR PAPER
====================================================================
Call for papers
WPSS'2010
A workshop on
Parallel Satisfiability Solving:
SAT and beyond SAT,
Parallel Solving on New Architectures
as part of the HPCS'10 Conference
Le CENTRE DE CONGRES de CAEN
Caen, Normandy, France
June 28 -- July 2, 2010
http://cisedu.us/cis/hpcs/10/main/callForPapers.jsp
====================================================================
Submission Deadline: February 15, 2010
SCOPE AND OBJECTIVES
During the last decade, the fundamental Satisfiability Problem (SAT) has been extensively studied.
This interest of the community significantly grows because of its conceptual simplicity and its
ability to describe a wide set of various problems, including hardware verification, planning,
automated reasoning, and others. Consequently, there is an increasing demand for high performance
SAT-solving algorithms in industry. To date, the parallel SAT solving remains a challenging
problem. In spite of the actual trend in processor development, which is moving from single-core to
multi-core CPU, there exist few parallel solving works dedicated to the SAT problem. This workshop
will focus on SAT and beyond SAT solving techniques exploiting parallelism within a context of High
Performance Computing including massively parallel architectures such as Global Processing Units
(GPUs) and Field-Programmable Gate Arrays (FPGAs).
We invite papers in this emerging discipline which includes, but not limited to, the following areas
of interest.
- High Performance Computing for SAT, Max-SAT #SAT and QBF solving.
- General-Purpose Computation on GPUs (GPGPU) for SAT*
- Reconfigurable Computing and FPGA for SAT*
- Parallel SAT* Pre-processing
- Portfolios and/or Hybridized Algorithms within a Parallel Context
IMPORTANT DATES
Paper Submissions: ------------------------------------------- February 15, 2010
Acceptance Notification: ------------------------------------- March 15, 2010
Camera Ready Papers and Registration Due: -------------------- April 15, 2010
WORKSHOP ORGANIZERS
Michael Krajecki, CReSTIC, Universite de Reims Champagne-Ardennes, France
Email: michael.krajecki@univ-reims.fr
Lakhdar Sais, CRIL, Universite d'Artois, France
Email: sais@cril.univ-artois.fr
Gilles Dequen, MIS, Universite de Picardie, France
Email: gilles.dequen@u-picardie.fr
International Program Committee:
All submitted papers will be reviewed by the workshop technical program committee members following
similar criteria used in HPCS.
- Francois Bodin, IRISA, Rennes, France
- Clementin Tayou Djamegni, University of Dschang, Cameroon
- Youssef Hamadi, Microsoft Research Cambridge, U.K.
- Marijn Heule, TU Delft, The Netherlands
- Bertrand Le Cun, Universite de Versailles Saint-Quentin en Yvelines, France
- Tobias Schubert, Albert-Ludwigs-University of Freiburg, Germany
- Carsten Sinz, University of Karlsruhe, Germany
- Peter Stuckey, University of Melbourne, Australia
If you have any questions about paper submission or the workshop, please contact the Workshop
organizers at the above addresses.
|
| | | | |
| | |
| |
====================================================================
Call for papers
WPSS'2010
A workshop on
Parallel Satisfiability Solving:
SAT and beyond SAT,
Parallel Solving on New Architectures
as part of the HPCS'10 Conference
Le CENTRE DE CONGRES de CAEN
Caen, Normandy, France
June 28 -- July 2, 2010
====================================================================
SCOPE AND OBJECTIVES
During the last decade, the fundamental Satisfiability Problem (SAT) has been extensively studied.
This interest of the community significantly grows because of its conceptual simplicity and its
ability to describe a wide set of various problems, including hardware verification, planning,
automated reasoning, and others. Consequently, there is an increasing demand for high performance
SAT-solving algorithms in industry. To date, the parallel SAT solving remains a challenging
problem. In spite of the actual trend in processor development, which is moving from single-core
to multi-core CPU, there exist few parallel solving works dedicated to the SAT problem. This
workshop will focus on SAT and beyond SAT solving techniques exploiting parallelism within a
context of High Performance Computing including massively parallel architectures such as Global
Processing Units (GPUs) and Field-Programmable Gate Arrays (FPGAs).
We invite papers in this emerging discipline which includes, but not limited to, the following
areas of interest.
- High Performance Computing for SAT, Max-SAT #SAT and QBF solving.
- General-Purpose Computation on GPUs (GPGPU) for SAT*
- Reconfigurable Computing and FPGA for SAT*
- Parallel SAT* Pre-processing
- Portfolios and/or Hybridized Algorithms within a Parallel Context
IMPORTANT DATES
Paper Submissions: ------------------------------------------- February 15, 2010
Acceptance Notification: ------------------------------------- March 15, 2010
Camera Ready Papers and Registration Due: -------------------- April 15, 2010
WORKSHOP ORGANIZERS
Michael Krajecki, CReSTIC, Université de Reims Champagne-Ardennes, France
Email: michael.krajecki@univ-reims.fr
Lakhdar Sais, CRIL, Université d'Artois, France
Email: sais@cril.univ-artois.fr
Gilles Dequen, MIS, Université de Picardie, France
Email: gilles.dequen@u-picardie.fr
For more details, see the official CFP.
|
| | | | |
| | |
| |
Context and scientific objectives: SAT (decide if a Boolean formula, typically in conjunctive
normal form, admits a valuation which makes it true?) is a fundamental problem in complexity
theory with very large practical benefits. Modern SAT solvers can now handle propositional
satisfiability problems with hundreds of thousands of variables or more. However, many practical
instances remain difficult to all the available SAT solvers. Consequently, new approaches are
clearly needed to solve these challenging industrial problems. In this context and with the light
of the next generation of computer architectures, the design of parallel satisfiability solvers
becomes a fundamental issue. The aim of this PhD is to provide new theoretical and practical
advances for parallel satisfiability solving.
Laboratory: CRIL - CNRS UMR 8188, Université d'Artois, Lens, France
Supervision:
Pr. Lakhdar Sais, CRIL, Lens, France
Dr. Youssef Hamadi, Microsoft Research, Cambridge, UK
Application: please send : CV, motivation letter, recommendation letters to : sais@cril.fr
|
| | | | |
| | |
| | | Recent years have shown a major architectural shift in computer hardware. The traditional efficiency gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall and performance improvements have to be found elsewhere. The new direction is to add more computing units (cores) to a chip in order to raise its computational power. The products resulting from this multi-core strategy are now on every desktop and yet the horizon is wide open since the number of cores is expected to grow exponentially. This technological shift represents an important challenge for many computer sciences fields whose best algorithms have to be rethought for multi-core-based parallelization. The goal of this special issue is to officially acknowledge this evolution, and to present recent advanced in the parallel processing of SAT problems. |
| | | | |
| | |
| |
Context and scientific objectives: SAT (decide if a Boolean formula, typically in conjunctive
normal form, admits a valuation which makes it true?) is a fundamental problem in complexity theory
with very large practical benefits. Modern SAT solvers can now handle propositional satisfiability
problems with hundreds of thousands of variables or more. However, many practical instances remain
difficult to all the available SAT solvers. Consequently, new approaches are clearly needed to
solve these challenging industrial problems. In this context and with the light of the next
generation of computer architectures, the design of parallel satisfiability solvers becomes a
fundamental issue.
The aim of this PhD is to provide new theoretical and practical advances for parallel
satisfiability solving.
Laboratory: CRIL - CNRS UMR 8188, Université d'Artois, Lens, France
Supervision:
Pr. Lakhdar Saïs, CRIL, Lens, France
Dr. Youssef Hamadi, Microsoft Research, Cambridge, UK
Application : please send : CV, motivation letter, recommendation letters to : sais@cril.fr
|
| | | | |
| | |
| |
Call for papers
WPSS
A workshop on
Parallel Satisfiability Solving:
SAT and beyond SAT,
Parallel Solving on New Architectures
as part of the HPCS'09 Conference
June 21 - 24, 2009
Leipzig, Germany
Submission Deadline: March 22, 2009
During the last decade, the fundamental Satisfiability Problem (SAT) has been extensively studied.
This interest of the community significantly grows because of its conceptual simplicity and its
ability to describe a wide set of various problems, including hardware verification, planning,
automated reasoning, and others. Consequently, there is an increasing demand for high performance
SAT-solving algorithms in industry. In spite of the actual trend in processor development, which
is moving from single-core to multi-core CPU, there exist few parallel solving approaches dedicated
to SAT problems using shared memory architectures.
This workshop will focus on SAT and beyond SAT solving techniques exploiting parallelism in
emerging massively multi-threaded and multi-core architectures. Recently, Global Processing Units
(GPUs) have evolved to address programming of general-purpose computations. We will particularly
focus on the use of general-purpose GPUs and coprocessor computing techniques to overcome
traditional barriers to parallelization.
We invite papers in this emerging discipline which includes, but not limited to, the following
areas of interest.
- Satisfiability Solving Using Shared Memory
- General-Purpose Computation on GPUs (GPGPU) for SAT
- Reconfigurable Computing and FPGA for SAT
- Parallel SAT, MaxSAT, #SAT and QBF pre-processing
Important Dates:
- Paper Submissions: March 22, 2009
- Acceptance Notification: April 10, 2009
- Camera Ready Papers and Registration Due: April 24, 2009
Workshop Organizers:
- Michael Krajecki, CReSTIC, Univ. de Reims Champagne-Ardennes, France : michael.krajecki@univ-reims.fr
- Lakhdar Sais, CRIL, Univ. d'Artois, France : sais@cril.univ-artois.fr
- Gilles Dequen, MIS, Univ. de Picardie, France : gilles.dequen@u-picardie.fr
Workshop Program Committee:
All submitted papers will be rigorously reviewed by the special session technical program committee members.
- François Bodin, IRISA, Rennes, France
- Youssef Hamadi, Microsoft Research Cambridge, U.K.
- Tobias Schubert, Albert-Ludwigs-University of Freiburg, Germany
- Bertrand Le Cun, Université de Versailles Saint-Quentin en Yvelines, France
- Carsten Sinz, University of Karlsruhe, Germany
|
| | | | |
| | |
| |
Journal on Satisfiability, Boolean Modeling and Computation
ISSN 1574-0617
Special Issue on Parallel SAT Solving
Call for Papers
Deadline for paper submission: November 30th, 2008
Guest Editor
Youssef Hamadi, Microsoft Research youssefh at microsoft dot com.
General Information
Recent years have shown a major architectural shift in computer hardware. The traditional efficiency
gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall
and performance improvements have to be found elsewhere. The new direction is to add more computing
units (cores) to a chip in order to raise its computational power. The products resulting from this
multi-core strategy are now on every desktop and yet the horizon is wide open since the number of
cores is expected to grow exponentially. This technological shift represents an important challenge
for many computer sciences fields whose best algorithms have to be rethought for multi-core-based
parallelization. The goal of this special issue is to officially acknowledge this evolution, and to
present recent advanced in the parallel processing of SAT problems.
Topics
We welcome the submission of works related to the parallel processing (shared-memory and/or
message-passing based) of SAT, MAX-SAT and QBF problems.
Submission
This special issue welcomes original high-quality contributions that have been neither published in
nor submitted to any journals. All submissions should be written in terms understandable by general
readers of the journal. All submissions will be refereed according to JSAT standards, as described
at JSAT web page. Submissions should be written in LaTeX and formatted with JSAT LaTeX style file
according to JSAT's author guidelines, and should not exceed 20 pages. Submissions should be emailed
to youssefh at microsoft dot com within the deadline marked above.
About JSAT
JSAT is a peer-reviewed journal which is freely distributed electronically and published in print by
IOS Press. The scope of JSAT is propositional reasoning, modeling and computation, and related
topics. JSAT publishes high-quality original research papers and survey papers which evidently
contribute to deeper insight on a SAT-related topic.
|
| | | | |
| | |
| |
In conjunction with, International Conference on Principles and Practice of Constraint Programming
(CP'08), International Conference on Automated Planning and Scheduling (ICAPS'08), International
Conference on Knowledge Representation and Reasoning(KR'08), 12th International Workshop on
Non-monotonic Reasoning (NMR'08) .
September 15, 2008. Sydney, Australia.
Organizers
Youssef Hamadi and Pascal Van Hentenryck.
Workshop description
Recent years have shown a major architectural shift in computer hardware. The traditional efficiency
gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall
and performance improvements have to be found elsewhere. The new direction is to add more computing
units (cores) to a chip in order to raise its computational power. The products resulting from this
multi-core strategy are now on every desktop and yet the horizon is wide open since the number of
cores is expected to grow exponentially. The previous technological shift represents an important
challenge for many computer sciences fields whose best algorithms have to be rethought for
manycore-based parallelization. The goal of this workshop is to provide a forum which will consider
the consequences of the previous shift for constraint-based combinatorial search. The scope is not
restricted to constraint programming or constraint satisfaction, and the organizers would
particularly welcome contributions related to Automated Planning or to any other related domain.
In order to encourage the systematic and principled exploration of manycore based parallel search,
this event will welcome works on all the aspects of parallel search. Typical topics include, but are
not restricted to:
· Parallel search
· Hybrid parallel search
· Knowledge sharing in search
· Determinism in parallel search
Attendance
At least one author of each accepted submission must attend the workshop.
Presentation and submission format
Half-day workshop. Full papers of no more than 15 pages formatted using the LNCS style,
http://www.springer.de/comp/lncs/authors.html. Short papers (at least 3 pages or 3,000 words)
addressing an important problem for further research or describing an interesting lesson learned.
Papers must be addressed in pdf to youssefh at microsoft dot com.
Important dates
Submission deadline: June 23th
Notification of acceptance: July 28th
Camera-ready copy deadline: August 4th
Workshop: September 15th
Program committee
· Tanj Bennett, Microsoft, Redmond, USA
· Youssef Hamadi, Microsoft Research , Cambridge, UK
· Pascal Van Hentenryck, Brown University, Brown, USA
· Simon Kasif, Boston University, Boston, USA
· Richard Korf, UCLA, Los Angeles, USA
· Vipin Kumar, University of Minnesota, Minneapolis, USA
· Bertrand Mazure, CRIL-CNRS, Lens, France
· Yehuda Naveh, IBM Research, Haifa, Israel
· Lakhdar Sais, CRIL-CNRS, Lens, France
· Tobias Schubert, Albert-Ludwigs-University of Freiburg, Freiburg, Germany
Contact information
Youssef Hamadi. Email: youssefh at microsoft dot com
|
| | | | |
| | |
|  | |  | | | | | Date: | 05-Apr-2007 | | Title: | CFV'07 Call for Papers
| | Hits: | 1498 | | 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 |
| | | | |
| | |
| | That technical report is a preliminary version of the chapter with the same title appearing in Parallel Combinatorial Optimization , Edited by El-Ghazali Talbi, Wiley-Interscience, October 2006.
Abstract:
The past few years have seen enormous progress in the performance of propositional satisfiability (SAT) solvers, and consequently they are widely used in industry for many applications.
In spite of this progress, there is strong demand for higher SAT algorithms efficiency to solve harder and larger problems. Unfortunately, most modern solvers are sequential and fewer are parallel. Our intention is to review the work of this last decade on parallel resolution of SAT with DPLL solvers which are the most widely used complete ones.
|
| | | | |
| | |
| | | | | | | | Date: | 26-Nov-2006 | | Title: | Special issue of JSAT on CFV
| | Hits: | 2112 | | 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. |
| | | | |
| | |
| | | | | | | | Date: | 04-May-2006 | | Title: | List of papers accepted to SAT06 available!
| | Hits: | 1933 | | Contributed by: | Daniel Le Berre | | Keywords: | Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, Random 3SAT, Complexity, Randomization, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Instance simplification, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, Dynamic restarts, Linear Programming, SAT-Based, Linear Constraints, SAT Hardware, Satisfiability Modulo Theory |
| | | | | | |
| | | Out of 80 submissions the program committee selected 26 regular and 11 short papers. |
| | | | |
| | |
| | | This work describes the design and implementation of a highly optimized, multithreaded algorithm for the propositional satisfiability problem. The algorithm is based on the Davis-Logemann-Loveland sequential algorithm, but includes many of the optimization techniques introduced in recent years. The document provides experimental results for the execution of the parallel algorithm on a variety of multiprocessor machines with shared memory architecture. In particular, the overwhelming effect of parallel execution on the performance of processor cache is studied. |
| | | | |
| | |
| |
************************* URGENT *******************************************
Postdoctoral Position at University of METZ (FRANCE)
* Subject: Parallel Resolution of the Satisfiability Problem
* From: Daniel Singer
* Date: January 2005
Postdoctoral Positions for Research on Parallel Algorithms for Satisfiability Problem
Applications are invited for postdoctoral positions at
the Computer Science Laboratory (LITA), Department of Computer Science
at the University of Metz.
Candidates will perform research on parallel algorithms and develop
programs for the parallel resolution of SAT on different architectures:
clusters, multiprocessors or distributed machines.
Candidates must not be French nationality, must have a PhD in computer science,
mathematics, or a related discipline. Expertise in parallel computing is essential,
and expertise in Satisfiability (DPLL solvers) is highly desirable.
The positions are for a period of one year.
The salary will be 1830 euros/month.
Positions are available immediately. Applications will be accepted
until poistions are filled the latest 15 February 2005.
Interested applicants please contact or submit via e-mail urgently a resume CV, and names of
three references to Daniel SINGER at singer@sciences.univ-metz.fr for further information.
Daniel SINGER
Universite' de Metz
UFR MIM
Ile du Saulcy
F57045 Metz Cedex
FRANCE
tel: +33 (0)3.87.31.52.85
fax: +33 (0)3.87.31.53.09
e-mail: singer@sciences.univ-metz.fr
http://lita.sciences.univ-metz.fr/~singer/
-----------------------------------------------------------------------------
Candidates who are speaking french are encouraged but it is not required.
-----------------------------------------------------------------------------
|
| | | | |
| | |
| | | | | | | | Date: | 07-Aug-2003 | | Title: | WalkSAT-MPI - A Distributed Version of WalkSAT
| | Hits: | 1862 | | Contributed by: | | | | OKgenerator is a generator for random CNF's, based
on the Advanced Encryption Standard (AES), the successor
of DES, as its random source. It is intented to serve
as a standard generator, enabling people to communicate
random formulas by just refering to the parameter values.
OKgenerator is especially designed to generate mixed clause
sizes, and furthermore also generalised CNF's for non-boolean
variables can be generated. Due to its flexible output format
it is possible to use OKgenerator as a random generator for numbers,
bits, or permutations, for example.
I plan to build up a (hopefully) large database for random formulas,
containing information about whether they are satisfiable or not,
and also running times of solvers on them. This database shall be
accessible over the Internet, and I hope to be able to deploy some kind of
"grid" technology, using the computing power of the SAT community.
The package comes with documentation. Included is a report
on the design of OGgenerator, explaining also a research program
for a generic adaptive heuristics for DLL-like SAT solvers, based
on "data mining" of the above database.
Also included is a first tool for automatic generation, processing
and evaluation of experiments (only a very first tool --- more should
follow). |
| | | | |
| | |
| | | | | | | | 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 |
| | | | | | |
| | |
|
|
|
| |
