6. Relationship with previous work
The first use of SAT solvers for configuration synthesis was reported in . The Alloy  system provides a firstorder logic language (Boolean logic with individuals and quantifiers over finite domains). Statements in this language are verified by transforming these into Boolean formulas and solving these with a SAT solver. However, quantifier removal, an essential part of translating first-order logic into Boolean, can lead to very large Boolean formulas. Thus, this approach does not scale to networks of realistic size. DADC addresses this problem by preprocessing constraints to solve as much of these as possible using algorithmic methods, leaving behind a constraint that truly requires the power of an SMT solver .
The systems described in , , , are only for verifying reachability properties of a network. They are not intended for the other tasks that DADC accomplishes such as configuration synthesis and repair.
DADC has been motivated by the same problems that Software-Defined Networking has been: it is hard to conceptualize networks as a whole, configuration is hard, and networks are not programmable. SDN’s approach to solving these problems is to separate the data and control planes. The network fabric contains utterly simple networking devices with only data-plane features such as forwarding and access control. All control-plane features such as routing protocols, tunneling and encryption are abstracted away into a logically centralized controller. The controllers communicate with devices over an out-ofband network using a well-defined API such as Openflow . The biggest concern about this approach is that the powerful control-plane protocols have to be reimplemented from a centralized standpoint. If configuration is hard, programming is a lot harder!
DADC solves the first problem by allowing one to specify network-wide requirements. In other words, the conceptualization of the network as a whole is the set of requirements that it should satisfy. DADC solves the second problem by solving requirements using SMT solvers. What makes configuration hard is that requirements induce complex constraints between configuration variables and these constraints have to be manually solved. By using DADC to automatically and correctly configure existing control-plane protocols, one can fully exploit their power. For the third problem, it relies on interfaces provided by vendors, e.g., SNMP or SSH. The granularity of these interfaces is indeed coarse. However, well-defined APIs are now being offered in the new generation of components. DADC will be extended to use these in the future. A description of the application of DADC to specifying and emulating hybrid networks i.e., with both pure SDN and legacy components, is described in .
7. Overview of SAT and SMT solvers
Boolean logic is the most primitive language for modeling constraints. Examples of Boolean constraints are p∨q, p∧q, ¬p, p כq where p,q are propositional variables. The satisfiability problem (SAT) is to find values of propositional variables so a given constraint becomes true. For example, p∧q has only one solution, p=t,q=t, whereas p∨q has three solutions: p=t, q=t; p=t,q=f; p=f,q=t. Even though SAT is NP-complete, modern solvers  can often solve millions of Boolean constraints in millions of variables in seconds. The techniques behind these solvers were pioneered by Professor Sharad Malik, one of our coauthors. If a constraint is unsolvable, SAT solvers output an unsat-core, a typically small part of the constraint that is itself unsatisfiable. An unsat-core can be taken to be the “root-cause” of unsatisfiability. For example, the constraint p כq∧p∧¬q∧u∧v∧w∧x ∧y∧z has unsat core p⊃q∧p∧¬q. The variables u,v,w,x,y,z do not contribute to unsatisfiability.
However, Boolean logic is too low-level a language for modeling network constraints. We need to be able to talk about things like routers, interfaces, addresses and relationships between these. While these things and relationships can, in principle, be expressed in Boolean logic, a much more expressive option is to use the languages offered by Satisfiability Modulo Theories (SMT) solvers such as Z3 , CVC4  and Yices . These combine SAT solvers with domain-specific ones. Three domains, and their solvers, used in DADC are EUF (Equality of Unintepreted Functions), linear arithmetic and bitvector logic. EUF can be used to model data structures.