Date: 28-Nov-2008 Title: Call for Papers: SAT 2009 - 12th International Conference on Theory and Applications of Satisfiability Testing Hits: 37 Contributed by: Daniel Le Berre Keywords: conference information         SAT 2009 - 12th International Conference on Theory and Applications of Satisfiability Testing Call for Papers June 30 - July 3, 2009, Swansea, United Kingdom http://cs.swan.ac.uk/~csoliver/SAT2009/index.html * The International Conference on Theory and Applications of Satisfiability Testing is the primary annual meeting for researchers studying the propositional satisfiability problem (SAT). SAT'09 is the twelfth SAT conference. SAT'09 features the SAT competition, the the Pseudo-Boolean evaluation, and the MAX-SAT evaluation. * The topics of the conference span practical and theoretical research on SAT and its applications and include, but are not limited to, proof systems, proof complexity, search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, simplifiers, tools, case studies and empirical results. SAT is interpreted in a rather broad sense: besides propositional satisfiability, it includes the domain of quantified boolean formulae (QBF), constraints programming techniques (CSP) for word-level problems and their propositional encoding and particularly satisfiability modulo theories (SMT). * Important dates: Abstract submission due: 20 Feb 2009; Paper submission: 27 Feb 2009; Notification: 29 Mar 2009.

Date: 21-Nov-2008 Title: A SAT solver inside Mathematica 7? Hits: 76 Contributed by: Daniel Le Berre Keywords: SAT application         From Mathematica web site: Mathematica 7 introduces major new capabilities in Boolean computation, for the first time bringing large-scale Boolean computation into mainstream computing. Building on recent algorithmic advances, Mathematica 7 provides comprehensive capabilities for handling Boolean expressions with hundreds to hundreds of thousands of variables—all fully integrated with Mathematica's other symbolic capabilities—making possible new approaches to large-scale design, verification and optimization of discrete and logical systems in a wide variety of fields.

Date: 21-Nov-2008 Title: AI'09 GRADUATE STUDENT SYMPOSIUM Hits: 43 Contributed by: Anonymous Keywords: call for papers, null         Kelowna, BC, Canada May 24, 2009 CALL FOR PAPERS – Deadline January 30th, 2009 AI 2009, the twenty-second Canadian Conference on Artificial Intelligence, invites graduate students to submit four-page extended abstracts of their thesis for possible inclusion in the AI 2009 Graduate Student Symposium. The symposium will be a one-day pre-conference event, where students of accepted abstracts will be invited to give a presentation on their thesis work before a group of peers as well as a small team of expert AI researchers who would offer a critique of each presentation and provide support, advice, and mentoring. Important Dates Full paper submission due: January 30th, 2009 Notification of acceptance: March 3rd, 2009 Final paper due: March 16th, 2009 Graduate Student Symposium: May 24th, 2009 Contact Svetlana.Kiritchenko at nrc-cnrc.gc.ca

Date: 25-Oct-2008 Title: Open Source ASP solver made available: Potassco Hits: 133 Contributed by: Daniel Le Berre Keywords: Answer Set Programming         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.

