Deadline Countdown

Heads up on SAT research

SAT related books

Other SAT related sites

Date: 26-Nov-2006 Title: Special issue of JSAT on CFV Hits: 2843 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: 03-Feb-2004 Title: An Improved Semidefinite Programming Relaxation for the Satisfiability Problem Hits: 2189 Contributed by: Miguel Anjos Keywords: Alternative approach, semidefinite programming         In this paper we introduce a new SDP relaxation for the satisfiability problem in conjunctive normal form. This SDP relaxation arises from the recently introduced paradigm of ``higher liftings' for constructing semidefinite programming relaxations of discrete optimization problems. In particular, we report the performance of our SDP relaxation on 3 of the 6 instances in the hgen8 set that were unsolved during the SAT 2003 competition. The SDP relaxation is infeasible for the 3 instances, and in particular it was able to prove in less than two hours the unsatisfiability of the instance hgen8-n260-01-S1597732451.shuffled-as.sat03-885 which was the smallest unsatisfiable instance that remained unsolved during the competition.