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.

BC1.1\n

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

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

The presedence of the unary and binary operations is the usual

• =>,
• ==,
• | and ^,
• &, and
• ~.

As an example, the constrained circuit

a := b & c;
b := [1,2](c,d,e);
ASSIGN a;

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

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;

ASSIGN g == AND(b,c,d), g == ODD(c,e,f);

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

• DES: des_3_1, des_4_1, des_4_2, des_5_1, des_5_2, des_5_3, des_5_4
  These circuits model known plain-text attacks on bounded rounds version of DES. Each benchmark subfamily des_r_b is parameterized by the number of rounds (r) and the number of plain tex blocks (b).
• GenFacBm
  These circuits encode factoring problems of 30-40 bits wide prime and composite numbers by using atree and braun multipliers. The circuits were generated with the genfacbm tool by Tuomo Pyhälä.
• Heljanko Concur 2001 extended
  These are circuits obtained by expressing bounded model checking problems of Petri nets as Boolean circuit satisfiability. For the technique, see the paper

  Keijo Heljanko, Bounded Reachability Checking with Process Semantics, in CONCUR 2001 - Concurrency Theory, Lecture Notes in Computer Science, 2001, Volume 2154, Springer, pages 218-232.

  The circuits were generated by using the nets and translator tool by Keijo Heljanko available at the experiments page of the paper. The archive above contains more circuits than used in the paper as the SAT solvers have evolved since 2001.

• Tommi A. Junttila and Ilkka Niemelä. Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking. In J. Lloyd et al., editors, Computational Logic - CL 2000; First International Conference, volume 1861 of Lecture Notes in Artificial Intelligence, pages 553-567, London, UK, July 2000. Springer, Berlin.
  Gzipped postscript (116 Kb) © Springer-Verlag. Bibtex Entry.