GCAI will feature the following invited talk. 

• Robert Nieuwenhuis (Technical University of Catalonia).
  SAT-based techniques for integer linear constraints
  ABSTRACT. SAT and SAT Modulo Theories (SMT) are well known as workhorses for formal verification applications.  But SAT- and SMT-like techniques are also highly effective for AI applications such as constraint solving and optimization.  Here we explain how this idea has been validated at Barcelogic.com and elsewhere.  We shorty introduce SAT/SMT as well as our new IntSat method for Integer Linear Programming (ILP) and 0-1 ILP. 
  Some demos on real-world industrial problems will illustrate easy logic-based modeling and cases where our solvers outperform the best-known commercial ones.