# Download¶

The most recent version of the tool (1.04, Janyary 2018) can be downloaded here:

`bddsolve-source-1.04.zip`

The source code.

The previous version (1.03, September 2011) is still available here:

`bddsolve-windows-32bit-1.03.zip`

A Windows 32 bit build.`bddsolve-windows-64bit-1.03.zip`

A Windows 64 bit build.`bddsolve-linux-32bit-1.03.zip`

A Linux 32 bit build.`bddsolve-linux-64bit-1.03.zip`

A Linux 64 bit build.`bddsolve-source-1.03.zip`

The source code.

It’s also available as a FreeBSD Port: http://www.freshports.org/science/bddsolve

# Running Bddsolve¶

Get an overview of all available options:

bddsolve --help

Run the tool with input file.b

bddsolve file.b

The BDD package Buddy has two memory related options that can be set using the
command line options `-n`

and `-c`

.
If these numbers are chosen too small, the program may spend a lot of time
garbage collecting. Note that there is an upperbound to the number of nodes
that fits in memory.

-n [ --node-number ] arg (=1000000) node number of the bdd package (Buddy) -c [ --cache-size ] arg (=10000) cache size of the bdd package (Buddy)

The Buddy documentation recommends the following values for these parameters:

problem size | node number | cache size |
---|---|---|

small | 10000 | 1000 |

medium | 100000 | 10000 |

large | 1000000 | variable |

Finally there is a parameter `-s`

that has only effect for reachability problems.
When it is set to true, the reach algorithm will stop as soon as a solution
has been found.

-s [ --stop-at-solution ] arg (=0) stop the algorithm as soon as a solution is found

# BDD issues¶

When the available memory is not sufficient, the Buddy package ends with an out of memory message. In such cases, one can try to increase the number of nodes and cache size parameters. If this still doesn’t help, then the only solution is to find a better encoding of the problem.

Note

The order of the variables in the BDD is the same as the order of the variables specified
by the user in the `:variables`

section.

The order of the variables used as the order for the BDD representation may have a great influence on the efficiency of the program. So it is important to carefully consider the order of the variables.

# Satisfiability problems¶

The program satbdd receives an arbitrary formula in propositional logic as its input, and yields as its output whether it is satisfiable. This is done by computing the ROBDD of the formula by means of the BDD package Buddy. In case the formula is satisfiable also the following information is provided:

- the size of the corresponding ROBDD,
- the total number of satisfying assignments, and
- the values for one of these satisfying assignments (if it exists).

The input consists of

Field | Meaning |
---|---|

:logic | The problem type (SAT) |

:variables | The boolean variables involved. |

:formula | The considered formula. |

# Reachability problems¶

Given a set of initial states, a transition relation and a set of final states, the program reach can establish how many of these final states are reachable from the given initial states. This is done by consecutively computing the sets B0, B1, B2, ..., where Bi is the set of states reachable from the initial states in at most i steps. This process stops as soon as Bi = Bi+1. In that case Bi represents all reachable states, which will be intersected by the given set of final states. All these sets are represented by ROBDDs, and all computations are done by means of the BDD package Buddy. For the relevant sets of states the program yields both the size and the number of nodes of the ROBDD representing it.

The set of initial states, the transition relation and the set of final states are all given by formulas in propositional logic.

A state can be considered as a map π from the variables to {false, true} a formula Φ defines the set of states π for which evaluating Φ in π yields true. For instance, in this way the set consisting of the single state π satisfying π(si) = true for i = 1, 2, 3, ... may be represented by the formula (and s1 s2 s3).

In this representation *and* corresponds to intersection and or corresponds to union of sets.
Describing the transition relation is slightly more involved then describing just sets of
states. A transition relation is not a set of states, but a set of state transitions, where a state
transition is a pair of states. In representing this by a formula two kinds of variables occur:
the starting point of such a transition and the end point of the transition. This distinction
is made by adding a suffix to the variable name: for the start states the variable names are
followed by the symbol 0, for the end states the variable names are followed by the symbol
1. A formula ΦT in this double set of variables describes the following set of transitions:

there is a transition from π0 to π1 if and only if the formula ΦT yields the value true if for every i0 the value π0(i) is evaluated, and for every i1 the value π1(i) is evaluated.

As an example, consider the following program fragment

if a then b := c

over the four variables a, b, c, d. The transition relation corresponding to this program fragment can be represented in this way by

(a0 ↔ a1) /\ (c0 ↔ c1) /\ (d0 ↔ d1) /\ (a0 → (b1 ↔ c0)) /\ (¬a0 → (b0 ↔ b1))

In the given format this may be represented as

(and (iff a0 a1) (iff c0 c1) (iff d0 d1) (implies a0 (iff b1 c0)) (implies (not a0) (iff b0 b1)) )

In order to be able to use the program reach yourself it is important to understand such an example in detail, so we give some more explanation. The variable a0 represents the original value of the variable a, and a1 the new value. The conjunct a0 ↔ a1 describes that in the given program fragment the value of the variable a does not change. Similarly c0 ↔ c1 and d0 ↔ d1 describe that the values of c and d do not change. The conjunct a0 → (b1 ↔ c0) describes that if the original value of a is true, then after execution of the program fragment the value of b is equal to the original value of c. Finally, the conjunct ¬a0 → (b0 ↔ b1) describes that the value of b does not change in case the original value of a is not true. In total this describes 16 possible transitions: for every of the 16 possible original states exactly one transition is allowed.

