Real engineering problems which can (only) be solved by SAT solvers

MSc Jan Söderberg, SystemWeaver, jan.soderberg@systemweaver.com

Introduction

There are engineering problems that can be expressed as so-called Boolean satisfiability problems, or “SAT” problems[1]). There are as well algorithms to solve such problems, i.e. to find the Boolean values (“true” or “false”, or 1 or 0) for the variables in the expression that would yield a “true” result.

A complete solution to any SAT problem can be found by transforming the input expression into the classical disjunctive normal form (DNF[2]), i.e. a set of And expressions joined by Or operations, where one solution to the problem is all variables in one of the And expressions being true.

Example: SAT = (v1 Or v2 Or v3) And (v4 Or v5) And (v6),

With the alternative tree solutions:

1. v1 = true, v2 = true, v3 = true, or
2. v4 = true, v5 = true, or
3. v6 = true

Depending on the application we may search for all, or just a single solution to the SAT problem, or to make sure there is no solution at all – which of course is the negation of the first.

Transforming a Boolean expression into the DNF form may not seem overly complex, given the exercises we have all had in elementary school: to simplify or factorize algebraic expressions, in order to derive the desired result. However, in fact, this problem belongs to the hardest class of mathematical problems, which cannot be expected to be solved at polynomial time, i.e. the time to find a solution depends on an exponential function of the number of variables! [3]

To realize that this statement of complexity is actually true, we can see that an expression of N Boolean variables will have 2^N possible combinations, i.e. the number of possible combinations, or alternative solutions to evaluate, will grow exponentially with the number of variables: Adding a new variable to the expression will double the number of solutions to evaluate.

Note that in the examples below a prefix notation is sometimes used, rather than the more common infix. The reason for this is that the format offers improved readability and clarity for large and nested expressions. Example: Or(And (Variable1, Variable2), And(Variable3, Variable4)) rather than (Variable1 And Variable2) Or (Variable3 And Variable4).

In following text we will give examples of real engineering problems that can be expressed as SAT problems.

Engineering problem #1: Fault Tree Analysis

Fault trees[4] express the logics behind individual faults in a system, leading to a top level system failure, and is a tool commonly used in the reliability or safety analysis of systems.

One problem related to fault trees is finding all sets of faults in a fault tree that results in a top-level failure, a so called (minimal) cut set, and, the likelihood of the same failure, given the likelihood of each fault.

For this problem the SAT expression is the fault tree itself, representing the logical expression of how each variable contributes to the top-level fault. Note that we usually need all solutions to the problem, i.e. all minimal cut sets, since any of these may be the most likely one.

SAT expression

Example:

‘No start of an engine’ [failure] = ‘No compression’ [fault] Or ‘No spark’ [fault] Or ‘No fuel’ [fault]

A fault expression like the one above can be extended by analyzing more closely the possible underlying faults, leading to for example the ‘No spark’ fault.

Note that under certain conditions the likelihood can easily be calculated from the original fault tree expression, using the principle that the likelihood of any event in a set of events (“Or”) is the sum of the likelihood of the individual events, and the likelihood of all events in a set of events (“And”) is the product of the likelihoods. (With the condition of all likelihoods being small))

This calculation will however yield the wrong result if there is any correlation between the events, especially if any of the variables appear more than once in the expression. On the other hand, basing the calculation on the DNF form will give the correct result.

A solution for Fault Tree Analysis (FTA), including graphical editing and inclusion of controls or requirements can be provided by SystemWeaver, as seen below. The solution also correctly calculates minimal cut sets and corresponding failure probabilities.

Figure 1 Implementation of FTA and Cut Set analysis in SystemWeaver.

Engineering problem #2: Variability consistency

Another problem is to check if a feature-based product line architecture[5],[6] in fact allows for inconsistent configurations. One such case of inconsistency is if an interface required by one of the components of the architecture is not provided by any of the other components in a given valid or allowed configuration, according to the feature set defining the configuration.

The condition for a single of the interfaces – this condition is easy to extend to cover all the interfaces – is a valid feature set according to the feature model, combined (i.e. And:ed) with the feature set providing the required interface, again combined with the negated (i.e. Not And) set of features granting the required provided interface. Note that features are usually seen as Boolean variables, so no additional or alternative representation of these is required.

Note also that since the existence of an interface is given by the existence of a component providing the interface, the condition for existence can simply be replaced by the feature condition for the existence of the that component.

SAT expression

The inconsistency condition of a single pair of ports as described above can thus be expressed as:

<Feature condition for an allowed configuration>
And
<Feature condition for the ‘require’ port>
Not And
<Feature condition for the ‘provide’ port>

If the feature conditions can all be expressed as Boolean logic expressions – which is often the case – or if additional numerical conditions can all be converted into boolean expressions as well, e.g. by replacing discrete ranges with separate Boolean variables – this problem also becomes a SAT problem.

Complete solutions to variability and Product Line Architectures can be provided by SystemWeaver.

The Variant Matrix views in SystemWeaver supports editing of variability conditions, using a grid type view:

Figure 2 Variant Matrix in SystemWeaver, facilitating selection of features of a specific configuration or variant

