SAT problem
- We propose a new strategy to manage learnt clauses on CDCL solvers. The source code of the solver minisat_psmdyn is available here. The associated paper has received the best paper award at SAT 2011 conference.
- Take a look to our SAT solver glucose
- We also work on a version of glucose enriched with extended resolution, see here for more details
- SatHyS is a hybrid SAT solver (combination of CDCL and local search). It is efficient on a large panel of benchmarks
SAT Modulo Theory
Satisfiability modulo theories (SMT) can be seen an an extended form of propositional satisfiability where propositions are either simple boolean propositions or constraints in a specific theory- I was a member of the MathSAT team. MathSAT is based on the approach of integrating a state-of-the-art SAT solver with a hierarchy of dedicated solvers for the different theories (here, Linear arithmetic over the integers). MathSAT has been applied on formal verification of timed systems
Finite model Generation
A finite model of a first-order theory is an interpretation of the constants, function symbols a nd predicates over a finite domain of individuals, that satisfies the axioms of the theory. Model generation can be used to prove the consistency of a first-order theory (i.e. testing that a model exists) or to find a counter model to disprove its validity. More specifically, it can be used within more general theorem provers to find a counter example of some expected conjecture or automatically generated lemma and hence help the program prove or refute the validity of fo rmulas. In this sense, model generation is complementary to theorem proving.
I worked on different ways to improve finite model generators :- constraint propagation
- Elimination of isomorphic interpretations
A modified version of the finite model generator SEM (Hantao and Jian Zhang) is available (source code in C). It contains different improvements proposed (see also journal of automated reasoning paper).