====== SATMiner ======

SATMiner is a library for searching interesting patterns using constraint programming/SAT backend. 
It was initially developed as a prototype for the [[http://liris.cnrs.fr/dag|DAG]] project, in collaboration with people at [[http://www.cril.univ-artois.fr/decMining/|CRIL]].

It is currently used as a basis for experiments on SAT/pseudo boolean based pattern mining on:
  * sequences
  * attributes sets in relational data (SatQL language)

The current version is coded in Java and uses [[http://www.sat4j.org/|SAT4J]] and a modified version of [[http://minisat.se/|MiniSat]] as backends. It also uses the [[http://boolvar.sourceforge.net/|BoolVar/PB]] library, as well as an implementation of [[http://dl.acm.org/citation.cfm?id=1575495|cardinality networks]] for translation of some pseudo-boolean constraints to SAT.

===== Download =====

GIT, stable branch: https://liris.cnrs.fr/~ecoquery/satminer.git, {{:research:satminer:satminer.jar|lastest stable binary jar file}}

  * {{:research:satminer-2014-05-12.tgz|source}} (2014-05-12, changed syntax for SatQL((this breaks backward compatibility)): now SQL expressions (queries and conditions) should be in  "{ }" braces and Java joins are not available anymore. However arbitrary SQL expressions can now be used)
  * {{:research:satminer-2014-04-15.tbz|source}} (2014-04-15, added IF THEN, LIKE, LIMIT to SatQL,  [[http://liris.cnrs.fr/~ecoquery/files/satminer-2014-04-15-with-bench-data.tbz|version including bench datasets]])
  * {{:research:satminer-2014-02-18.tgz|source}} (2014-02-18, includes Boolvar/PB and a modified version of minisat, fixes compilation problems)
  * {{:research:satminer-2014-02-17.tgz|source}} (2014-02-17, includes Boolvar/PB and a modified version of minisat)

===== Involved people =====
  * [[http://liris.cnrs.fr/~ecoquery|Emmanuel Coquery]] (LIRIS)
  * [[http://www.cril.univ-artois.fr/~jabbour/|Said Jabbour]] (CRIL)
  * [[http://liris.cnrs.fr/~jmpetit|Jean-Marc Petit]] (LIRIS)
  * [[http://www.cril.univ-artois.fr/~sais/|Lakhdar Sais]] (CRIL)

===== Related publications =====

  * Emmanuel Coquery, Saïd Jabbour, Lakhdar Saïs, Yakoub Salhi: //A SAT-Based Approach for Discovering Frequent, Closed and Maximal Patterns in a Sequence//. [[http://www.lirmm.fr/ecai2012/|ECAI 2012]]: 258-263 {{:research:ecai2012046.pdf|pdf}}
  * Emmanuel Coquery, Jean-Marc Petit, Lakhdar Sais: //Using SAT and SQL for Pattern Mining in relational databases//. [[http://cocomile.disi.unitn.it/2012/index.html|First workshop on COmbining COnstraint solving with MIning and LEarning]], 2012. {{:research:rl_sql_sat.pdf|pdf}}
  * Emmanuel Coquery, Saïd Jabbour, Lakhdar Sais: //A Constraint Programming Approach for Enumerating Motifs in a Sequence//. [[http://liris.cnrs.fr/wdpm2011/|ICDM Workshops 2011, WDPM]]: 1091-1097 {{:research:wdpm2011wks.pdf|pdf}}