 |
22 elements available | | | Source code of Lingeling and its multi-threaded front-end Plingeling has been published under GPL. |
| |  | |  |
| | |
| | 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." |
| | | | |
| | |
| | | We are looking to fill a position as university
assistant at either PhD or Post-Doc level.
Deadline for applications is May 12.
Please contact Armin Biere for more information. |
| | | | |
| | |
| | | MTSS (multi-threaded SAT solver) is a SAT solver designed to solve random formulas on multi-cores computers. It also gives the opportunity to parallelize existing SAT solver (even sequential ones under a binary format). The parallelized SAT solver could be designed for random or industrial formulas. In this latter case, MTSS is able to share learnt clauses during the simultaneous executions of the external SAT solver. As an example, we provide a Minisat version which can be executed with MTSS with clauses sharing. The library needed to share clauses is also provided. More informations about this solver and its associated parallel framework can be found at http://www.parallel-sat.net/. |
| | | | |
| | |
|  | |  | | | | | Date: | 11-May-2009 | | Title: | HLDVT 2009: Call for Papers
| | Hits: | 553 | | Contributed by: | Anonymous | | Keywords: | BDD, Random 3SAT, Verification, EDA, Benchmark, SAT application, Equivalency Reasoning, SAT tools, call for papers, SAT-Based, SAT/CP, Hybrid solver, null, null, null, null, null |
| | | |  |  | |
| | | Call for Papers
***************************************************************
HLDVT 2009
IEEE International High-Level Design, Validation and Test Workshop
http://www.hldvt.com/09/
Grand Hyatt, San Francisco, California, November 4-6, 2009
***************************************************************
Please visit http://www.hldvt.com/09/HLDVT09_cfp.pdf |
| | | | |
| | |
| | | | | | | | 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: | | |
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.
|
| | | | |
| | |
| | |
| | The new version of UBCSAT (1.1) is available.
http://www.satlib.org/ubcsat/
UBCSAT is an implementation and experimentation environment for Stochastic
Local Search (SLS) Algorithms for SAT and MAX-SAT.
It includes a large number of SLS algorithms:
http://www.satlib.org/ubcsat/algorithms
This is a fairly significant release, with a lot of new features, including:
* an improved help interface
* new algorithms (Adaptive G2WSAT+p, Novelty++, PAWS, DDFW, VW2)
* several new reports and statistics
see
http://www.satlib.org/ubcsat/revisions.txt for a full list of revisions
Please note that the behaviour of some switches has changed so be careful if you
plan to swap binaries.
If you have any problems, questions, feedback feel free to contact the
author:
Dave Tompkins davet [at] cs.ubc.ca |
| | | | |
| | |
| | | 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 |
| | | | |
| | |
| | | | | | | | Date: | 07-Jan-2008 | | Title: | Practical SAT: A tutorial on applied satisfiability solving, Niklas Een, FMCAD, November 11, 2007
| | Hits: | 1304 | | Contributed by: | Daniel Le Berre | | Keywords: | DPLL, Data structure, Verification, Structure of problems, EDA, SAT application, Instance simplification, Learning, SAT tools, branching heuristics, Dynamic restarts, variable ordering heuristic, General Interest, SAT-Based, SAT-solver, null, null, null |
| | | | | | |
| | From the presentation web page:
The presentation consists of five programs (4 binaries, 1 source code):
* PracticalSAT: Views the slides. Will provide documentation upon run.
* MiniSat_demo: Shows inner workings of MiniSat.
* MiniSat_viz: Visualizes certain key parameters of the SAT run.
* SatELite_demo: Demonstrates CNF preprocessing.
* OptSynth: Source code for a program solving the synthesis problem
discussed in the slides using MiniSat.
A zip file containing all the executables for Linux is available here.
The zip file expands into a directory named PracticalSAT. The directory also
contains additional README files with more information on how to use the three latter programs.
Updated: changed link to minisat page with linux, cygwin and windows binaries.
|
| | | | |
| | |
| |
That paper reports the implementation of a modern SAT solver in 70 lines of OCAML!
Beware: the paper is written in French, but OCAML programmers should be able to grasp the ideas behind the solver.
The SAT solver is embedded in the ERGO SMT solver.
http://ergo.lri.fr/
|
| | | | |
| | |
| | We are pleased to announce of Z3 version 1.1.
Z3 is a new high-performance theorem prover for Satisfiability Modulo
Theories (SMT) problems being developed at Microsoft Research. Z3
supports linear real and integer arithmetic, fixed-size bit-vectors,
extensional arrays, uninterpreted functions, and quantifiers. Z3 has
already been integrated in several projects and products at
Microsoft. It can read problems in SMT-LIB, Simplify and a native
low-level format. Z3 can also be invoked programmatically from either
C/C++, OCaml or from .NET.
More information about Z3, including download links are available from:
http://research.microsoft.com/projects/z3
Kind regards,
Leonardo de Moura and Nikolaj Bjorner.
|
| | | | |
| | |
| | We are pleased to announce the open source availability of the
Decision Procedure Toolkit (DPT). DPT is a modern SMT solver. This
release provides a MiniSAT-like DPLL solver, a DPLL(T) style theory
combination mechanism, and a solver for the theory of Uninterpreted
Functions (EUF). The next release will add a linear arithmetic solver
and a cooperation mechanism for more than one theory.
DPT is an open source project licensed under the Apache 2.0 license.
You can download DPT from sourceforge.
DPT is intended to serve as a platform for experiments in SMT solvers
and their applications. Subsequent releases will include features
like model generation, proof production and interpolants. We also
expect to support parametric theories and the HOL logic.
The DPT design philosophy emphasizes flexible interfaces and
transparent implementation over raw speed. DPT is implemented in
OCaml. These decisions not withstanding, speed is good, and so we
have made a reasonable effort to ensure DPT is fast.
Further announcements about DPT will be made on the dpt-announce mailing
list. You can subscribe to the list via the project web site.
Kind regards,
Amit Goel, Jim Grundy and Sava Krstic |
| | | | |
| | |
| | | Abstract: Solvers for the Boolean satisfiability problem are an important base technology for many applications. The most efficient SAT solvers for industrial applications are based on the DPLL algorithm with clause learning and conflict analysis dependent decision heuristics. The solver MiniSAT v1.14 was modified to use a neural-net-based decision heuristic and search strategy. The weights and biases of the multilayer feedforward neural net are generated by an evolution strategy which is trained on a sample set of SAT problems. Problems solved with the evolved solutions encounter a similar number of conflicts as the original program, but require a higher number of decisions. |
| | | | |
| | |
| | | From the author's web site:
Jat is a solver for Boolean satisfiability implemented in Java. It is a search-based solver which works on CNF input. It is built for SAT-application building and research. As such jat has a strong interest in being efficient, but tries to avoid sacrificing modularity and flexibility when the associated performance hit is more or less negligable for practical applications.
Jat has a rich API including computation of interpolents, enumeration of satisfying minterms, a simple plug-in architecture for adding external (non-propositional) reasoning, proof generation and validation, and several plug-in components for research (learning, variable ordering, etc.).
In terms of performance, jat implements some innovative features including backtrack-aware 2 literal watching, a self-minimizing clause cache, and progress-sensitive restarts.
Jat also has a convenient command line interface which incorporates proof generation, validation, and certificate generation. Jat and its source code are currently available here as part of a sat-based verification toolkit.
|
| | | | |
| | |
| | | The source code of Tinisat, the world's smallest competitive clause learning SAT solver, is now available, along with detailed experimental results. |
| | | | |
| | |
|
|
|
|
|
|
|
|
|
| |
