Interval algebra is used to describe relationships between time intervals over a time axis. Constraints are placed between each time interval so that when boolean expressions are constructed, they can be validated with the help of a SAT solver.

There are three main input data structures and some algorithms that allow for the generation of the boolean clauses that describe the constraints between all the time intervals, and they'll be described in the two following sections.

All the classes and methods can be found inside the allen/input module, so every reference to Python files will be relative to that.

Since the file format of the input files is briefly described with EBNF, I'll introduce some basic BNF that can be used to understand the rest of the specifications (I'm using the format as specified in here):

ws := ? any ws character ?;
nl := ? newline character ?;
relationship :=
    "<" | ">" | "m" | "mi" | "o" | "oi" | "s" |
    "si" | "d" | "di" | "f" | "fi" | "=";
relationships_list := "(", ws, {relationship, ws}, ")";

The first data structure is the inverse relationships table, in particular found in this repository under data/inverse_relationships_table.txt. It's quite small and its only purpose is to describe, given a specific relationship between two time intervals t1 and t2, what would the relationship be if the time intervals were actually the opposite, that is, it specifies the relationship that would be present between t2 and t1. The order in which we define the relationships between two or more time intervals matters, since the time axis is where the intervals reside. The table has a simple structure and is defined by a number of rows (in particular 13 rows since all the possible relationship types are actually 13) where each row contains first the normal relationship (that we defined before as being from t1 to t2), a double colon and the inverse relationship (that we defined before as being, this time, from t2 to t1).

The function read_inverse_relationships_table() inside inverse_relationships_table.py module provides a quick way to load all the data inside a practical data structure defined by the InverseRelationshipsTable class. This class exactly mirrors the contents of the file with a list-based data structure where each item is a tuple.

Each line can briefly be described using BNF as:

line := relationship, ws, "::", ws, relationship, nl;

The second data structure is the ternary constraints table. Let's say that we take into account the existence of three time intervals, called t1, t2 and t3. We also specify that the relationship between t1 and t2 is r_t1t2 and that the relationship between t2 and t3 is r_t2t3, then, because of Allen's interval algebra, only a few select relationships between t1 and t3 will actually make sense, from the whole set. This table thus defines, for a given pair of relationships r_t1t2 and r_t2t3, what's the set of possible relationships that can be found between t1 and t3 and we could call that r_t1t3.

As with the previous structure, the function read_ternary_constraints_table() inside ternary_constraints_table.py quickly reads the table from the given file path and, as before, returns a data structure that exactly mirrors the contents of the file. In particular, the TernaryConstraintsTable is the class instance that is returned by the function. The table contains a series of lines where each line is composed by the first two relationships r_t1t2 and r_t2t3 separated by a single colon and then a double colon precedes a list enclosed by round brackets of all the possible r_t1t3 relationships. This table can be found under this repository in the data/ternary_constraints_table.txt file.

Each line can briefly be described using BNF as:

line := relationship, ws, ":", ws, relationship, ws, "::", ws, relationships_list, nl;

The third and last data structure is the list of time intervals groups. For each input file in question, many groups can be contained inside it. A single group is defined as being a list of relationships between a well known number of time intervals, where each pair of time intervals might be related by one or multiple relationships. An example of time intervals groups can be found inside the data/time_intervals folder, with various kinds of data sizes.

The function read_time_intervals_table() reads all the time intervals groups inside the input file and returns a list of TimeIntervalsGroup instances where each one of them represents the exact data provided by the group. As usual, the file is line-based but the groups have a header that indicates the number of time intervals, followed by some lines that define the relationships between two time intervals (each time interval is referenced by a number from zero up to one less than the total number of time intervals written in the header) and a final line containing a dot that marks the end of the current group.

Each group can briefly be described with BNF as:

intervals_count := ? any positive integer number ?;
time_interval := ? any non-negative integer number less than the intervals count ?;

header := intervals_count, nl;
line := time_interval, ws, time_interval, ws, "::", relationships_list, nl;
end := ".", nl;
group := header, {line}, end;

Given the input data, some algorithms are used to generate boolean clauses whose satisfiability will be later checked by a SAT solver. In particular, we're always using:

• at least one,
• at most one,
• inverse implication

and the user gets to choose between:

• ternary implication, or
• expression reference.

All the above algorithms will now be explained in the following sections. Before that, a brief explanation on what a boolean clause is. Generally, in the context of boolean SAT solvers, the input data is a list of clauses. Each clause is essentially a boolean expression composed by subsequent OR operators on individual literals, where each literal can be plain or negated. Thus, a single boolean clause can be for example x1 x2 -x3 whose actual meaning is x1 OR x2 OR (NOT x3). In our case, each literal can either represent a relationship between two time intervals (thus described by a triple: t1, t2, and r_t1t2) or it can be referring to an expression

I will also refer to the configuration, indicating the current time intervals group taken into account and whose algorithms are being applied on.

Considering the fact that most of the time, in the time intervals group, for each set of relationships that can be found between a generic t1 and t2, the size of said set is bigger than one (in other words, it specifies that there can be more than one relationship between t1 and t2), we want to generate a clause that expresses the fact that at least one of those relationships has to be found in the given configuration. We express that constraint by ORing together all the literals into a single clause, where for each clause we work with time intervals t1 and t2 and we compose literals by using, in turn, every relationship that's possible between t1 and t2.

