Download

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

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

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).