Recent news about SAT subscribe via RSS

• Jul 6, 2015  FMCAD Student Forum 2015 by Georg Weissenbacher CFP 

  The deadline of this year's FMCAD student forum has been extended - the new deadline is July 09, 2015.

• Jul 2, 2015  SAT & CSP Track at IEEE ICTAI 2015 by Jean-Marie Lagniez CFP 

  Due to many requests, a new submission deadline has been fixed.

• Jun 12, 2015  22nd RCRA workshop (RCRA 2015) by Marco Maratea CFP 

  This event follows the series of the RCRA (Knowledge Representation and Automated Reasoning) annual meetings, held since 1994. The success of the previous events shows that RCRA is becoming a major forum for exchanging ideas and proposing experimentation methodologies for algorithms in Artificial Intelligence.

• Jun 11, 2015  Fifth International Workshop on the Cross-Fertilization Between CSP and SAT by Yael Ben-Haim CFP 

  CSPSAT 2015: Call for Papers
  Fifth International Workshop on the Cross-Fertilization Between CSP and SAT
  In conjunction with CP 2015
  Cork, Ireland
  August 31, 2015
  

• Jun 2, 2015  SAT & CSP Track at IEEE ICTAI 2015 by Jean-Marie Lagniez CFP 

  Following the success of the first and second editions of the SAT and CSP technologies special track at ICTAI 2013 and ICTAI 2014, this year again the IEEE-ICTAI conference will highlight a track dedicated to SAT and CSP.

• Jun 1, 2015  Weakening Cardinality Constraints Creates Harder Satisfiability Benchmarks by Ivor Spence Benchmarks 

  For some time, the satisfiability formulae that have been the most difficult to solve for their size have been crafted to be unsatisfiable by the use of cardinality constraints. Recent solvers have introduced explicit checking of such constraints, rendering previously difficult formulae trivial to solve. A family of unsatisfiable formulae is described that is derived from the sgen4 family but cannot be solved using cardinality constraints detection and reasoning alone. These formulae were found to be the most difficult during the SAT2014 competition by a significant margin and include the shortest unsolved benchmark in the competition, sgen6- 1200-5-1.cnf.

• May 25, 2015  MAXSAT 2015 Evaluation by Jordi Planes Competition  CFP 

  Submission for the MAXSAT competition is now open. The deadline for submitting solvers and benchmarks is June 30.

• May 20, 2015  ACAI’15 Summer School on Constraints Solving Techniques in AI by Daniel Le Berre Event 

  In odd-numbered years, the European Coordinating Committee for Artificial Intelligence (ECCAI) sponsors a specialised course in Artificial Intelligence, called Advanced Course on Artificial Inteliigence (ACAI).

• May 16, 2015  22th RCRA workshop (RCRA 2015) by Marco Maratea CFP 

  The RCRA group (Knowledge Representation & Automated Reasoning) of theAI*IA (Italian Association for Artificial Intelligence) organizes the 22th RCRA workshop: Experimental evaluation of algorithms for solving problems with combinatorial explosion (RCRA 2015)

• May 11, 2015  CFP QUANTIFY 2015 by Florian Lonsing CFP  QBF 

  The goal of the 2nd International Workshop on Quantification (QUANTIFY 2015) is to bring together researchers who investigate the impact of quantification from a theoretical as well as from a practical point of view.

• Apr 30, 2015  Fifth International Workshop on the Cross-Fertilization Between CSP and SAT by Yael Ben-Haim CFP 

  CSPSAT 2015: Call for Papers
  Fifth International Workshop on the Cross-Fertilization Between CSP and SAT
  In conjunction with CP 2015
  Cork, Ireland
  August 31, 2015
  

• Apr 23, 2015  SAT'15 Deadline Extended by Sean Weaver CFP 

  Abstract submission deadline for SAT'15 extended to April 29th!

• Apr 22, 2015  Overview and analysis of the SAT Challenge 2012 solver competition by Adrian Balint, Anton Belov, Matti Järvisalo and Carsten Sinz Competition 

  Programs for the Boolean satisfiability problem (SAT), i.e., SAT solvers, are nowadays used as core decision procedures for a wide range of combinatorial problems. Advances in SAT solving during the last 10–15 years have been spurred by yearly solver competitions. In this article, we report on the main SAT solver competition held in 2012, SAT Challenge 2012. Besides providing an overview of how SAT Challenge 2012 was organized, we present an in-depth analysis of key aspects of the results obtained during the competition.

• Apr 17, 2015  13th International Conference on Logic Programming and Non-monotonic Reasoning by Francesco Calimeri CFP 

  Updated deadlines.

• Apr 3, 2015  18th Int. Conf. on Theory and Applications of Satisfiability Testing by Sean Weaver CFP 

  Abstract submission deadline for SAT'15 is April 22nd!

• Mar 18, 2015  New version 1.2 of PBLib is out! by Peter Steinke PBO 

  Many different encodings for Pseudo-Boolean (PB) constraints into conjunctive normal form (CNF) have been proposed in the past. The PBLib project starts to collect and implement these encodings to be able to encode PB constraints in a very simple, but effective way.

• Mar 18, 2015  ICCL Summer School on Reasoning in Dresden, Germany, September 13 - 26, 2015 by Peter Steinke CFP 

  The summer school “Reasoning” is a platform for knowledge transfer within a very rapid increasing research community in the field of “Computational Logic”. We will offer introductory courses covering the fundamentals of reasoning, courses at advanced levels, as well as applied courses and workshops dedicated to specialized topics and the state of the art. All lecturers are leading researchers in their field and have been awarded prizes.

• Mar 13, 2015  CFP QUANTIFY 2015 by Florian Lonsing CFP  QBF 

  The goal of the 2nd International Workshop on Quantification (QUANTIFY 2015) is to bring together researchers who investigate the impact of quantification from a theoretical as well as from a practical point of view.

• Mar 2, 2015  13th International Conference on Logic Programming and Non-monotonic Reasoning by Francesco Calimeri CFP 

  Complimentary membership offer for conference registrants new to AAAI.

• Feb 28, 2015  Savile Row 1.6.2 Released with SAT backend by Daniel Le Berre Tools 

  The main change in 1.6.2 is the addition of the SAT backend. The first iteration of this feature was written by Patrick Spracklen as a summer student project. All constraints in the language have a SAT encoding. MiniSat and Lingeling are fully supported as backend solvers: 1.6.2 can run them, parse the solution and collect some statistics from the solver.