To give an example, let's say that between time intervals 3 and 4 there can only be relationships before (<), equal (=) or overlapping (o). We then generate the at least one clause by using three literals, one for each relationship and all of them using the same pair of time intervals. In the following code block, the resulting clause is explained:

Line describing the relationships in the time intervals group:
    3 4 :: ( < = o )
    
Literals as defined by what's required by the algorithm:
    l1: relationship < between time intervals 3 and 4
    l2: relationship = between time intervals 3 and 4
    l3: relationship o between time intervals 3 and 4
    
Resulting clauses:
    l1 OR l2 OR l3

It's pretty clear that for the clause to be true, it's enough to have one of those literals to be true, that is, to have one of the three possible relationships to actually be the one specified in the given configuration.

This algorithm is pretty similar to the at least one counterpart, but instead specifies the exact opposite: between two time intervals that can be related by more than one possible relationship, generate a clause that makes sure at most one of those relationships is the one given in the configuration and not more.

To do this, we construct not one but a series of clauses each indicating that it's not possible for two relationships to be specified in the configuration at the same time. Let's say that we have two time intervals 3 and 4, as before and that the relationships between them are before (<), equal (=) or overlapping (o). We know that it's not possible for the configuration to have both 3 and 4 related by relationships before and equal, or by before and overlapping or again by equal and overlapping. We construct a boolean expression that's an AND of two negated literals, each one indicating that between 3 and 4 there's a different relationship. We do that with all the possible combinations of relationships.

Since the resulting clauses aren't in the format required by the SAT solver that needs all literals ORed together to form a single clause, we need to take advantage of the properties of boolean algebra and use De Morgan's theorem to swap the AND of the two negated literals with the same two non-negated literals ORed together. The code block provides an example:

Generic boolean expression:
    !x_{t1, t2, r1} & !x_{t1, t2, r2}

Line describing the relationships in the time intervals group:
    3 4 :: ( < = o )
    
Literals as defined by what's required by the algorithm:
    l1: relationship < between time intervals 3 and 4
    l2: relationship = between time intervals 3 and 4
    l3: relationship o between time intervals 3 and 4
    
Resulting clauses:
    -l1 OR -l2
    -l1 OR -l3
    -l2 OR -l3

This is quite simpler than the rest of the algorithms as it expresses the fact that, given time intervals t1 and t2, if the relationship between them is something, then it should also be true that if we swap the order of the time intervals, the relationship between them should be the exact inverse of the previous relationship. Here too we take advantage of the propositional logic's rules to change an implication into a valid boolean expression that can be used in a SAT solver.

Generic boolean expression:
    x_{t1, t2, r} => x_{t2, t1, inverse_of(r)} which is
    !x_{t1, t2, r} | x_{t2, t1, inverse_of(r)}

Line describing the relationships in the time intervals group:
    3 4 :: ( < = o )
    
Literals as defined by what's required by the algorithm:
    l1: relationship < between time intervals 3 and 4
    l2: relationship > between time intervals 4 and 3 (the inverse of 3 and 4)
    
Resulting clauses:
    -l1 OR l2

This is one of the two algorithms that can be used to complete the list of clauses to be passed to the SAT solver. It puts into practice (actually, boolean expressions) what has been described in the section that describes the data structure. The below code block represents an example:

Generic boolean expression:
    x_{t1, t2, r1} & x_{t2, t3, r2} => x_{t1, t3, r3} which is
    !(x_{t1, t2, r1} & x_{t2, t3, r2}) | x_{t1, t3, r3} which is
    !x_{t1, t2, r1} | !x_{t2, t3, r2} | x_{t1, t3, r3}

Lines describing the relationships in the time intervals group:
    3 4 :: ( > )
    4 5 :: ( s fi )
    
Lines needed in the ternary constraints table:
    > : s :: ( > d f mi oi )
    > : fi :: ( > )
    
Literals as defined by what's required by the algorithm:
    l1: relationship > between time intervals 3 and 4
    l2: relationship s between time intervals 4 and 5
    l3: relationship fi between time intervals 4 and 5
    
    l4: relationship > between time intervals 3 and 5
    l5: relationship d between time intervals 3 and 5
    l6: relationship f between time intervals 3 and 5
    l7: relationship mi between time intervals 3 and 5
    l8: relationship oi between time intervals 3 and 5
    
    l9: relationship > between time intervals 3 and 5
    
Resulting clauses:
    -l1 OR -l2 OR l4 OR l5 OR l6 OR l7 OR l8
    -l1 OR -l3 OR l9

To be done.

Once all the required clauses have been generated, the allen/output module will take care of everything that's required to generate proper SAT input. Essentially, each literal for every clause will be identified by a single positive integer number thus the number_dict.py provides facilities to uniquely identify literals across clauses.

When two literals are found in two different clauses, the same integer number is used. Each clause is written by separating each contained literal with a space, eventually negating the integer number that represents the literal if it's negated and adding a zero at the end of the line to mark the end of the clause. Subsequent clauses are written in a separate line.