Difference between revisions of "Jobs/M2 2015 ADL SAT-based Minimization"

From LRDE

(Created page with "{{Job |Reference id=M2 2015 ADL SAT-based Minimization |Title=Minimization of Büchi automata using SAT-solving. |Dates=5-6 months in 2015 |Research field=Automata Theory |Rel...")
 
 
(5 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 
{{Job
  
{{Job
 
|Reference id=M2 2015 ADL SAT-based Minimization
  
|Reference id=M2 2015 ADL SAT-based Minimization
−
|Title=Minimization of Büchi automata using SAT-solving.
 +
|Title=Minimization of Büchi automata using SAT-solving
 
|Dates=5-6 months in 2015
  
|Dates=5-6 months in 2015
 
|Research field=Automata Theory
  
|Research field=Automata Theory
 
|Related project=Spot
  
|Related project=Spot
 
|Advisor=Alexandre Duret-Lutz
  
|Advisor=Alexandre Duret-Lutz
−
|General presentation of the field=The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique (in Spot version 1.2) allows us to minimize deterministic Büchi automata using a SAT-solver.
 +
|General presentation of the field=The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique allows us to minimize deterministic Büchi automata using a SAT-solver; the implementation is actually not restricted to Büchi and can work with deterministic omega-automata with any acceptance conditions.
−  
⚫
To minimize a n-state deterministic Büchi automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic
  
⚫
Büchi automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc.
  
   
  ⚫
To minimize a n-state deterministic omega-automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic
  ⚫
omega-automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc.
 
|Prerequisites=This internship targets students who:
  
|Prerequisites=This internship targets students who:
−
* have some experience in C++ programming and Unix development (experience with git would be a welcome bonus)
 +
* have some experience in C++ programming and Unix development (experience with git and emacs would be a welcome bonus)
 
* like to write clean and useful code (Spot is an open-source library used by other projects)
  
* like to write clean and useful code (Spot is an open-source library used by other projects)
 
* like to optimize
  
* like to optimize
 
* would like do get familiar with the amazing world of SAT-solvers and Büchi automata.
  
* would like do get familiar with the amazing world of SAT-solvers and Büchi automata.
−  
 
|Objectives=Presently, our first implementation saves the SAT problem as a huge file before calling the SAT-solver, and it does
  
|Objectives=Presently, our first implementation saves the SAT problem as a huge file before calling the SAT-solver, and it does
 
this for each iteration. The goal of this internship is to improve this situation in multiple ways:
  
this for each iteration. The goal of this internship is to improve this situation in multiple ways:
 
* implement purely technical optimizations (like direct communication with the SAT solver, bypassing any temporary files)
  
* implement purely technical optimizations (like direct communication with the SAT solver, bypassing any temporary files)
−
* take advantage of feature offered by modern SAT solvers (for instance an "incremental SAT-solver" can be given new constraints after it has found a solution, without needing to restart from scratch)
 +
* take advantage of features offered by modern SAT solvers (for instance an "incremental SAT-solver" can be given new constraints after it has found a solution, without needing to restart from scratch)
−
* implement optimization to the encoding of the SAT-problem, based on structural properties of the automaton (we have some ideas)
 +
* implement optimizations to the encoding of the SAT-problem, based on structural properties of the automaton (we have some ideas)
−  
⚫
In a second, step, we would like to generalize the existing technique to non-deterministic automata, or to different
  
−
types of acceptance conditions (i.e., not Büchi).
  
−  
⚫
|References=* On the usage of a SAT-solver for minimization: https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf
  
⚫
* For the present usage of SAT-based minimization in Spot: http://spot.lip6.fr/userdoc/satmin.html
  
   
  ⚫
In a second step, we would like to generalize the existing technique to non-deterministic automata (first as input, and then as output as well).
  ⚫
|References=* On the usage of a SAT-solver for minimization: https://www.lrde.epita.fr/~adl/dl/adl/baarir.15.lpar.pdf
  ⚫
* For the present usage of SAT-based minimization in Spots: https://spot.lrde.epita.fr/satmin.html
 
|Contact=<adl at lrde . epita . fr>
  
|Contact=<adl at lrde . epita . fr>
 
|Compensation=1000 € gross/month
  
|Compensation=1000 € gross/month
  +
|Future work opportunities=This internship can easily be prolonged as a PhD thesis.
  +
|Type=Master Internship
 
|Language=en
  
|Language=en
  +
|Published=No
 
}}
  
}}

Latest revision as of 17:28, 30 November 2016

Minimization of Büchi automata using SAT-solving
Reference id

M2 2015 ADL SAT-based Minimization

Dates

5-6 months in 2015

Research field

Automata Theory

Related project

Spot

Advisor

Alexandre Duret-Lutz

General presentation of the field

The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique allows us to minimize deterministic Büchi automata using a SAT-solver; the implementation is actually not restricted to Büchi and can work with deterministic omega-automata with any acceptance conditions.

To minimize a n-state deterministic omega-automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic omega-automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc.

Prerequisites

This internship targets students who:

  • have some experience in C++ programming and Unix development (experience with git and emacs would be a welcome bonus)
  • like to write clean and useful code (Spot is an open-source library used by other projects)
  • like to optimize
  • would like do get familiar with the amazing world of SAT-solvers and Büchi automata.
Objectives

Presently, our first implementation saves the SAT problem as a huge file before calling the SAT-solver, and it does this for each iteration. The goal of this internship is to improve this situation in multiple ways:

  • implement purely technical optimizations (like direct communication with the SAT solver, bypassing any temporary files)
  • take advantage of features offered by modern SAT solvers (for instance an "incremental SAT-solver" can be given new constraints after it has found a solution, without needing to restart from scratch)
  • implement optimizations to the encoding of the SAT-problem, based on structural properties of the automaton (we have some ideas)

In a second step, we would like to generalize the existing technique to non-deterministic automata (first as input, and then as output as well).

Benefit for the candidate
References
Place LRDE: How to get to us
Compensation

1000 € gross/month

Future work opportunities

This internship can easily be prolonged as a PhD thesis.

Contact

<adl at lrde . epita . fr> <adl at lrde . epita . fr>

Retrieved from "https://www.lrde.epita.fr/index.php?title=Jobs/M2_2015_ADL_SAT-based_Minimization&oldid=99725"