[File format] [Tools] [Benchmarks] [References]

Author: Tommi Junttila

For Boolean circuits, see standard textbooks on logic and/or computational complexity. Here we use a class of Boolean circuits which have, in addition to the standard and, or, not, variable and constant gates, also (i) n-ary parity and equivalence gates, (ii) if-then-else gates, and (iii) threshold gates (true iff atleast l and at most u of the child gates are true). Although these gates can be expressed with the normal and/or/not gates, it is convenient to have such gates.

Recall that a Boolean circuit has 2^n consistent truth assignments on the gates, where n is the number of input (variable) gates in the circuit. Therefore, we are rather interested in constrained Boolean circuits, which are Boolean circuits with the constraint that some of the gates must evaluate to true/false. The problem of solving whether a constrained Boolean circuit has any consistent truth assignments obeying the constraints (that is, whether the constrained circuit is satisfiable) is obviously an NP-complete problem.

## File Format

`BC1.1\n`
where \n is the newline character. The header line is followed by the actual circuit definition by the following context-free grammar:
 circuit → statement | statement circuit statement → name ; | name := formula ; | ASSIGN formulaList ; formula → formula == formula | EQUIV ( formulaList ) | formula => formula | IMPLY ( formula , formula ) | formula | formula | OR ( formulaList ) | formula & formula | AND ( formulaList ) | formula ^ formula | ODD ( formulaList ) | EVEN ( formulaList ) | ITE ( formula , formula , formula ) | [ int , int ] ( formulaList ) | ! formula | NOT ( formula ) | name | F | T | ( formula ) formulaList → formula | formula , formulaList
where
• int is a positive integer, and
• name is a string of ASCII letters, underscores, dots or apostrophes, starting with an ASCII letter or underscore. Names starting with an underscore are usually ignored in the output of the tools, e.g. their values are not given in satisfying truth assignments.
The meaning of the semicolon-separated definition and ASSIGN statements is as follows:
• A definition statement foobar; defines an input gate named "foobar".
• A definition statement foobar := f; defines a gate whose value is defined by the formula f.
• A formula EQUIV(f1,...fn) evaluates to true iff all f1,...,fn evaluate to a same value. f1 == f2 is equivalent to EQUIV(f1,f2) and corresponds to the usual binary bi-implication (equivalence) operation.
• A formula IMPLY(f1,f2) evaluates to true iff f1 evaluates to false or f2 evaluates to true and f2 evaluates to true. f1 => f2 is equivalent to IMPLY(f1,f2) and corresponds to the usual binary implication operation.
• A formula OR(f1,...,fn) evaluates to true iff at least one of f1,...,fn evaluates to true. f1 | f2 is equivalent to OR(f1,f2) and corresponds to the usual binary inclusive-or operation.
• A formula AND(f1,...,fn) evaluates to true iff all f1,...,fn evaluate to true. f1 & f2 is equivalent to AND(f1,f2) and corresponds to the usual binary and operation.
• A formula ODD(f1,...fn) evaluates to true iff an odd number of f1,...,fn evaluate to true. f1 ^ f2 is equivalent to ODD(f1,f2) and corresponds to the usual binary exclusive-or operation.
• A formula EVEN(f1,...fn) evaluates to true iff an even number of f1,...,fn evaluate to true.
• A formula ITE(i,t,e) evaluates to true iff i and t are true or i is false and e is true. This is the normal 'if i then t else e' operation.
• A formula [l,u](f1,...fn) evaluates to true iff at least l and at most u of f1,...,fn evaluate to true.
• A formula NOT(f1) evaluates to true iff f1 evaluates to false. !f1 is equivalent to NOT(f1) and corresponds to the usual unary negation operation.
• A formula foobar evaluates to true iff the gate foobar evaluates to true.
• A formula T (F) always evaluates to true (false).
• A formula (f1) is equivalent to the formula f1.
• An ASSIGN statement ASSIGN f1, f2, ..., fn; declares that all the formulas f1,...,fn must evaluate to true.
For each gate name g there should be at most one line of form g; or g := .... That is, each gate is defined at most once. Gates that are not defined in this way but that are mentioned in the description are implicitly defined to be input gates.

The presedence of the unary and binary operations is the usual

• =>,
• ==,
• | and ^,
• &, and
• ~.
The operator => associates to right while the others are left associative.

As an example, the constrained circuit

```a := b & c;
b := [1,2](c,d,e);
ASSIGN a;
```
has the input gates c,d,e, while the gate a is forced to evaluate to true. There are three satisfying truth assignments for this circuit: (i) c is true and d,e are false, (ii) c and d are true, e is false, or (ii) c and e are true, d is false.

The circuit defined should be acyclic, meaning that the definitions of gates may not depend cyclicly on each other. For instance,

```a := AND(b,~e,f);
b := [1,2](t1,t2,t3) & (a | e);
```
is not a valid Boolean circuit since the definition of a depends on b and the definition of b depends on a.

Note that Boolean formulae can be easily expressed with circuits: For a formula f = ..., simply define one gate f := .... To check whether the formula is satisfiable, force f to true by ASSIGN f; and check whether the circuit is satisfiable.

Although only one definition of form g := ... is allowed for each gate name g, it is easy to force g to be equivalent to other formulae, too. For instance, to have g equal to both AND(b,c,d) and ODD(c,e,f), define

```g1 := g == AND(b,c,d);
g2 := g == ODD(c,e,f);
ASSIGN g1, g2;
```
or simply
```ASSIGN g == AND(b,c,d), g == ODD(c,e,f);
```

## Tools

• BC package version 0.40, released in April 2015. This package includes:
• The bc2cnf tool translating circuits into equi-satisfiable DIMACS CNF formulae.
• Boolean circuit front-ends for the MiniSat and ZChaff SAT solvers. These solvers are not included in the package but you have to download them from their home pages.
• The bc2iscas89 tool translating circuits into ISCAS89 format.
• Translators between the Boolean circuit format above and the non-CNF DIMACS format.
The tools also support the previous version 1.0 of the circuit file format.

• The version 0.38 of the BCSat tool is available as statically linked Linux binaries.

BCSat is an implementation of a tableau method for Boolean circuit satisfiability checking [Junttila and Niemelä 2000].

A translator from old BCSat format to the current one is available here.