[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

A circuit file should start with the header line
where \n is the newline character. The header line is followed by the actual circuit definition by the following grammar:
circuit = (gate | assign)*

gate_def = name ';'
gate_def = name ':=' formula ';'
formula = formula '==' formula | 'EQUIV' '(' formula_list ')'
formula = formula '=>' formula | 'IMPLY' '(' formula ',' formula ')'
formula = formula '|' formula | 'OR' '(' formula_list ')'
formula = formula '&' formula | 'AND' '(' formula_list ')'
formula = formula '^' formula | 'ODD' '(' formula_list ')'
formula = 'EVEN' '(' formula_list ')'
formula = 'ITE' '(' formula ',' formula ',' formula ')'
formula = '[' int ',' int ']' '(' formula_list ')'
formula = `~` name | 'NOT' '(' name ')'
formula = name
formula = 'T' | 'F'
formula = '(' formula ')'

formula_list = formula | formula ',' formula_list

assign = 'ASSIGN' assign_list ';'
assign_list = single_assign | single_assign ',' assign_list
single_assign = name | '~' name
where int is a positive integer. 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

The operator => associates to right while the others are left associative. Note: the precedence order has changed to this on April 25, 2003. In order to avoid problems, it is therefore recommended to use parentheses and to write (a == b) => c instead of a == b => c.

The constraints ASSIGN force some gates to have a predefined value in all satisfying truth assignments. For instance, an contraint ASSIGN gate1, ~gate2, gate3; forces the truth assignments on the gates to have gate1 to evaluate to true, gate2 to false and gate3 to true.

As an example, the constrained circuit

a := b & c;
b := [1,2](c,d,e);
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;



The following benchmark families are currently available. If you have some others, please contact me.