The underlying format of the data produced from the view is expressed as logical conditions, with the validity of a product variant depending on a feature set, like in this case the feature ‘11300 mm liftheight’:

Figure 3 The underlying features and logical expressions of these, tied to a variant

Engineering problem #3: Completeness of tests

Another problem is that of checking whether all possible combinations of required environmental conditions have been included in a set of tests, or test cases, where each condition is assumed to be encoded into a separate logic variable.

Question to be answered:
Is there (at least) any of the required conditions that is not covered by any of the combined tests or test cases?

One example of a condition is that the test shall cover both the conditions daytime and nighttime.

Mutual exclusiveness

Some conditions, like ‘Daytime’ or ‘Nighttime’ might be mutually exclusive, and cannot be applied in the same test, so that multiple permutations of conditions may be required, for additional tests. Mutual exclusiveness like this can be expressed either as Exclusive Or (XOR) conditions in the logical conditions to be satisfied, or by making one alternative implicit, for example Nighttime == Not Daytime, which works for dual alternative cases.

SAT expression

The question to be answered can be formalized into:

<Environmental condition>
And Not
Or(Test1, Test2, …, Test N)

, where each test condition is expressed as And over all its conditions, and where the omission of a condition would be expressed as Not applied to the variable of that condition.
Note that although the test condition need to follow the constraints of the environment, there is no need to repeat these conditions, since they will anyway need to be fulfilled by the environmental condition constraints.

An example, where the environmental condition is simply ‘Daytime’ (exclusive) or ‘Nighttime’, with a single test using Daytime would be:

(Daytime and Not Nighttime) Or (Not Daytime and Nighttime)
And Not
Or(And(Daytime, Not Nighttime))

, with a possible solution: Daytime = false, Nighttime = true.

In case we could express Nighttime = Not Daytime, the same expression would be simplified into:

(Daytime) Or (Not Daytime)
And Not
Or(And(Daytime))

, with the (only) solution: Daytime = false.

Note that the environmental conditions may incorporate additional constraints apart from selection of excluding conditions. Such constraints can include grouping of conditions, where sets of conditions need to be set together. For example, the condition of ‘Highway driving’ could include a number of conditions specific to highway driving. All such conditions can be translated into logical operations like And or Or. To provide better understanding of these groupings we could give them a name or annotation, like using ‘Time of Day’ to group ‘Daytime’ and ‘Nighttime’. Figure 4 below includes several such groupings. Note that the name of groupings will not be represented as logical variables, but simply as the logical operation they represent.

If we complete the test suit with a test with nighttime conditions, the expression would becom (with no possible solution:

(Daytime) Or (Not Daytime)
And Not
Or(And(Daytime, Not Daytime))

Note that in the expressions and examples above the condition for the environment is that all possible environmental conditions are covered. Still, the condition expresses the required dependence between individual variables, which, as in the examples above, may require Or conditions between individual values.

Standardization of environmental conditions

A formalism that can be used for describing complex automotive environments, fulfilling the ISO 34503:2023 standard, suggested for the development of AD and ADAS systems can be provided by SystemWeaver, as illustrated by the screen shot below.

Figure 4 Implementation of ISO 34503:2023 standard in SystemWeaver

A final note on complexity

What about the NP complexity? How can a SAT solver overcome immense levels of complexity? A problem with 50 variables would require 2exp50 alternatives to be evaluated, equal to 10¹⁵ (i.e. 1 000 000 000 000 000 possible combinations). A computer evaluating a billion combinations per second would require more than a year to complete the calculations. And any additional variable would double that time.

Actually, there are a couple of circumstances that allow SAT solvers to solve problems, with number of variables that would seem prohibitive.

Firstly, although the number of variables may be high, the individual terms of the expression, in real life cases, will not involve but a fraction of all variables, which will reduce the number of possible combinations.

Secondly, modern SAT solvers use clever algorithms: Typically, they make a clever initial guess of a solution, and then make a search for solutions, by trying alternative values for selected variables, and then back-tracking the combinational binary tree of the logical condition, until a solution is found.

For example, in an expression like And(Not Or (Not A, B), Or (B And C)), it would be natural to start the guessing with A = true, B=false, C=true, simply by counting the number of Not operations on the variables, parsing the expression from left to right. By luck, this is the single solution, as parsing from right to left would have yielded B=true, which is not a solution.

There are couple of conceivable alternatives to the state-of-the-art SAT solvers: firstly, for small problems an exhaustive search /“brute force” approach could work, where each possible combination of values is tried in turn. Secondly, in the future, the use of quantum computing could solve any problem of this type at a fixed time. But until then we need to rely on smart algorithms.

[1] SAT: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

[2] DNF: https://en.wikipedia.org/wiki/Disjunctive_normal_form

[3] NP-completeness: / https://en.wikipedia.org/wiki/NP-completeness

[4] Fault tree: https://en.wikipedia.org/wiki/Fault_tree_analysis
Note that any logical expression can be seen as a “tree” when drawn in a tree style, where the logical expressions will form branches of the tree.

[5] https://en.wikipedia.org/wiki/Product-family_engineering

[6] https://en.wikipedia.org/wiki/Feature_model