Page 9 - Sirius_Annual_Report_2021

Silvia Lizeth Tapia Ta
Rudolf Schlatte
It is the problem of deciding the satisfiability5 of a quantifier -free first-order formula with respect to some decidable theories. For example, for the theory of linear arithmetic over the rational (LRA), a SMT(LRA) is the problem of checking the satisfiability of a formula φ consisting in atomic propo- sitions A1, A2, A3, ... and linear-arithmetic constraints over rational variables like
(2.1x_1 - 3.4x_2 +3.2x_3 ≤ 4.2)
combined by means of Boolean operators ¬,φ,φ,φ,φ. An LRA-interpretation μ is a function which assigns truth values to Boolean atoms and rational values to numerical variables. μ satisfies in the theory LRA if and only if μ makes the formula φ evaluate to true. φ is LRA-satisfiable if and only of it has at least one LRA-interpretation μ that satisfies it. The satisfiability of a SMT formula depends on the theory
it based on. For example, the qualifier-free formula
((y≤4x)⋀((y>0)⋀(y≤-4x+4)))⋀((x≥1)⋀(y≤2))⋀((x<1)⋀(y=(5x-4)))
is satisfiable over the theory of linear arithmetic over rational (possible solution: {x=0.87,y=0.35}); but is unsatisfiable over the theory of linear arithmetic over integers.
Many popular problems can be solved by SAT/SMT-based approaches, such as: travelling salesman problem, graph colouring problem, sudoku, knight tour, and dominating set. There are many highly efficient SAT/SMT that can solve many problem instances with hundreds of thousands of variables and millions of constraints. Some state-of-the-art solvers are Z3, Yices, MathSAT, MaxSAT.
SAT/SMT methods are being used in the integrated digi- tal planning demonstration. The work mainly focuses on applying SAT/SMT-based automated reasoning techniques to model, verify, and optimise the vessel schedules and cargo transport to improve the workflow of the planners, in a use case provided by Equinor.
SMOL - Semantic Micro Object Language
SMOL is a framework that integrates knowledge bases with object-oriented programming languages which uses Semantic Web technologies. The integration of semantic technologies directly into a programming language is used to ensure the correct usage of semantic meaning in the program through type systems and other tools. Through the clean separation between data modelling and program- ming, SMOL integrates smoothly with industry-strength frameworks and builds on the expertise already present for existing semantic technologies, such as SPARQL, OWL or RDF.
• Data export of simulation results into other tools
• Model exploration using formal analysis tools
Highlights of 2021
In 2021, the research group has developed a 90-minute ABS tutorial3, presented at the DisCoTec 2021 conference. The tutorial focused on the ABS language, its approach to modelling, and on tool usage. The ABS toolchain and an accompanying paper is currently being reviewed have been accepted for publication in the Elsevier journal Science of Computer Programming.
ABS is being used in the integrated digital planning4 and digital twins at SIRIUS, as shown in Figure 1, in collaboration with Equinor.
SAT/SMT - Satisfiability of formulas
Satisfiability Problem (SAT) is the problem of deciding the satisfiability5 of a Boolean formula. A Boolean formula is satisfiable if there exists an interpretation that assigns truth values to the Boolean atoms such that the formula evaluates to true. For example, the formula
((a ¬b) ⋀ (¬a c))
is satisfiable, possible solutions are: {¬a,¬b,¬c}, and {a,¬- b,c}; while the formula
((a ¬b) ⋀
(¬a b) (a
¬b))
is unsatisfiable.
Satisfiability Modulo Theories (SMT) is the extension of SAT.
SIRIUS ANNUAL REPORT 2021 | 9