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\nwhere \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 |
The presedence of the unary and binary operations is the usual
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);
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.
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.