SAT-solving in practice, with a tutorial example from supervisory control

DOI10.1007/S10626-009-0081-8MaRDI QIDQ843991zbMATH OpenOpenAlexFDO

Authors Koen Claessen, Niklas Eén, Mary Sheeran, Niklas Sörensson, Alexey Voronov, Knut Åkesson

Publication date 18 January 2010

Published in Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL https://research.chalmers.se/en/publication/98185

zbMATH Keywords

model checkingformal verificationsupervisory controlBoolean satisfiability problem

Mathematics Subject Classification ID

Hierarchical systems (93A13) Discrete event control/observation systems (93C65) Control/observation systems involving computers (process control, etc.) (93C83)

Recommendations

• scientific article; zbMATH DE number 5605058
• A Tutorial on Satisfiability Modulo Theories
• Propositional SAT solving
• Satisfiability: where Theory meets Practice (Invited Talk).
• scientific article; zbMATH DE number 1903342

Cites work

• scientific article; zbMATH DE number 1796153 (Why is no real title available?)
• scientific article; zbMATH DE number 1798189 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Computer Aided Verification
• Correct Hardware Design and Verification Methods
• Formal Methods in Computer-Aided Design
• Graph-Based Algorithms for Boolean Function Manipulation
• Interpolation and SAT-based model checking.
• Optimal speedup of Las Vegas algorithms
• SAT-solving in practice, with a tutorial example from supervisory control
• Supervisory Control of a Class of Discrete Event Processes
• The complexity of theorem-proving procedures

Cited in

(5)

• The possibilistic Horn non-clausal knowledge bases
• Accelerating a continuous-time analog SAT solver using GPUs
• Explaining the \texttt{cumulative} propagator
• Safe PLC Controller Implementation IEC 61131-3 Compliant based on a Simple SAT Solver: Application to Manufacturing Systems
• SAT-solving in practice, with a tutorial example from supervisory control

Describes a project that uses

Uses Software

• UMDES
• BerkMin
• Chaff
• SATO
• MiniSat

This page was built for publication: SAT-solving in practice, with a tutorial example from supervisory control

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q843991)