Date: 03-Aug-2005 Title: DC-SSAT: A Divide-and-Conquer Approach to Solving Stochastic Satisfiability Problems Efficiently Hits: 3 Contributed by: Stephen Majercik Keywords:         We present DC-SSAT, a sound and complete divide-and-conquer algorithm for solving stochastic satisfiability (SSAT) problems that outperforms the best existing algorithm for solving such problems (ZANDER) by several orders of magnitude with respect to both time and space. DC-SSAT achieves this performance by dividing the SSAT problem into subproblems based on the structure of the original instance, caching the viable partial assignments (VPAs) generated by solving these subproblems, and using these VPAs to construct the solution to the original problem. DC-SSAT does not save redundant VPAs and each VPA saved is necessary to construct the solution. Furthermore, DC-SSAT builds a solution that is already human-comprehensible, allowing it to avoid the costly solution rebuilding phase in ZANDER. As a result, DC-SSAT is able to solve problems using, typically, 1-2 orders of magnitude less space than ZANDER, allowing DC-SSAT to solve problems ZANDER cannot solve due to space constraints. And, in spite of its more parsimonious use of space, DC-SSAT is typically 1-2 orders of magnitude faster than ZANDER. We describe the DC-SSAT algorithm and present empirical results comparing its performance to that of ZANDER on a set of SSAT problems.

Date: 02-Aug-2005 Title: SAT 2005 Competition detailed results Hits: 16 Contributed by: Daniel Le Berre Keywords: BMC, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Repository, Random 3SAT, Randomization, Verification, Structure of problems, EDA, Benchmark, SAT application, Randomised Algorithms, Instance simplification, Learning, SAT tools, branching heuristics, Dynamic restarts, Preprocessing, Unit Propagation         All the data concerning the SAT 2005 competition is now publicly available (including benchmarks access). Watch out the competition blog for new additions on that web site.

Date: 27-Jul-2005 Title: CAMA: A Multi-Valued Satisfiability Solver Hits: 23 Contributed by: Cong Liu Keywords: DPLL, Intelligent Backtracking, Equivalency Reasoning, Learning, multi-value         Binaries for Windows Cygwin and Linux are available for download.

Date: 19-Jul-2005 Title: Award winning (crafted category) Vallst source code available! Hits: 135 Contributed by: Daniel Le Berre Keywords:         The source code of the winner of the SAT and SAT+UNSAT specialties in the crafted category at the SAT 2005 competition is now available. Note that the webpages are temporarily hosted on the SAT competition website because the author had some trouble to host it on vallst.org for the moment.

Date: 08-Jul-2005 Title: MiniSAT and SatELite source code available! Hits: 237 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.