Course projects topics

•(Mostly  survey  +  some  experiments)  Study  different  conflict-­‐clause  learning  schemes,  and  see  which  schemes  work  most  efficiently  at  inversion/collision  problems  for  hash  functions  •(Experimental  project  with  MapleSAT)  Optimizing  learning  rate  to  learn  “high  quality”  conflict  clauses.  Modify  the  reward  function  of  the  branching  heuristic  such  that  variables  in  low-­‐LBD  learnt  clause  get  a  higher  reward.  •(Survey)  SMT  solvers  for  refinement  types  •(Survey)  Branching  heuristics  in  SAT  solving  •(Experimental  project  with  MapleSAT)  Use  programmatic  interface  of  a  SAT  solver  to  encode  constraints  to  guide  search  •(Experimental  project  with  MapleSAT)  Clause  minimization  technique  to  reduce  size  of  conflict  clause  database  •(Experimental  project  with  MapleSAT)  How  to  initialize  branching  heuristics  such  that  the  solver  is  faster  than  the  current  approach  where  all  variables  get  the  same  initial  activity  score.

 Can  we  use  community  structure?              .