 |
See all Softwares
101 elements available | | | Variant 4 of the siege solver is available. Huge performance improvements over v3. |
| |  | |  |
| | |
| | | Sharad Malik group at princeton university has developed a new SAT solver, Chaff, that seems
to outperform others state-of-the-art SAT solvers by one or two order of magnitude on real world,
structured instances (EDA, VLSI, ...). Chaff is a highly optimized version of the Davis and
Putnam procedure, using conflict analysis, restarts and an interesting notion of learning.
A development snapshot of Chaff is available for download for Solaris and Linux.
A paper explaining how Chaff works and providing experimental results is available as well. |
| | | | |
| | |
| | |
|  | |  | | | | | Date: | 30-Jun-2005 | | Title: | Java package for conversion into SAT problem.
| | Hits: | 4037 | | Contributed by: | Kerry M. Soileau | | Keywords: | Data structure, Computational logic, Alternative approach, Structure of problems, SAT application, Satisfiable Problems Generation, SAT tools, Logic, programming language, General Interest, Boolean functions, Generative SAT library |
| | | |  |  | |
| | | A Java package which compiles a problem into an equivalent SAT problem. |
| | | | |
| | |
| | | | | | | | Date: | 03-May-2003 | | Title: | The opensat project
| | Hits: | 2768 | | Contributed by: | Daniel Le Berre | | Keywords: | DPLL, Intelligent Backtracking, Data structure, Local Search, BDD, QBF, SAT application, Randomised Algorithms, Learning, SAT tools, branching heuristics |
| | | | | | |
| | | OpenSAT is an open source (LGPL) SAT framework in Java.
The OpenSAT reference implementation and an OpenSAT compliant solver (JQuest2)
participated to the SAT2003 competition.
A poster presentation of the OpenSAT project will be made during the SAT2003 conference. |
| | | | |
| | |
| | | | | | | | Date: | 08-Jul-2005 | | Title: | MiniSAT and SatELite source code available!
| | Hits: | 2694 | | Contributed by: | Daniel Le Berre | | Keywords: | BMC, DPLL, Intelligent Backtracking, Data structure, Verification, EDA, SAT application, Instance simplification, SAT tools, pseudo boolean optimization, preprocessors, Preprocessing |
| | | | | | |
| | From the authors, Niklas Eén and Niklas Sörenson:
On the page you will find binaries, sources, documentation and projects
related to MiniSat, including the Pseudo-boolean solver MiniSat+ and the
CNF minimizer/preprocessor SatELite. Together with SatELite, MiniSat
recently won the three industrial categories of the SAT 2005 competition
with a reassuring marginal to the other solvers.
|
| | | | |
| | |
| | | Strife is a SAT/QBF solver using a novel approach that does not require any search. Source code is available for download, as well as detailed explanations of how it works. |
| | | | |
| | |
| | | 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). |
| | | | |
| | |
| | |
| | |
| | From the authors:
NuSMV is a reimplementation and extension of SMV, the first model
checker based on BDDs. It has been designed to be an open architecture
for model checking, which can be reliably used for the verification of
industrial designs, as a core for custom verification tools, and as a
testbed for formal verification techniques.
NuSMV version 2 extends NuSMV with new model checking algorithms and
techniques. It combines classical BDD-based symbolic techniques with
SAT-based techniques. It also presents other new features: for
instance, it allows for a more powerful manipulation of multiple
models; it can generate flat models for the whole language; it
implements new partitioning techniques; it allows for cone of
influence reduction.
The BDD-based model checking component exploits the CUDD library
developed by Fabio Somenzi at Colorado University. The SAT-based model
checking component includes a Bounded Model Checker, connected to the
SIM SAT library developed by the University of Genova.
NuSMV version 2 is distributed with an OpenSource license, namely the
GNU Lesser General Public License (LGPL). The aim is to provide a
publicly available state-of-the-art symbolic model checker. With the
OpenSource development model, a whole community participates in the
development of a software systems, with a distributed team and
independent peer review. This may result in a rapid system evolution,
and in increased software quality and reliability: for instance, the
OpenSource model has boosted the take-up of notable software systems,
such as Linux and Apache. With the NuSMV OpenSource project, we would
like to reach the same goals within the model checking community,
opening the development of NuSMV.
|
| | | | |
| | |
| | | First binary release of the QBF solver QUANTOR. |
| | | | |
| | |
| | | The 2clseq (Two Clause Eq) solver is now available on-line.
The source code is available for non-commercial use, and there is also
a Linux executable that should be fairly portable.
The system is exactly the same as the version that
was entered in the recent SAT2002 competition.
Briefly 2clseq is a DPLL SAT solver that is unlike most other state-of-the-art SAT
solvers. In particular, 2clseq uses extensive reasoning at each node of the DPLL
search tree, and it demonstrates, perhaps for the first time, that extra reasoning
can be effective in terms of final performance. On some types of problems 2clseq performs better
than any other solver I know of. Also worth noting is that 2clseq does quite well on random
problems as well as on more structured "industrial" type problems.
Also on-line are two papers one to appear at AAAI-2002, and one that appeared at
SAT2002, describing the 2clseq approach.
Please contact me if you have any questions of find any problems with the distribution.
Fahiem
fbacchus@cs.toronto.edu |
| | | | |
| | |
| |
The UBCSAT software is availabe for download at:
http://www.satlib.org/ubcsat
-- the software was described in a paper presented at SAT 2004.
UBCSAT is a framework for Stochastic Local Search (SLS) algorithms for SAT. It includes fast implementations of many existing SLS algorithms (WalkSAT, SAPS, Adaptive Novelty+, ...) in a framework designed to facilitate the empirical analysis of SLS algorithms. UBCSAT has been designed to make it easy to add new algorithms and reporting capabilities, and so future releases will include more algorithms and features. Note that UBCSAT also provides support for the weighted MAX-SAT problem.
If you would like to be notified of future releases of UBCSAT, we have set up a mailing list you can subscribe to (details are on the website).
|
| | | | |
| | |
| | | [UPDATE]
Ronen Brafman released a new version of his CNF simplifier (see its IJCAI'01 paper
A Simplifier for Propositional Formulas with Many Binary Clauses ,
for more details).
This release does not need anymore the LEDA library. It uses the STL instead.
BEWARE: that version of 2-Simplify was found buggy (5 june 2002).
This message will be removed when 2-Simplify will be corrected.
|
| | | | |
| | |
| | | Binaries for Windows Cygwin and Linux are available for download. |
| | | | |
| | |
| | | Prophet Engine is a BMC property checking engine, developed by Roman Gershman and based on the paper by [Strichman01]. Prophet does not use any advanced techniques, such as abstraction-refinement or k-induction. Nevertheless, despite being developed with simplicity in mind, Prophet is fast, because it is based on the latest SAT solving technology. In fact, the engine can be used as a good reference point for other, more complicated techniques. |
| | | | |
| | |
| | | | | | | | Date: | 25-Oct-2002 | | Title: | A new release of BerkMin !!
| | Hits: | 2037 | | Contributed by: | | | | An instance simplifier written in C++. It is based on simplification rules on implication graph.
A technical report explaining how it works is included in the archive. |
| | | | |
| | |
| | | | | | | | Date: | 18-Nov-2002 | | Title: | A new SAT solver - Jerusat
| | Hits: | 1995 | | Contributed by: | | | |
| | |
| | | The generalized version "kcnfs" of "cnfs", extending to the solving of
random k-SAT formulae, is available (source code) at :
http://www.laria.u-picardie.fr/~dequen/sat/ |
| | | | |
| | |
| | | The web page contains a boolean circuit input format and software to translate instances in that format into CNF. |
| | | | |
| | |
| | | This tool takes a boolean formula with CMU SMV syntax as input and converts it into CNF (DIMACS format). This is done efficiently, i.e., by adding variables, not by multiplication. |
| | | | |
| | |
| | From the solver's web site:
It is a trimmed version of 2004.5.13 [Note: SAT 2004 competition version]. Many unused or dead codes are removed. Most codes are re-formatted for easy reading. You might get a little speed up as well. If the functionality that you require is removed, please use the original 2004.5.13 version.
|
| | | | |
| | |
| | The first public distribution of the QBF solver sKizzo is now available for download.
sKizzo is a hybrid QBF solver based on propositional skolemization. It mixes q-resolution based reasoning, complete and incomplete symbolic reasoning, SAT-based reasoning, and DPLL-like reasoning. It is part of a suite (not yet available for download) that allows the user to extract unsatisfiable cores, produce witnesses of satisfiability (certificates) for SAT formulas, query such certificates, and more.
The software is distributed in binary format for the PPC/OSX and i386/Linux platforms. Current version is 0.6-beta. A detailed user manual is included. Feedback from users is welcome.
Next steps will be to:
- Distribute the companion application ozziKs to certify the satisfiability of formulas.
- Distribute the C library libQBM to load, manage and query certificates of satisfiability for QBFs.
|
| | | | |
| | |
| | | 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. |
| | | | |
| | |
| | | The latest version of SATO and related papers can be found at this site. |
| | | | |
| | |
| | | The QBF solver Quaffle is now available in source code for immediate download. To our limited knowledge, this is the first QBF solver that is avialable in source code. Quaffle, which is a loose acronym for Quantified Formula Evaluator with Learning, is an experimental QBF solver that incorporates the concept of satisfaction directed implication as well as non-chronological backtracking and learning for both satisfactions and conflicts. The main idea of the solver is described in two papers that are available on the same web page.
The code is in version 0.1. That means it's not a proper example for coding style. It is also not designed for ease of hacking. We welcome comments and bug reports. |
| | | | |
| | |
| | |
| | From the site:
SIM is a library of efficient procedures for propositional satisfiability (SAT) problems.
The current version of SIM (ver. 1beta) allows for:
- 9 branching heuristics: 2JWHeur [HV94], BoehmHeur [BB92], JWHeur [JW90], MomsHeur [Pre93], RndHeur, RelsatHeur, SatoHeur [Zha97],
SatzHeur [LA97], UnitieHeur, and UsrHeur
- chronological backtracking
- backjumping
- relevance and size learning
- pure literal rule, if learning is not used
- Horn relaxation
- the specification of model variables
We are going to implement preprocessing techniques, and to extend pure literal rule to learning.
SIM is used in the following systems:
- NuSMV: a symbolic model checker developed as a joint project between CMU and IRST.
- Thunder-Forecast, a proprietary architecture for model checking developed by Intel Corp.
The source code in C is available from the site. A C++ version can be obtained on demand. |
| | | | |
| | |
| | | | | | | | Date: | 07-Aug-2003 | | Title: | WalkSAT-MPI - A Distributed Version of WalkSAT
| | Hits: | 1839 | | Contributed by: | | | | The march_dl SAT solver is an upgraded version of the successful march_eq SAT solver, which won two categories in the SAT 2004 competition. Its source-code and a description are now available at the SAT@Delft homepage. The main improvements in march_dl are: (1) Additional pre-processing techniques; (2) a more dynamic look-ahead procedure; (3) implementation of a double (second level) lookahead; and (4) increased readability of the source-code. |
| | | | |
| | |
| | | the CNF Solver and the IJCAI-01 paper
"A backbone-search heuristic for efficient solving of hard 3-SAT formulae"
are available |
| | | | |
| | |
| | | Please note that this is Berkmin version 56, whose results
are described in the DATE-2002 paper, not Berkmin 62, the
version that competed in SAT2002 solver competition. |
| | | | |
| | |
| | | This is the first public release of Limmat a satisfiability solver. It
reads a propositional formula in Dimacs format and checks it for
satisfiability. Limmat is inspired by Chaff and Grasp. In addition it
provides a fast conflict detection mechanism in boolean constraint
propagation and compared to Chaff fast access to both watched literals in a
clause. It is implemented in C with handcrafted data structures and
includes a solid test frame work. |
| | | | |
| | |
| | |
| | | Based on the master/slave model for communications and on a dynamic
preemptive workload balancing by work stealing, //Satz can run on any
Linux or Unix machines in a local network. Currently //Satz requires
that all machines in the local network share the same home directory
(using NFS).
Each used machine is a slave, while the master runs on an arbitrary
machine. When one slave becomes idle after finishing its work, it
sends a work request to the master which evaluates the workload of
each busy slaves and sends the first remaining subtree of the most
loaded slave to the idle slave.
When a slave finds a solution (for satisfiable problems) or all slaves
send a work request (for unsatisfiable problems), the master stops the
resolution.
//Satz supports fault-tolerance. Every hours, all slaves send their
current context to the master. If a slave dies, the master sends its
saved context to the idle slave at the time of workload balancing so
that the work of the died slave can be continued. The resolution can
be so stopped and re-started from an interruption point.
The source code of //Satz is available at
http://www.laria.u-picardie.fr/~cli |
| | | | |
| | |
| | | | | | | | Date: | 27-Apr-2003 | | Title: | Jerusat 1.2 executables
| | Hits: | 1643 | | Contributed by: | | | From the web page:
Many SAT instances arising out of real-world problems such as model-checking require hours,
even days, to solve, in the process taking up significant system resources. It would be very
useful to be able to have, at any point, a measure of the progress made on solving the
instance so far. Unfortunately, no such facility currently exists for any of the major SAT
solvers in use. Our progress bar attempts to fix this shortcoming.
In addition to providing a measure of progress towards the solution of a SAT instance, a
progress bar for SAT solvers has another, potentially more important purpose: it can be used
to achieve a better algorithm for solving SAT instances. There are several SAT solvers in use
today; all use slightly different algorithms and heuristics; many also have several heuristics
they can use. Though on average some solvers may outperform others, for any given instance it
is very difficult to predict which solver will provide the optimum result. Moreover, the
difference between the optimum and non-optimum solver can be quite large. If we could have a
reasonably dependable progress bar, we could use it to select the optimum solver by running
several solvers for a short time, choosing the one that made the most progress in that time,
and running it on the whole problem. If the instance is sufficiently large, the overhead of
running several servers for a short time initially is small compared to the savings achieved
by using the optimal algorithm.
A paper describing the progress bar principle is available.
A version of RELSAT 2.0 and the last version of SATO with the progress bar are available as
well.
A standalone version of the progress bar to equip your own SAT solver is also available. |
| | | | |
| | |
| | | This binary package, NIMO, includes the combinational circuit SAT solver Nimo_CSAT, the sequential circuit solver Nimo_SeqSAT, the bounded model checking tool Nimo_BMChecker, the invariant checking tool Nimo_IChecker and the sequential equivalence checking tool Nimo_SEChecker |
| | | | |
| | |
| | | Hypre is a new implementation of the Hyper Binary Resolution + Equality Reduction rule
used in the sat solver 2clseq. It is much faster (sometimes 2 orders of magnitude) than the
hypbin+eq reasoner imbedded in 2clseq, and it can be extremely effective in simplifying
the formula. Reductions of thousands of variables are quite common (on structured problems).
The paper and some results are reported in
this SAT2003 paper
The software is available at the 2clseq
homepage. |
| | | | |
| | |
| | | A gateway to invoke relsat 2.1 (a systematic satisfiability solver & model
counter) using an e-mail request. I you're unwilling or unable to install relsat,
or lack a machine with reasonable CPU power, then you might find this gateway
useful. |
| | | | |
| | |
| | | Satz214 + Detection of implied literals suggested by Daniel Le Berre |
| | | | |
| | |
| | | From the authors web site:
This is the first release of MiniSat 2, featuring variable elimination style simplification natively. It is a cleaned up version of the winning entry of SAT-Race 2006 and is intended to subsume SatELite and SatELiteGTI.
|
| | | | |
| | |
| | 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.
|
| | | | |
| | |
| | | Ttcnf computes all truth tables of CNF boolean expressions with one to five variables. It counts these truth tables in a number of ways. These results may be useful in understanding CNF expressions. |
| | | | |
| | |
| | The QBF solver IQTest, which was discribed in
L. Zhang, "Solving QBF with Combined Conjunctive and Disjunctive Normal Form", Twenty-First National Conference on Artificial Intelligence (AAAI 2006), Boston, MA, July 2006
is available from my homepage, together with some benchmarks used in the paper. |
| | | | |
| | |
| | | First public source release of our BDD based SAT solver EBDDRES, which can also
generate resolution proofs. A trace checker for the proofs produced
by EBDDRES can also be downloaded at http://fmv.jku.at/tracecheck. |
| | | | |
| | |
| | | | | | | | Date: | 13-Apr-2007 | | Title: | MiniMarch version 1.1 available
| | Hits: | 1369 | | Contributed by: | Siert Wieringa | | Keywords: | branching heuristics, preprocessors, symmetry, Lookahead, SAT-Solver Competition, SAT-solver, branching heuristics, preprocessors, symmetry, Lookahead, SAT-Solver Competition, SAT-solver |
| | | | | | |
| | MiniMarch is a modified version of MiniSat v2.0 Beta. The design goal was to make a version of MiniSat that is less sensitive to shuffling of the input formula. MiniMarch's techniques include the application of clause sorting and activity initialization. A lookahead branching direction heuristic is used and MiniSat's simplifying preprocessor has been modified.
The MiniMarch SAT solver was submitted to the SAT Competition 2007 but has unfortunatelly been disqualified due to incorrect answers caused by a bug in the parsing of the input formula.
MiniMarch version 1.1 is what the submitted solver should have been. More information and the source code is now available from SAT @ Delft. |
| | | | |
| | |
| | | Actin (ACTivity INitialization) is a modification of MiniSAT 1.14 that attempts to improve solving times by initializing the activities with values computed from the CNF. The algorithm was evolved with genetic programming (GP). The solver participated in SAT-Race 2006.
I am offering the GP program that evolves the algorithm for download to interested parties. A number of training problems can be given to the program, which will run GP for a number of generations and print out the best individual of each generation. |
| | | | |
| | |
| | |
| | | | | | | | Date: | 05-Jan-2007 | | Title: | SBSAT, a state-based SAT solver
| | Hits: | 1305 | | Contributed by: | Sean Weaver | | Keywords: | BMC, DPLL, Local Search, BDD, SAT tools, preprocessors, Boolean functions, Linear Constraints, SAT-solver, Hybrid solver, Cardinality solving |
| | | | | | |
| | | Information about the state-based SAT solver SBSAT, including a new version w/ source code, can be found here: http://www.cs.uc.edu/~weaversa/SBSAT.html |
| | | | |
| | |
| | | Executables of RSat have been made available.
RSat is a DPLL-based SAT solver that won the third place in the SAT-Race 2006 competition.
For more information, please visit the RSat website at
http://reasoning.cs.ucla.edu/rsat |
| | | | |
| | |
| | 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 |
| | | | |
| | |
| | | A branch and bound solver for Max-SAT that incorporates into a Max-SAT
solver some of the technology developed for Satz (see below). At each node
of the proof tree it transforms the formula into an equivalent formula that
preserves the number of unsatisfied clauses by applying some efficient refinements
of unit resolution that the authors have defined for Max-SAT (e.g., it replaces
$x, y,
eg x vee
eg y$ with $Box, x vee y$, it replaces $x,
eg x vee y,
eg x vee z,
eg y vee
eg z$ with $Box,
eg x vee y vee z,
x vee
eg y vee
eg z$). MaxSatz implements a lower bound computation
method that consists of incrementing the lower bound by one for every disjoint
inconsistent subset that can be detected by unit propagation. Moreover, the lower
bound computation method is enhanced with failed literal detection. The variable
selection heuristics takes into account the number of positive and negative occurrences
in binary and ternary clauses.
Maxsatz and its variants are the best performing solvers in the unweighted maxsat
category in the 2006 maxsat solvers evaluation and the 2007 maxsat solvers evaluation.
References:
Chu Min LI, Felip Manya, Jordi Planes, "New Inference Rules for Max-SAT",
in Journal of Artificial Intelligence Research, October 2007, Volume 30, pages 321-359
Chu Min LI, Felip Manya, Jordi Planes, "Detecting disjoint inconsistent subformulas
for computing lower bounds for Max-SAT". In Proceedings of the 21st National
Conference on Artificial Intel ligence (AAAI-06), Boston, USA, pp. 86–91. AAAI Press. |
| | | | |
| | |
| | | The source code of RSat which participated in the SAT'07 competition
is now available at http://reasoning.cs.ucla.edu/rsat. Included in the
source code is an interface for recursive-style SAT solving which can
also be used to perform exhaustive search for applications such as
model counting and knowledge compilation. |
| | | | |
| | |
| | | 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.
|
| | | | |
| | |
| | | MiraXT is a multithreaded SAT solver that was designed to take advantage of current and future shared memory multiprocessor systems. The experimental results in [2] show that already in single threaded mode, MiraXT compares well to other state-of-the-art SAT algorithms on a wide range of industrial problems. In threaded mode, it provides cutting edge performance, as speedup is obtained on both satisfiable and unsatisfiable instances.
[1] T. Schubert, M. Lewis, N. Kalinnik, and B. Becker. Solver Description of the different configurations of MiraXT, entering the SAT Competition 2007.
[2] M. Lewis, T. Schubert, and B. Becker. Multithreaded SAT Solving. In 12th Asia and South Pacific Design Automation Conference, 2007. |
| | | | |
| | |
| |
Among the new features:
* New SAT solver presented to the SAT Race 2006 including the
expensive reason simplification developed in MiniSAT 1.14
(MiniLearningHeapExpSimp)
* New command line configuration of solvers
* Optional more robust (but less efficient) CNF input (allows to
include comments between constraints): jar -jar sat4j.jar
EZCNF:/my/dimacs/file.cnf
* Basic support for And Inverter Graph format, in both ASCII (aag) and binary (aig)
form.
* Improved and simplified Pseudo Boolean code.
* Fine code tuning provided by Dieter von Holten: 10% speedup in
average.
* Memory management: constraints are removed only when memory is
exhausted.
* Bug fixing in the optimization framework.
* Improved code for the CSP to SAT conversion.
* Improved Javadoc.
* Rapid Restart Strategy, as in RSAT and picosat.
* Improved solvers for pseudo boolean constraints
* Use now Java generics to prevent user to setup a solver with
incompatible components (i.e. a heuristics that needs information
available only from a specific representation of binary clauses
with a usual clause representation for instance).
For more details, see https://wiki.objectweb.org/sat4j/Wiki.jsp?page=WhatsNewInSAT4J1.7
The release is available as 3 archives:
* Full archive (sat4j-1.7.jar, 1.3MB) with all needed Java required libraries, including the Rhino
Javascript interpreter needed by the CSP to SAT translator.
* SAT friendly archive (sat4j-1.7-nojs.jar, 600 KB) without the Rhino library. It means that the
CSP to SAT translator won't work out of the box (adding the rhino library to Java classpath fix the
problem). This is the best option for people willing to have a simple way to try SAT4J for SAT
solving.
* Integrators friendly archive (sat4j-1.7-nojs-nocommons.jar, 348 KB) without the rhino nor the
jakarta commons libraries needed by SAT4J (cli,beanutils and logging).
|
| | | | |
| | |
| | | | | | | | Date: | 09-Jan-2008 | | Title: | MaxSAT solver msuncore
| | Hits: | 999 | | Contributed by: | | | | Dear All,
Ace is a package that compiles a Bayesian network into an Arithmetic Circuit (AC) and then uses the AC to answer multiple queries with respect to the network. Compilation proceeds by encoding the network into CNF, compiling the CNF into d-DNNF by making use of the c2d knowledge compiler, and extracting the AC from the compiled d-DNNF. Ace can also be used to encode networks into CNF without compiling, which makes it a valuable source of interesting problems for weighted model counters and knowledge compilers.
The Ace web page is http://reasoning.cs.ucla.edu/ace. From this page, you can download the recently released version 1.2 of Ace, some benchmarks on which Ace has been applied, and some papers that describe the theoretical foundations of Ace and its relation to approaches based on weighted model counting. |
| | | | |
| | |
| | ozziKs is the implementation of an algorithm that:
- builds a certificate of satisfiability C(F) - a.k.a. strategy or policy or quantified model - for any given true Quantified Boolean Formula F for which a suited inference log is available (at present, only the QBF solver sKizzo produces a suited log);
- verifies C(F) against F, thus certifying in a solver-independent way the validity of F;
- evaluates user-provided expressions of various kinds over C(F);
- writes to file in different formats C(F) and/or the result of the evaluation of the above mentioned expressions.
A detailed user manual is available here. Linux, OS-X, and cygwin versions are available for download at
http://sKizzo.info. |
| | | | |
| | |
| | | This is the first source release of Quantor. It uses a BSD style license.
Version 3.0 is essentially the one that entered the QBF evaluation. |
| | | | |
| | |
| | | After several requests, I have updated relsat to build with recent gnu & MS compilers. |
| | | | |
| | |
| | | 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. |
| | | | |
| | |
| | From the authors web site:
BAT implements a state-of-the-art decision procedure for solving quantifier-free formulas over the extensional theory of fixed-size bit-vectors and fixed-size bit-vector arrays (memories). Such problems often appear in hardware, software, and security domains. BAT uses innovative techniques for efficiently translating from the high-level BAT language into tractable SAT problems.
|
| | | | |
| | |
| | | The MiniUnsat Minimal Unsatisfiable Subset (MUS) finder software is now available trough the link above.
It implements the algorithm presented at SAT2008 in the paper "Finding Guaranteed MUSes fast" by Hans van Maaren and Siert Wieringa. |
| | | | |
| | |
| | |
| | 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 |
| | | | |
| | |
| | | ReViVal is a new preprocessing technique developped by Cédric Piette, Youssef Hamadi and Lakhdar Saïs. ReVivAl is going to be presented in a few days at ECAI'08. The source code of version v0.16 is now available at http://www.cril.fr/~piette/revival
The main idea of this preprocessing is to perform particular forms of resolution (through Unit Propagation) for efficiently producing sub-clauses. It can also use different schemes of learning to add relevant clauses. The vivification algorithm ReViVal is based on is designed to be fully integrated within a SAT solver, taking advantage of most recent techniques and data structures implemented for SAT. The proposed implementation of ReVivAl is based on Minisat. |
| | | | |
| | |
| |
Potassco, the Potsdam Answer Set Solving Collection, bundles tools for
Answer Set Programming (ASP) developed at the University of Potsdam.
So far, this collection contains the source, binaries, and documentation
of the answer set solver clasp, the grounder GrinGo, and their combinations
Clingo and iClingo:
- GrinGo has had its second major release, now supporting function symbols,
classical negation, disjunction, aggregates, an much more.
- Clingo is a monolithic combination of clasp and gringo.
- iClingo is an ASP system that allows for dealing incrementally with
parameterized problems, as encountered for instance in bioinformatics,
planning, and model checking.
- clasp comes now in release 1.1.1
More systems, tools, and documentation will follow.
For bug reports, feature or support requests use either the tracker
at http://sourceforge.net/tracker/?group_id=238741 or drop the authors a mail.
|
| | | | |
| | |
| |
Here is a notice for Cryptol, a specification language and
interpreter for Cryptographic algorithms. Cryptol was just released
today and is free to download from www.cryptol.net for Windows, Linux,
and OSX. From the website: "Cryptol is a language for writing
specifications for cryptographic algorithms. It is also a tool set for
producing high-assurance, efficient implementations in VHDL, C, and
Haskell. The Cryptol tools include the ability to equivalence check
the reference specification against an implementation, whether or not
it was compiled from the specifications."
Cryptol makes heavy use of Satisfiability technology to prove
properties about Cryptol specifications. Cryptol makes it simple to
automatically translate any Cryptol function into an And/Inverter
Graph (Armin's AIGER format) and prove various properties using a
SAT-based tool like Alan Mischenko's ABC. Cryptol also supports
translating into various formats used by SMT solvers like Z3, yices,
and others. Because of this, Cryptol can be used for more than
cryptography.
This free trial version lets you explore the Cryptol language. It compiles
and interprets Cryptol specifications but does not translate the specification
into an implementation and only QuickCheck verification is enabled. The download
includes the documentation suite and many examples.
|
| | | | |
| | |
| | | From the project web site:
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine of formal verification.
Currently OpenSMT supports only the theory of Equality with Uninterpreted Functions (or QF_UF, according to the SMT-LIB terminology). We also provide an "empty" theory solver, that can be used as a template for the development of other theory solvers on top of the existing algorithms. The communication with the rest of the tool is already provided. In the future we plan to extend OpenSMT with other theories.
OpenSMT is built on top of MiniSAT (http://minisat.se). We tried to modify it as little as possible. We carefully marked each modified/added line of code.
OpenSMT is currently released under the GNU General Public Licence version 3. Code is available via SVN at http://code.google.com/p/opensmt/.
|
| | | | |
| | |
| | | BoolVar is a Java library dedicated to problem translation. The input problem has to be specified with Boolean variables and user constraints. The output problem is either a propositional or a peudo-Boolean satisfiability problem, which can be solved thanks to any suitable solver. Please visit BoolVar for more details. |
| | | | |
| | |
| | | NFLSAT is a new SAT solver that operates on the negation normal form (NNF) of the given Boolean circuits. The input to NFLSAT is a Boolean circuit in And Inverter Graph (AIG) format or ISCAS format. |
| | | | |
| | |
| | | Armin Biere just released the source code of precosat, which got first place in the application SAT+UNSAT global category, while being second in the two specific SAT and UNSAT categories. |
| | | | |
| | |
| | | Laurent Simon and Gilles Audemard just made available the source code of their SAT solver glucose.
Glucose got first place in application UNSAT category and second place in SAT+UNSAT application category. |
| | | | |
| | |
| | | | | | | | Date: | 03-Jun-2009 | | Title: | MiniQBF 1.0
| | Hits: | 419 | | Contributed by: | | | | (sorry for double post, I resubmitted due to bad formatting...)
RegSTAB is a SAT-solver able to deal with formulae patterns
e.g. you can give it the pattern "P_1 / /i=1..n (P_i -> P_i+1) / -P_n" and RegSTAB will be able to tell you that this is unsatisfiable for all n>0
|
| | | | |
| | |
| | | The new release focuses mainly in simplifying the integration and the use of the solvers in Java programs.
The release includes also improved pseudo boolean and maxsat solvers.
SAT4J 2.1 core and pseudo packages will ship with Eclipse 3.5 next month. |
| | | | |
| | |
| | | Dear all,
The ManySAT source code is now online here. If you use it in your research or in any application, please send us a small email, and we will put you in our list of known users.
We hope that this new resource will benefit to the whole SAT community!
Bests,
Said, Lakhdar, and Youssef |
| | | | |
| | |
| | We present the IDP system, a system for model expansion (a generalization of finite model generation) for FO(ID), i.e., first-order logic extended with inductive definitions.
IDP consists of two components: a grounder called GidL, and a propositional model generator called MiniSat(ID), which is een extension of MiniSat. GidL is very flexible, and allows arbitrary FO input. MiniSat(ID) exploits the full propagation efficiency of MiniSat.
To illustrate its use: consider the problem of graph colouring. The following is an IDP file that models the problem:
Given:
type {Vertex Colour}
Edge(Vertex,Vertex)
Find:
Colouring(Vertex):Colour
Satisfying:
! c1 c2: Edge(c1,c2) => Colouring(c1) ~= Colouring(c2).
Here "!" means "for all" and "~=" means "not equals"; otherwise the semantics is obvious (we refer to the website for a formal exposition). Then with a given interpretation of the domains Vertex and Colour and of Edge/2, such as
Vertex = {a; b; c}
Colour = {R; G; B}
Edge = {a,b; b,c; c,a}
the IDP system will swiftly find an expansion model, e.g.,
Colouring = {a->R; b->G; c->B}
More complex problems may include inductive definitions (e.g. transitive closure) and aggregate expressions. |
| | | | |
| | |
| | | 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/. |
| | | | |
| | |
| | | Niklas Sorensson just released Minisat 2.2 today, during the SAT conference.
The source code is now available in a public GIT repository. |
| | | | |
| | |
© 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