Date: 24-Oct-2008 Title: An activity based Heuristic for SAT Hits: 163 Contributed by: LAKHDAR SAIS Keywords: DPLL         Title: Improving backtrack Search by means of Redundancy Abstract : In this paper, a new heuristic that can be grafted to many of the most efficient branching strategies for Davis Putnam procedures for SAT is described. This heuristic gives higher weight to clauses that have been shown unsatisfiable at some previous steps of the search process. It is shown efficient for many classes of SAT instances, in particular structured ones. by Brisoux L., Grégoire É., Saïs L., Proc. of the 11th Int. Symposium on Methodologies for Intelligent Systems (ISMIS'99), Z.W. Ras and A. Skowron (eds.), Varsovie, Pologne, LNCS 1609, Springer, pp. 301-309, juin 1999

Date: 24-Oct-2008 Title: A US Patent has been published this summer regarding Chaff (Inventors Moskewicz, Madigan and Malik) Hits: 205 Contributed by: Daniel Le Berre Keywords: null         Here is a statement from Sharad Malik regarding the consequence of such patent for academia: The chaff software and related intellectual property have been freely available for research purposes and will continue to be available for free use by the research community for non-commercial purposes. This includes the development of other SAT solvers with this technology as well as their research use. (See http://www.princeton.edu/~chaff/zchaff.html. for all terms and conditions). For commercial use of this technology please contact John Ritter (jritter@princeton.edu) in the Office of Technology Licensing at Princeton University.

Date: 22-Oct-2008 Title: Applied Formal Verification Track EuroCAST'09 Hits: 138 Contributed by: Armin Biere Keywords: BMC, Verification, QBF, SAT application, SAT tools, null         Applied Formal Verification Track EUROCAST'09 Las Palmas, Canary Islands, Spain IMPORTANT DATES February 15-20, 2009 Ext. Abstracts: 31. Oktober, 2008 (2 pages LNCS style) Conference: 15.-20. February, 2009 Full Papers: 30. April, 2009 (prob. again in LNCS) http://www.iuctc.ulpgc.es/spain/eurocast2009/index.html TOPICS In the last decade the topic of formal verification has left the ivory tower of academic research. In hardware design many industrial projects rely in one way or the other on formal verification tools. The same trend can be seen in software. The main driving force behind this development is on one hand the increasing complexity of todays design, which can not be handled by traditional testing techniques alone, and on the other hand by the increasing dependability of our daily lives on computer systems. However, also the core engines, such as SAT solvers are becoming much more powerful. In this workshop we want to bring to together researchers in applied formal verification. We focus on formal verification engines. The topics include, but are not limited to the following Satisfiability (SAT) Satisfiability Modulo Theories (SMT) Quantified Boolean Formulas (QBF) Constraint Programming (CP) Equivalence Checking (EC) Model Checking (MC) Theorem Proving (TP) Beside papers on verification engines we also welcome case studies and papers on the border line of verification, including synthesis, compilation and modelling. Our main goal is to improve practicability and scalability of formal methods. SUBMISSION An extended two pages abstract, including references in English with indication of the workshop of the intended contribution, e.g. 'Applied Formal Verification' must be sent (via webpage or by e-mail) before October, 31, 2008 to the Organizing Commitee Chairman: aquesada@dis.ulpgc.es.

Date: 08-Oct-2008 Title: Effective SAT Solving, by Niklas Sorensson, Thesis for the Degree of Doctor of Philosophy, University of Gothenburg, September 2008 Hits: 298 Contributed by: Daniel Le Berre Keywords: Data structure, SAT application, Instance simplification, SAT tools, pseudo boolean optimization, SAT-Based, Linear Constraints, SAT-solver, Cardinality solving, Pseudo-Boolean Solving         Thesis's abstract: A growing number of problem domains are successfully being tackled by SAT solvers. This thesis contributes to that trend by pushing the state-of-the-art of core SAT algorithms and their implementation, but also in several important application areas. It consists of five papers: the first details the implementation of the SAT solver MINISAT and the other four papers discuss specific issues related to different application domains. In the first paper, catering to the trend of extending and adapting SAT solvers, we present a detailed description of MINISAT, a SAT solver designed for that particular purpose. The description additionally bridges a gap between theory and practice, serving as a tutorial on modern SAT solving algorithms. Among other things, we describe how to solve a series of related SAT problems efficiently, called incremental SAT solving. For finding finite first order models the MACE-style method that is based on SAT solving is well-known. In the second paper we improve the basic method with several techniques that can be loosely classified as either transformations that make the reduction to SAT result in fewer clauses or techniques that are designed to speed up the search of the SAT solver. The resulting tool, called PARADOX, won the SAT/Models division of the CASC competition in 2003 and has not been beaten since by a single general purpose model finding tool. In the last decade the interest in methods for safety property verification that are based on SAT solving has been steadily growing. One example of such a method is temporal induction. The method requires a sequence of increasingly stronger induction proofs to be performed. In the third paper we show how this sequence of proofs can be solved efficiently using incremental SAT solving. The last two papers consider two frequently occurring types of encodings: (1) the problem of encoding circuits into CNF, and (2) encoding 0-1 integer linear programming into CNF and how to use incremental SAT to solve the intended optimization problem. There are several encoding patterns that occur over and over again in this thesis but also elsewhere. The most noteworthy are: incremental SAT, lazy encoding of constraints, and bit-wise encoding of arithmetic influenced by hard- ware designs for adders and multipliers. The general conclusion is: deploying SAT solvers effectively requires imple- mentations that are efficient, yet easily adaptable to specific application needs. Moreover, to get the best results, it is worth spending effort to make sure that one uses the best codings possible for an application. However, it is important to note that this is not absolutely necessary. For some applications naive problem codings work just fine which is indeed part of the appeal of using SAT solving.

Date: 04-Oct-2008 Title: Canadian AI 2009 Hits: 174 Contributed by: Anonymous Keywords: null         AI'09, the twenty-second Canadian Conference on Artificial Intelligence, will be held in Kelowna, British Columbia (May 25-27, 2009). The organizers invite papers that present original work in all areas of Artificial Intelligence. Paper submission due: January 23rd, 2009 Notification of acceptance: March 3rd, 2009 Final paper due: March 16th, 2009

Date: 02-Oct-2008 Title: OpenSMT: an Open Source SMT solver based on Minisat 2.0 Hits: 217 Contributed by: Daniel Le Berre Keywords: SAT application, SAT-Based         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/.