The input consists of

Field | Meaning |
---|---|

:logic | The problem type (REACH) |

:variables | The boolean variables involved. |

:initial_state | A formula representing the initial states. |

:transition_relation | A formula representing the transition relation. |

:final_state | A formula representing the final states. |

# Examples¶

The SAT problem below

(benchmark sat :logic SAT :variables(a[0] a[1]) :formula (and a[0] a[1]) )

results in the following output:

bddsolve parameters: formula file: sat.b bdd node number: 1000000 bdd cache size: 10000 stop at solution: no benchmark: sat.txt logic: SAT notes: variables: a[0] a[1] number of variables : 2 number of nodes : 2 number of validations : 1 0 seconds elapsed for solving sat problem validation: 11

The validation 11 denotes that (a[0], a[1]) = (true, true) is a satisfying assignment.

The reach program below

(benchmark reach :logic REACH :variables (a b c d) :initial_state (and a b c d) :transition_relation (or (or (and (iff a0 b1) (iff a1 b0) (and (iff c0 c1) (iff d0 d1))) (and (iff b0 c1) (iff b1 c0) (and (iff a0 a1) (iff d0 d1))) (and (iff c0 d1) (iff c1 d0) (and (iff a0 a1) (iff b0 b1))) ) (and (and b0 c0 (not a1)) (and (iff b0 b1) (iff c0 c1) (iff d0 d1)) ) (and (and (not (or d0 c0)) (iff c1 (or a0 b0))) (and (iff a0 a1) (iff b0 b1) (iff d0 d1)) ) ) :final_state (and (not a) (not b) (not c) (not d)) )

results in the following output:

bddsolve parameters: formula file: reach.b bdd node number: 1000000 bdd cache size: 10000 stop at solution: no benchmark: reach logic: REACH notes: variables: a b c d ------------------------------------------------ - reach algorithm - ------------------------------------------------ iteration bdd size # reachable states 0 4 1 1 3 2 2 4 3 3 5 4 4 6 5 5 7 6 6 6 8 7 6 11 number of possible transitions : 43 number of reachable final states : 0 0 seconds elapsed for solving reach problem 0 seconds elapsed for backtracking solution REACH FAILED

After 7 iterations no new states are found. The final state can not be reached.

# Syntax¶

The syntax of bddsolve closely resembles the benchmark language of the
SMT-LIB Standard, see
The SMT-LIB Standard: Version 1.2.
The most important difference is the definition of *an_formula*.

N.B. In particular, note that integers are not supported.

simple_identifier ::= a sequence of letters, digits, dots (.), single quotes (’), and underscores ( ), starting with a letter user_value_content ::= any sequence of printable characters where every occurrence of braces ({ }) is preceded by a backslash ( \ ) user_value ::= '{' user_value_content '}' numeral ::= '0' | a non-empty sequence of digits not starting with 0 indexed_identifier ::= simple_identifier '[' numeral (':' numeral)* ']' identifier ::= indexed_identifier | simple_identifier var ::= '?' simple_identifier fvar ::= '$' simple_identifier attribute ::= ':' simple_identifier annotation ::= attribute | attribute user_value prop_atom ::= "true" | "false" | fvar | identifier an_atom ::= prop_atom | '(' prop_atom annotation+ ')' not_clause ::= '(' "not" an_formula annotation* ')' implies_clause ::= '(' "implies" an_formula an_formula annotation* ')' if_then_else_clause ::= '(' "if_then_else" an_formula an_formula an_formula annotation* ')' and_clause ::= '(' "and" an_formula an_formula* annotation* ')' or_clause ::= '(' "or" an_formula an_formula* annotation* ')' xor_clause ::= '(' "xor" an_formula an_formula* annotation* ')' iff_clause ::= '(' "iff" an_formula an_formula annotation* ')' an_formula ::= not_clause | implies_clause | if_then_else_clause | and_clause | or_clause | xor_clause | iff_clause | an_atom //--- Theories ---// string_content ::= any sequence of printable characters where every occurrence of double quotes (") is preceded by a backslash ( \ ) string ::= '"' string_content '"' //--- Logics ---// logic_name ::= identifier //--- Benchmarks ---// bench_name ::= identifier bench_attribute ::= ":logic" logic_name | ":variables" '(' (fvar | identifier)+ ')' | ":formula" an_formula | ":initial_state" an_formula | ":transition_relation" an_formula | ":final_state" an_formula | ":notes" string | annotation benchmark ::= '(' "benchmark" bench_name bench_attribute+ ')'

# Contact¶

If you encounter issues with the software, please contact J.W.Wesselink<at>tue<dot>nl.

# Known issues¶

- The error messages of the parser don’t always give a hint about what went wrong.

# Changelog¶

version 1.0.4 (17/01/2018)

- Applied a fix for compilation with clang 6, supplied by Ed Schouten.

version 1.0.3 (08/09/2011)

- Variables are printed in the same order as they were specified by the user.
- The grammar has been pruned, such that all productions are actually used.
- 64 bit executables have been added.

version 1.0.2 (11/05/2010)

- Improved error messages of the parser.

version 1.0.1 (03/09/2010)

- Added handling of comments (everything on a line after ‘;’ is ignored).