Deadline Countdown

Heads up on SAT research

SAT related books

Other SAT related sites

Date: 16-Jul-2010 Title: Parallel SAT Solving on Peer-to-Peer Desktop Grids Hits: 191 Contributed by: Sven Schulz Keywords: SAT tools, Distributed Computing, distributed parallel dynamic learning, Divide-and-Conquer Algorithms, null, null         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."

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: 31-Oct-2006 Title: Decomposing satisfiability problems: Using graphs to get better insight into satisfiability problems Hits: 1081 Contributed by: Marijn Heule Keywords: Divide-and-Conquer Algorithms, Visualisation         This master thesis deals with the question how to exploit the structure of a CNF to solve it faster. We focus on a "divide and conquer" approach to solve satisfiability (SAT) problems. Several decomposable graph representations of CNF formulas are studied on various structures instances. Small (bi-)connected components in these graphs turned out to come from blocked clauses in general. To increase the chance of graphs falling apart the formulas are preprocessed by removal of redundant clauses. We show that the tree decomposition of graph representations can provide (visual) insight in the structure of formulas. However, to compute these decompositions (even approximations) is very time consuming, making it ineffective for practical use. The diameter of these graphs - which is fast to compute - seems to be an effective indicator to select the fastest SAT solver architecture to solve the underlying formula. We introduce the concept of a variable break-set: When all variables in a break-set are assigned a truth value, the remaining formula will be partitioned. Branching on break-set variables can increase the performance of the solver, although the improvement depends largely on the quality of the break-set.

Date: 19-Jan-2006 Title: An update has been released of software which compiles a broad class of problems into a SAT formulas. Hits: 2270 Contributed by:       Date: 03-Aug-2005 Title: DC-SSAT: A Divide-and-Conquer Approach to Solving Stochastic Satisfiability Problems Efficiently Hits: 1620 Contributed by: Stephen Majercik Keywords: Stochastic Satisfiability, Divide-and-Conquer Algorithms         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.         © 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.