CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

SAT-Solving in Practice, with a Tutorial Example from Supervisory Control

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Niklas Een ; Mary Sheeran (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Niklas Sörensson ; Alexey Voronov (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation)
Discrete Event Dynamic Systems (0924-6703). Vol. 19 (2009), 4, p. 495-524.
[Artikel, refereegranskad vetenskaplig]

Satisfiability solving, the problem of deciding whether the variables of a propositional formula can be assigned in such a way that the formula evaluates to true, is one of the classic problems in computer science. It is of theoretical interest because it is the canonical NP-complete problem. It is of practical interest because modern SAT-solvers can be used to solve many important and practical problems. In this tutorial paper, we show briefly how such SAT-solvers are implemented, and point to some typical applications of them. Our aim is to provide sufficient information (much of it through the reference list) to kick-start researchers from new fields wishing to apply SAT-solvers to their problems. Supervisory control theory originated within the control community and is a framework for reasoning about a plant to be controlled and a specification that the closed-loop system must fulfil. This paper aims to bridge the gap between the computer science community and the control community by illustrating how SAT-based techniques can be used to solve some supervisory control related problems.

Nyckelord: Formal verification, Boolean satisfiability problem, Model checking, Supervisory control

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2009-09-16. Senast ändrad 2016-07-01.
CPL Pubid: 98185


Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)
Institutionen för data- och informationsteknik (GU) (GU)
Institutionen för signaler och system, Automation (2005-2017)


Informations- och kommunikationsteknik
Datavetenskap (datalogi)
Teoretisk datalogi

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

Using Formal Methods for Product and Production Development -- Industrial Applications for Boolean Satisfiability Solvers

On Formal Methods for Large-Scale Product Configuration