JSAT Links


JSAT Links offers you a glance to web sites which are recognized as useful to our community. We welcome links to sites containing benchmarks, solvers or news ( not personal home pages ).

Generally, an email to the editor in chief containing a short description ( plain text ) and the URL involved, will suffice to have a link established. Please check the JSAT Solvers page to see how your contribution will be exposed. Please restrict to three or four lines only in your description.

It is emphasized that contributions to JSAT Links are not considered Journal contributions and hence are not to be referred to as such. When it becomes apparent that a link is outdated or not functioning properly it will be removed.

Contributions are indexed by date of submission ( year/month/day ).

Benchmarks   Solvers and Tools   News   Competitions  



Benchmarks

2005-11-01. Emmanuel Zarpas.
BMC Benchmarks from the IBM Formal Verification Benchmarks Library (URL). SAT benchmarks generated by Bounded Model Checking in formal verification of several systems on chip. Several instances were used in the SAT03, 04, 05 competitions.

2005-08-16. Volker Sorge.
New Quasigroup Benchmarks (URL). Benchmarks generated during the automatic construction of classification theorems for quasigroups. Problems are available in DIMACS and extended DIMACS format.

2004-11-11. Holger Hoos et al.
SATLIB (URL). Resources for SAT related research. This web site provides a large and varied collection of benchmark instances, a number of solvers and some other information.

2004-10-26. Ke Xu.
Forced Satisfiable SAT Benchmarks (URL). Benchmarks are generated based on a random CSP model with exact phase transitions. The results of SAT Competition 2004 show that as the problem size increases, these benchmarks can become very challenging to solve for various SAT solvers.

2004-10-26. Miroslav Velev.
SAT Benchmarks (URL). SAT benchmarks generated by M.N. Velev in formal verification of high-level microprocessors by correspondence checking.



Solvers and tools

2008-12-20. Paulo Flores.
PMSAT (URL). PMSat is a parallel SAT-solver that uses MiniSAT as engine. PMSat was implemented with MPI technology, a portable and the industry's de-facto standard for distributed computation, to be executed in clusters or grids of computers. It was developed at INESC-ID, in the ALGOS group by Luís Gil, a student of Computer Science at Instituto Superior Técnico / Technical University of Lisbon, under supervision of professors Paulo Flores, Luís Miguel Silveira. A description of the solver and its results can be found in the JSAT journal (Vol. 6, pages 71-98, Nov. 2008).

2007-08-18. Christian Herde.
HySAT (URL). HySAT is a satisfiability checker for Boolean combinations of arithmetic constraints over real- and integer-valued variables which can also be used as a bounded model checker for hybrid (discrete-continuous) systems. A peculiarity of HySAT, which sets it apart from many other solvers, is that it is not limited to linear arithmetic, but can also deal with nonlinear constraints involving transcendental functions.

2006-04-27. Roberto Sebastiani.
Mathsat (URL). Satisfiability modulo theories (SMT) can be seen an an extended form of propositional satisfiability, where propositions are either simple boolean propositions or constraints in a specific theory. MathSAT is a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Function (EUF), Separation Logic (SEP), Linear Arithmetic over the Reals
(LA(R)) and Linear Arithmetic over the Integers (LA(Z)). MathSAT is based on the approach of integrating a state-of-the-art SAT solver with a hierarchy of dedicated solvers for the different theories, and implements several optimization techniques. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power, in such a way that more expensive layers are called less frequently. MathSAT has been applied in different real-world application domains, ranging from formal verification of infinite state systems (e.g. timed and hybrid systems) to planning with resources, equivalence checking and model checking of RTL hardware designs.

2006-02-28. CRIL.
SAT4J (URL). SAT4J is an open source library of SAT solvers in Java. The aim of the library is to allow Java developers to embed SAT technology into their application. The library is updated regularly with latest SAT technologies proven effective during the SAT competitions.

2005-07-15. Niklas Een.
The MiniSat page (URL). Contains sources and binaries for the open-source SAT solver MiniSat and related software, such as SatELite (CNF minimizer) and MiniSat+ (Pseudo-Boolean solver). The combination of MiniSat and SatELite won the industrial categories of the SAT competition 2005.

2005-02-10. Fadi Aloul.
PBS (URL). An incremental pseudo-Boolean backtrack search SAT solver and optimizer. Can read CNF and PB (0/1 inequality) constraints.

2005-02-10. Fadi Aloul.
Shatter (URL). A pre-processor that identifies and breaks symmetries of CNF formulas. Symmetries are identified using the graph automorphism tool Saucy. They are then broken by adding appropriate symmetry-breaking clauses to the original formula.

2005-02-10. Fadi Aloul.
Satometer (URL). Measures the progress of backtrack-search SAT solvers. It can be used with any backtrack search SAT solver to report the percentage of search space actually explored by the solver. It requires the solver to emit the set of clauses corresponding to the conflicts encountered during the search. It can be used dynamically, while the SAT solver is running, to indicate progress in the search for a solution or as a postprocessor to analyze the result of an aborted or completed search.

2005-02-10. Fadi Aloul.
MINCE (URL). FORCE (URL). A pre-processor that performs a static global ordering of the problem's variables. Can be used for SAT and BDDs. MINCE uses the leading-edge hypergraph placer CAPO. FORCE is much faster than MINCE, doesnt use any external tools, and consists of less than 1000 lines of code.

2005-01-13. Armin Biere.
Limmat, Limboole, Compsat and Quantor (URL). Beside the SAT solvers Limmat with its front-end Limboole and Compsat, this is also the home page of the QBF solver Quantor. All of them took part in recent SAT and QBF solver competitions.

2004-11-11. Alexander Nadel.
JERUSAT (URL). Jerusat's main feature is that while exploring the subspace under -A (A is a decision literal), it explores only paths found to be dependent on A's value earlier. Jerusat came in first in the Industrial, Satisfiable category at the SAT'04 competition.

2004-10-26. Sharad Malik et al.
SAT Research at Princeton (URL). The chaff website provides the latest software releases for the chaff SAT package, the quaffle QBF package, as well as all publications from the Princeton SAT group.

2004-10-05. Marijn Heule et al.
March (URL). A lookahead SAT-solver with extended pre-processor reasoning and a 3-SAT translator. Fast performance is realised by data-structures optimised for the lookahead routines and the addition of the so-called constraint resolvents.

2004-10-05. Marijn Heule et al.
March_eq (URL). A lookahead SAT-solver with integrated equivalence reasoning. Most important steps regarding equivalence reasoning are performed during the pre-processing. March_eq solved most benchmarks and series in the "handmade all" category at the SAT 2004 competition.



News

2005-07-05. Holger Hoos.
The SAT Conferences Page (URL). This page contains information on the coming and past SAT conferences and people involved.

2004-11-04. Daniel Le Berre.
SAT Live! (URL). The aim of this web site is to collect data concerning any kind of work related to SAT. It is the place to announce new published articles, new versions of software, new conferences and so on.



Competitions

2006-08-02. Roberto Sebastiani et al.
The Satisfiability Modulo Theories Competition (URL). SMT-COMP is a satellite event of CAV'06 (August 16 - 20, 2006, Seattle, Washington, USA).

2006-01-10. Carsten Sinz et al.
SAT-race 2006 (URL). Special event on Solver competition, affiliated with the SAT 2006 conference.

2004-11-04. Daniel Le Berre et al.
The SAT 2005 Competition (URL). The official web site of the yearly SAT competition. Contains the competition rules, the input/output format, tools for the competitors. The detailed results of all the competitions are available from this site.