A DPLL(T) Framework for Verifying Deep Neural Networks
Deep Neural Networks (DNNs) have emerged as an effective approach to tackling
real-world problems. However, like human-written software, DNNs can have bugs
and can be attacked. To address this, research has explored a wide-range of
algorithmic approaches to verify DNN behavior. In this work, we introduce
NeuralSAT, a new verification approach that adapts the widely-used DPLL(T)
algorithm used in modern SMT solvers. A key feature of SMT solvers is the use
of conflict clause learning and search restart to scale verification. Unlike
prior DNN verification approaches, NeuralSAT combines an abstraction-based
deductive theory solver with clause learning and an evaluation clearly
demonstrates the benefits of the approach on a set of challenging verification
benchmarks.
Hai Duong, ThanhVu Nguyen, Matthew Dwyer
# A DPLL(T) Framework for Verifying Deep Neural Networks

###### Abstract.

Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, automatically-generated DNNs can have bugs and be attacked. This thus attracts many recent interests in developing effective and scalable DNN verification techniques and tools. In this work, we introduce a NeuralSAT, a new constraint solving approach to DNN verification. The design of NeuralSAT follows the DPLL(T) algorithm used modern SMT solving, which includes (conflict) clause learning, abstraction, and theory solving, and thus NeuralSAT can be considered as an SMT framework for DNNs. Preliminary results show that the NeuralSAT prototype is competitive to the state-of-the-art. We hope, with proper optimization and engineering, NeuralSAT will carry the power and success of modern SAT/SMT solvers to DNN verification. NeuralSAT is available from: [https://github.com/dynaroars/neuralsat](https://github.com/dynaroars/neuralsat)

deep neural network verification, clause learning, abstraction, constraint solving, SAT/SMT solving

## 1. Introduction

Deep Neural Networks (DNNs) have emerged as an effective approach for solving challenging real-world problems. Among many others, they have been used for image recognition (He et al., 2016; Krizhevsky et al., 2012), autonomous driving (Rao and Frtunikj, 2018; Salay et al., 2020), airplane collision control (Julian et al., 2016), power grid control (Siano et al., 2012), fake news detection (Thota et al., 2018), drug synthesis and discovery (Grebner et al., 2021), and COVID-19 detection and diagnosis (Khan et al., 2020; Ozturk et al., 2020).

However, just like traditional software, DNNs can have "bugs", e.g., producing unexpected results on inputs that are different from those in training data, and be attacked, e.g., small perturbations to the inputs by a malicious adversary or even sensorial imperfections result in misclassification (Isac et al., 2022; Ren et al., 2020; Yang et al., 2022; Zhang et al., 2019; Zugner et al., 2018). These issues, which have been observed in many DNNs (Goodfellow et al., 2014; Szegedy et al., 2014) and demonstrated in the real world (Eykholt et al., 2018), naturally raise the question of how DNNs should be tested, validated, and ultimately _verified_ to meet the requirements of relevant robustness or safety standards (Huang et al., 2020; Katz et al., 2017).

To address this question, researchers have developed a variety of techniques and tools to verify DNNs (e.g., (Huang et al., 2017; Katz et al., 2022, 2019; Liu et al., 2021; Muller et al., 2021; Urban and Mine, 2021; Wang et al., 2021)). Constraint-based approaches (Ehlers, 2017; Huang et al., 2017; Katz et al., 2017) aim to both correctly prove and disprove properties, but do not scale to large networks. In contrast, abstraction-based approaches (Muller et al., 2021; Singh et al., 2018, 2019; Wang et al., 2018, 2021) scale much better, but while modern abstraction verification tools can often refine their abstractions to avoid returning spurious counterexamples they are incomplete.

The problem of verifying non-trivial properties of DNNs with piecewise linear activation functions, such as "ReLU", has been shown to be reducible (Katz et al., 2017) from the classical satisfiability (SAT) problem (Cook, 1971). Despite this complexity, the ability of satisfiability modulo theories (SMT) solvers to scale to large formulae encoding real-world verification problems (Kroening and Strichman, 2016) suggests that a similar approaches might be effective for DNN verification. However, the constraint-based DNN verifiers developed to date (Ehlers, 2017; Katz et al., 2017, 2022, 2019) are not among the state-of-the-art as determined by DNN verification competitions (Bak et al., 2021; Muller et al., 2022).

Techniques like Planet(Ehlers, 2017) and Reluplex(Katz et al., 2017, 2022) demonstrated how the semantics of a trained DNN could be encoded as a constraint in Linear Real Arithmetic (LRA) and
combined with a specification also expressed in LRA for verification. In principle, such constraints can be solved by any SMT solver equipped with an LRA _theory solver_ (T-solver). The DPLL(T) algorithm implemented by modern SMT solvers works by moving back and forth between solving an abstract propositional encoding of the constraint and solving a theory-specific encoding of a constraint fragment corresponding to a partial assignment of propositional literals. The challenge in solving DNN verification constraints lies in the fact that each neuron gives rise to a disjunctive constraint to encode its non-linear behavior. In practice, this leads to a combinatorial blowup in the space of assignments the SMT solver must consider at the abstract propositional level. To resolve the exponential complexity inherent in such constraints, both Planet and Reuplex chose to _push_ the disjunctive constraints from the propositional encoding down into the theory-specific encoding of the problem, leveraging a technique referred to as splitting-on-demand (Barrett et al., 2006). This works to an extent, but it does not scale well to large DNNs (Bak et al., 2021; Muller et al., 2022). We observe that the choice to pursue an aggressive splitting-on-demand strategy sacrifices the benefit of several of the key algorithmic techniques that make SMT solvers scale - specifically _conflict-driven clause learning_(CDCL) (Bayardo Jr and Schrag, 1997; Marques Silva and Sakallah, 1996; Marques-Silva and Sakallah, 1999) and theory propagation (Kroening and Strichman, 2016).

In this paper, we revisit the design of a DPLL(T) solver for DNN verification by developing a T-solver that incorporates abstraction to (1) accelerate unsatisfiability checking of partial assignments and to (2) deduce implied literals to realize a form of theory propagation that drives clause learning to accelerate solving at the abstract propositional level. We present the **NeuralSAT** framework, which consists of a lazy, incremental LRA-solver that can be parameterized by state-of-the-art abstractions, such as LiRPA (Wang et al., 2021; Xu et al., 2020), to efficiently perform exhaustive theory propagation. In SS5, we formalize NeuralSAT and prove that it is sound and complete, and that it terminates. We then describe a NeuralSAT prototype that supports neural networks with different layer types, e.g., fully-connected, convolutional, and residual, and piecewise-linear activation functions, e.g., ReLU. In SS7 we present results demonstrating that NeuralSAT establishes the state-of-the-art in constraint-based DNN verification improving substantially on Reluplex's successor Marabou (Katz et al., 2022, 2019), which also employs abstraction and deduction, but does not exploit CDCL. Moreover, despite the fact that NeuralSAT is an early stage prototype, that is not highly optimized, it ranks second to \(\alpha-\beta\)-CROWN in solving benchmarks from the VNN-COMP competition.

The contributions of this work lie in: (i) developing a domain-specific LRA-solver that allows for the benefits of CDCL to accelerate SMT-based DNN verification,; (ii) proving the soundness, completeness, and termination of the approach; (iii) developing a prototype NeuralSAT implementation which we release as open source; and (iv) empirically demonstrating that the approach compares favorably with the state-of-the-art in terms of scalability, performance, and ability to solve DNN verification problems. Constraint-based DNN verifiers, like Planet and Reuplex, pioneered the application of formal verification to reason about neural network behavior. Subsequent work abandoned completeness in order to scale, but NeuralSAT demonstrates that by leveraging CDCL constraint-based verification can scale and, we believe, it offers a platform for further advances in DNN verification.

## 2. Background

### Satisfiability and DPLL(T)

The classical satisfiability (SAT) problem asks if a given propositional formula over Boolean variables can be satisfied (Biere et al., 2009). Given a formula \(f\), a SAT solver returns sat if it can find a satisfying assignment that maps truth values to variables of \(f\) that makes \(f\) evaluate to true, and
unsat if it cannot find any satisfying assignments. The problem is NP-Complete and research into methods for efficiently solving problem instances has been ongoing for multiple decades.

DPLL.Fig. 1 gives an overview of **DPLL**, a SAT solving technique introduced in 1961 by Davis, Putnam, Logemann, and Loveland [Davis et al. 1962]. DPLL is an iterative algorithm that takes as input a propositional formula in CNF form and (i) decides an unassigned variable and assigns it a truth value, (ii) performs Boolean constraint propagation (BCP) (also called Unit Propagation), which detects single literal clauses that either force a literal to be true in a satisfying assignment or give rise to a conflict; (iii) analyzes the conflict to backtrack to a previous decision level d1; and (iv) erases assignments at levels larger than d1 to try new assignments. These steps repeat until DPLL finds a satisfying assignment and returns sat, or decides that it cannot backtrack (d1=-1) and returns unsat.

Modern DPLL solving improves the original version with conflict-driven clause learning (**CDCL**) [Bayardo Jr and Schrag 1997; Marques Silva and Sakallah 1996; Marques-Silva and Sakallah 1999]. DPLL with CDCL can _learn new clauses_ to avoid past conflicts and backtrack more intelligently (e.g., using non-chronologically backjumping). Due to its ability to learn new clauses, CDCL can significantly reduce the search space and allow SAT solvers to scale to large problems. In the following, whenever we refer to DPLL, we mean DPLL with CDCL.

DPLL(T).DPLL(T) [Nieuwenhuis et al. 2006] extends DPLL for propositional formulae to check SMT formulae involving non-Boolean variables, e.g., real numbers and data structures such as strings, arrays, lists. DPLL(T) combines DPLL with dedicated _theory solvers_ to analyze formulae in those theories1. For example, to check a formula involving linear arithmetic over the reals (LRA), DPLL(T) may use a theory solver that uses linear programming to check the constraints in the formula. Modern DPLL(T)-based SMT solvers such as Z3 [Moura and Bjorner 2008] and CVC4 [Barrett et al. 2011] include solvers supporting a wide range of theories including linear arithmetic, nonlinear arithmetic, string, and arrays [Kroening and Strichman 2016].

Footnote 1: SMT is Satisfiability Modulo Theories and the T in DPLL(T) stands for Theories.

### The DNN verification problem

A _neural network_ (**NN**) [Goodfellow et al. 2016] consists of an input layer, multiple hidden layers, and an output layer. Each layer has a number of neurons, each connected to neurons from previous layers through a predefined set of weights (derived by training the network with data). A **DNN** is an NN with at least two hidden layers.

The output of a DNN is obtained by iteratively computing the values of neurons in each layer. The value of a neuron in the input layer is the input data. The value of a neuron in the hidden layers is computed by applying an _affine transformation_ to values of neurons in the previous layers, then followed by an _activation function_ such as the popular Rectified Linear Unit (ReLU) activation.

For this activation, the value of a hidden neuron \(y\) is \(ReLU(w_{1}v_{1}+\ldots+w_{n}v_{n}+b)\), where \(b\) is the bias parameter of \(y\), \(w_{i},\ldots,w_{n}\) are the weights of \(y\), \(v_{1},\ldots,v_{n}\) are the neuron values of preceding layer, \(w_{1}v_{1}+\cdots+w_{n}v_{n}+b\) is the affine transformation, and \(ReLU(x)=\max(x,0)\) is the ReLU activation. The values of a neuron in the output layer is evaluated similarly but it may skip the activation function. A ReLU activated neuron is said to be _active_ if its input value is greater than zero and _inactive_ otherwise.

Figure 1: Original DPLL Algorithm.
_DNN Verification._ Given a DNN \(N\) and a property \(\phi\), the _DNN verification problem_ asks if \(\phi\) is a valid property of \(N\). Typically, \(\phi\) is a formula of the form \(\phi_{in}\Rightarrow\phi_{out}\), where \(\phi_{in}\) is a property over the inputs of \(N\) and \(\phi_{out}\) is a property over the outputs of \(N\). A DNN verifier attempts to find a _counterexample_ input to \(N\) that satisfies \(\phi_{in}\) but violates \(\phi_{out}\). If no such counterexample exists, \(\phi\) is a valid property of \(N\). Otherwise, \(\phi\) is not valid and the counterexample can be used to retrain or debug the DNN (Huang et al., 2017).

_Example._ Fig. 2 shows a simple DNN with two inputs \(x_{1},x_{2}\), two hidden neurons \(x_{3},x_{4}\), and one output \(x_{5}\). The weights of a neuron are shown on its incoming edges, and the bias is shown above or below each neuron. The outputs of the hidden neurons are computed the affine transformation and ReLU, e.g., \(x_{3}=ReLU\left(-0.5x_{1}+0.5x_{2}+1.0\right)\). The output neuron is computed with just the affine transformation, i.e., \(x_{5}=-x_{3}+x_{4}-1\).

A valid property for this DNN is that the output is \(x_{5}\leq 0\) for any inputs \(x_{1}\in[-1,1],x_{2}\in[-2,2]\). An invalid property for this network is that \(x_{5}>0\) for those similar inputs. A counterexample showing this property violation is \(\{x_{1}=-1,x_{2}=2\}\), from which the network evaluates to \(x_{5}=-3.5\). Such properties can capture _safety requirements_ (e.g., a rule in an collision avoidance system in (Katz et al., 2017; Kochenderfer et al., 2012) is "if the intruder is distant and significantly slower than us, then we stay below a certain threshold") or _local robustness_(Katz et al., 2017) conditions (a form of adversarial robustness stating that small perturbations of a given input all yield the same output).

_Abstraction._ ReLU-based DNN verification is NP-Complete (Katz et al., 2017) and thus can be formulated as a SAT or SMT checking problem. Direct application of SMT solvers does not scale to the large and complex formulae encoding real-world, complex DNNs. While custom theory solvers, like Planetand Reluplex, retain the soundness, completeness, and termination of SMT and improve on the performance of a direct SMT encoding, they too do not scale sufficiently to handle realistic DNNs citebak2021second.

Applying techniques from abstract interpretation (Cousot and Cousot, 1977), abstraction-based DNN verifiers overapproximate nonlinear computations (e.g., ReLU) of the network using linear abstract domains such as interval (Wang et al., 2018), zonotope (Singh et al., 2018), polytope (Singh et al., 2019; Xu et al., 2020). As illustrated in Fig. 8 abstract domains can model nonlinearity with varying degrees of precision using polyhedra that are efficient to compute with. This allows abstraction-based DNN verifiers to side-step the disjunctive splitting that is the performance bottleneck of constraint-based DNN verifiers.

A DNN verification technique using an approximation, e.g., the polytope abstract domain, works by (i) representing the input ranges of the DNN as polytopes, (ii) applying transformation rules to the affine and ReLU computations of the network to compute polytope regions representing values of neurons, and (iii) finally, converting the polytope results into output bounds. The resulting outputs are an overapproximation of the actual outputs.

## 3. Overview of NeuralSAT

NeuralSAT is a SMT-based DNN verifier that uses abstraction in its theory solver to accelerate satisfiability checks and the exploration of the space of variable assignments. Fig. 3 gives an overview of NeuralSAT, which follows the DPLL(T) framework (SS2) and consists of standard DPLL components (light shades) and the theory solver (dark shade).

Figure 2. An FNN with ReLU.
NeuralSAT construct a propositional formula over Boolean variables that represent the activation status of neurons (_Boolean Abstraction_). Clauses in the formula assert that each neuron, e.g., neuron \(i\), is active or inactive, e.g., \(v_{i}\lor\overline{v_{i}}\). This abstraction allows us to use standard DPLL components to search for truth values satisfying these clauses and a DNN-specific theory solver to check the feasibility of truth assignments with respect to the constraints encoding the DNN and the property of interest.

NeuralSAT now enters an iterative process to find assignments satisfying the activation clauses. First, NeuralSAT assigns a truth value to an unassigned variable (_Decide_), detects unit clauses caused by this assignment, and infers additional assignments (_Boolean Constraint Propagation_). Next, NeuralSAT invokes the theory solver or T-solver (_DEDUCTION_), which uses LP solving and abstraction to check the satisfiability of the constraints of the current assignment with the property of interest. The T-solver can also infer additional truth assignments.

If the T-solver confirms satisfiability, NeuralSAT continues with new assignments (_Decide_). Otherwise, NeuralSAT detects a conflict (_AnalyzeConflict_) and learns clauses to remember it and backtrack to a previous decision (_Backtrack_). This process repeats until NeuralSAT can no longer backtrack, and return unsat, indicating the DNN has the property, or it finds a total assignment for all boolean variables, and returns sat (and the user can query NeuralSAT for a counterexample).

### Illustration

We use NeuralSAT to prove that for inputs \(x_{1}\in[-1,1],x_{2}\in[-2,2]\) the DNN in Fig. 2 produces the output \(x_{5}\leq 0\). NeuralSAT takes as input the formula \(\alpha\) representing the DNN:

\[\begin{split} x_{3}=ReLU(-0.5x_{1}+0.5x_{2}+1)\ \land\\ x_{4}=ReLU(x_{1}+x_{2}-1)\ \land\\ x_{5}=-x_{3}+x_{4}-1\end{split} \tag{1}\]

and the formula \(\phi\) representing the property:

\[\phi:-1\leq x_{1}\leq 1\land-2\leq x_{2}\leq 2\quad\Rightarrow\quad x_{5} \leq 0. \tag{2}\]

To prove \(\alpha\Rightarrow\phi\), NeuralSAT shows that _no_ values of \(x_{1},x_{2}\) satisfying the input properties would result in \(x_{5}>0\). Thus, we want NeuralSAT to return unsat for \(\overline{\alpha\Rightarrow\phi}\):

\[\alpha\ \land\ -1\leq x_{1}\leq 1\ \land\ -2\leq x_{2}\leq 2\ \land\ x_{5}>0. \tag{3}\]

In the following, we write \(x\mapsto v\) to denote that the variable \(x\) is assigned with a truth value \(v\in\{T,F\}\). This assignment can be either decided by Decide or inferred by BCP. We also write \(x@dl\) and \(\overline{x}@dl\) to indicate the respective assignments \(x\mapsto T\) and \(x\mapsto F\) at decision level \(dl\).

Boolean AbstractionFirst, NeuralSAT creates two Boolean variables \(v_{3}\) and \(v_{4}\) to represent the activation status of the hidden neurons \(x_{3}\) and \(x_{4}\), respectively. For example, \(v_{3}=T\) means \(x_{3}\) is active and thus is the constraint \(-0.5x_{1}+0.5x_{2}+1>0\). Similarly, \(v_{3}=F\) means \(x_{3}\) is inactive and therefore is \(-0.5x_{1}+0.5x_{2}+1\leq 0\). Next, NeuralSAT forms two clauses \(\{v_{3}\lor\overline{v_{3}}\ ;\ 0_{4}\lor\overline{v_{4}}\}\) indicating these variables are either active or inactive.

DPLL(T) IterationsNeuralSAT searches for an assignment to satisfy the clauses and the constraints they represent. In this example, NeuralSAT uses four iterations, summarized in Tab. 1, to determine that no such assignment exists and the problem is thus unsat.

Figure 3. NeuralSAT.
In _iteration 1_, as shown in Fig. 3, NeuralSAT starts with BCP, which has no effects because the current clauses and (empty) assignment produce no unit clauses. In DEDUCTION, NeuralSAT uses an LP solver to determine that the current set of constraints, which contains just the initial input bounds, is feasible 2. NeuralSAT then uses abstraction to approximate an output upper bound \(x_{5}\leq 1\) and thus deduces that satisfying the output \(x_{5}>0\) might be feasible. NeuralSAT continues with DECIDE, which uses a heuristic to select the unassigned variable \(v_{4}\) and sets \(v_{4}=F\). NeuralSAT also increments the decision level (\(dl\)) to 1 and associates \(dl=1\) to the assignment, i.e., \(\overline{v_{4}}@1\).

Footnote 2: We use the terms feasible, from the LP community, and satisfiable, from the SAT community, interchangeably.

In _iteration 2_, BCP again has no effect because it does not detect any unit clauses. In DEDUCTION, NeuralSAT determines that current set of constraints, which contains \(x_{1}+x_{2}-1\leq 0\) due to the assignment \(v_{4}\mapsto F\) (i.e., \(x_{4}=\mathtt{off}\)), is feasible. NeuralSAT then approximates a new output upper bound \(x_{5}\leq-1\), which means satisfying the output \(x_{5}>0\) constraint is _infeasible_.

NeuralSAT now enters ANALYZE-CONFLICT and determines that \(v_{4}\) causes the conflict (\(v_{4}\) is the only variable assigned so far). From the assignment \(\overline{v_{4}}@1\), NeuralSAT learns a "backjumping" clause \(v_{4}\), i.e., \(v_{4}\) must be \(T\). NeuralSAT now backtracks to \(dl\) 0 and erases all assignments decided _after_ this level. Thus, \(v_{4}\) is now unassigned and the constraint \(x_{1}+x_{2}-1\leq 0\) is also removed.

In _iteration 3_, BCP determines that the learned clause is also a unit clause \(v_{4}\) and infers \(v_{4}@0\). In DEDUCTION, we now have the new constraint \(x_{1}+x_{2}-1>0\) due to \(v_{4}\mapsto T\) (i.e., \(x_{4}=\mathtt{on}\)). With the new constraint, NeuralSAT approximates the output upper bound \(x_{5}\leq 0.5\), which means \(x_{5}>0\) might be satisfiable. Also, NeuralSAT computes new bounds \(0.5\leq x_{3}\leq 2.5\) and \(0<x_{4}\leq 2.0\), and deduces that \(x_{3}\) must be positive because its lower bound is 0.5 Thus, NeuralSAT has a new assignment \(v_{3}@0\) (\(dl\) stays unchanged due to the implication). Note that this process of inferring new assignments from the T-solver is referred to theory propagation in DPLL(T).

In _iteration 4_, BCP has no effects because we have no new unit clauses. In DEDUCTION, NeuralSAT determines that the current set of constraints, which contains the new constraint \(-0.5x_{1}+0.5x_{2}+1>0\) (due to \(v_{3}\mapsto T\)), is _infeasible_. Thus, NeuralSAT enters ANALYZE-CONFLICT and determines that \(v_{4}\), which was set at \(dl=0\) (by BCP in iteration 3), causes the conflict. NeuralSAT then learns a clause \(\overline{v_{4}}\) (the conflict occurs when we have the assignment \(\{v_{3}\mapsto T;v_{4}\mapsto T\}\), but \(v_{3}\) was implied and thus making \(v_{4}\) the conflict). However, because the assignment \(v_{4}\) was assigned at decision level 0, NeuralSAT can no longer backtrack and thus sets \(dl=-1\) and returns unsat.

This unsat result shows that the DNN has the property because we cannot find a counterexample violating it, i.e., no inputs \(x_{1}\in[-1,1],x_{2}\in[-2,2]\) that results in \(x_{5}>0\).

## 4. The NeuralSAT Approach

Fig. 4 shows the NeuralSAT algorithm, which takes as input the formula \(\alpha\) representing the ReLU-based DNN \(N\) and the formulae \(\phi_{in}\Rightarrow\phi_{out}\) representing the property \(\phi\) to be proved. Internally,
NeuralSAT checks the satisfiability of the formula

\[\alpha\wedge\phi_{in}\wedge\overline{\phi_{out}}. \tag{4}\]

NeuralSAT returns unsat if the formula unsatisfiable, indicating that \(\phi\) is a valid property of \(N\), and sat if it is satisfiable, indicating the \(N\) is not a valid property of \(\phi\).

NeuralSAT uses a DPLL(T)-based algorithm to check unsatisfiability. First, the input formula in Eq. 4 is abstracted to a propositional formula with variables encoding neuron activation status (BooleanAbstraction). Next, NeuralSAT assign values to Boolean variables (Decide) and checks for conflicts the assignment has with the real-valued constraints of the DNN and the property of interest (BCP and Deduce). If conflicts arise, NeuralSAT determines the assignment decisions causing the conflicts (AnalyzeConflict), backtracks to erase such decisions (Backtrack), and learns clauses to avoid those decisions in the future (AddClause). NeuralSAT repeats these decisions and checking steps until it finds a total or full assignment for all Boolean variables, in which it returns sat, or until it no longer can backtrack, in which it returns unsat. We describe these steps in more detail below.

### Boolean Abstraction

BooleanAbstraction (Fig. 4 line 1) encodes the DNN verification problem into a Boolean constraint to be solved by DPLL. This step creates Boolean variables to represent the _activation status_ of hidden neurons in the DNN. Observe that when evaluating the DNN on any concrete input, the value of each hidden neuron _before_ applying ReLU is either \(>0\) (the neuron is _active_ and the input is passed through to the output) or \(\leq 0\) (the neuron is _inactive_ because the output is \(0\)). This allows partial assignments to these variables to represent neuron activation patterns within the DNN.

Figure 4. The NeuralSAT DPLL(T) algorithm
From the given network, NeuralSAT first creates Boolean variables representing the activation status of neurons. Next, NeuralSAT forms a set of initial clauses ensuring that each status variable is either \(T\) or \(F\), indicating that each neuron is either active or inactive, respectively. For example, for the DNN in Fig. 2, NeuralSAT creates two status variables \(v_{3},v_{4}\) for neurons \(x_{3},x_{4}\), respectively, and two initial clauses \(v_{3}\lor\overline{v_{3}}\) and \(v_{4}\lor\overline{v_{4}}\). The assignment \(\{x_{3}=T,x_{4}=F\}\) creates the constraint \(0.5x_{1}-0.5x_{2}-1>0\wedge x_{1}+x_{2}-2\leq 0\).

### Dpll

After BooleanAbstraction, NeuralSAT iteratively searches for an assignment satisfying the status clauses (Fig. 4, lines 5- 16). NeuralSAT combines DPLL components (e.g., Decide, BCP, AnalyzeConflict, Backtrack) to assign truth values with a theory solver (SS4.3), consisting of abstraction and linear programming solving, to check the feasibility of the constraints implied by the assignment with respect to the network and property of interest.

NeuralSAT maintains several variables (Fig. 4, lines 1- 4). These include clauses, a set of _clauses_ consisting of the initial activation clauses and learned clauses; \(\sigma\), a _truth assignment_ mapping status variables to truth values; _igraph_, an _implication graph_ used for analyzing conflicts; and _dl_, a non-zero _decision level_ used for assignment and backtracking.

#### 4.2.1. Decide

From the current assignment, Decide (Fig. 4, line 15) uses a heuristic to choose an unassigned variable and assigns it a random truth value at the current decision level. We describe our decision heuristic for DNN reasoning in SS4.4.2. Note that if the current assignment is full, i.e., all variables have assigned values, Decide returns False (from which NeuralSAT returns sat).

#### 4.2.2. Boolean Constraint Propagation (BCP)

From the current assignment and clauses, BCP (Fig. 4, line 7) detects _unit clauses3_ and infers values for variables in these clauses. For example, after the decision \(a\mapsto F\), BCP determines that the clause \(a\lor b\) becomes unit, and infers that \(b\mapsto T\). Moreover, each assignment due to BCP is associated with the current decision level because instead of being "guessed" by Decide the chosen value is logically implied by other assignments. Moreover, because each BCP implication might cause other clauses to become unit, BCP is applied repeatedly until it can no longer find unit clauses. BCP returns False if it obtains contradictory implications (e.g., one BCP application infers \(a\mapsto F\) while another infers \(a\mapsto T\)), and returns True otherwise.

Footnote 3: A unit clause is a clause that has a single unassigned literal.

_Implication Graph._ BCP uses an _implication graph_(Barrett, 2013) to represent the current assignment and the reason for each BCP implication. In this graph, a node represents the assignment and an edge \(i\xrightarrow{c}j\) means that BCP infers the assignment represented in node \(j\) due to the unit clause \(c\) caused by the assignment represented by node \(i\). The implication graph is used by both BCP, which iteratively constructs the graph on each BCP application and uses it to determine conflict, and AnalyzeConflict (SS4.2.3), which analyzes the conflict in the graph to learn clauses.

_Example._ Assume we have the clauses in Fig. 5(a), the assignments \(\overline{v_{5}}\)@3 and \(v_{1}\)@6 (represented in the graph in Fig. 5(b) by nodes \(\overline{v_{5}}\)@3 and \(v_{1}\)@6, respectively), and are currently at decision level _dl_ 6. Because of assignment \(v_{1}\)@6, BCP infers \(v_{2}\)@6 from the unit clause \(c_{1}\) and captures that implication with edge \(v_{1}\)@\(6\xrightarrow{c_{1}}v_{2}\)@6. Next, because of assignment \(v_{2}\)@6, BCP infers \(v_{4}\)@6 from the unit clause \(c_{3}\) as shown by edge \(v_{2}\)@6 \(\xrightarrow{c_{3}}v_{4}\)@6.

Similarly, BCP creates edges \(v_{1}\)@\(6\xrightarrow{c_{2}}v_{3}\)@6 and \(\overline{v_{5}}\)@\(\xrightarrow{c_{2}}v_{3}\)@6 to capture the inference \(v_{3}\)@6 from the unit clause \(c_{2}\) due to assignments \(\overline{v_{5}}\)@3 and \(v_{1}\)@6. Now, BCP detects a conflict because
clause \(c_{4}=\overline{o_{3}}\lor\overline{u_{4}}\) cannot be satisfied with the assignments \(v_{4}(\emptyset 6\) and \(v_{3}(\emptyset 6\) (i.e., both \(v_{3}\) and \(v_{4}\) are \(T\)) and creates two edges to the (red) node \(\kappa\): \(v_{4}(\emptyset 6\xrightarrow{c_{4}}\kappa\) and \(v_{3}(\emptyset 6\xrightarrow{c_{4}}\kappa\) to capture this conflict.

Note that in this example BCP has the implication order \(v_{2},v_{4},v_{3}\) (and then reaches a conflict). In the current implementation, NeuralSAT makes an arbitrary decision and thus could have a different order, e.g., \(v_{3},v_{4},v_{2}\).

#### 4.2.3. Conflict Analysis

Given an implication graph with a conflict such as the one in Fig. 5(b), AnalyzeConflict learns a new _clause_ to avoid past decisions causing the conflict. The algorithm traverses the implication graph backward, starting from the conflicting node \(\kappa\), while constructing a new clause through a series of resolution steps. AnalyzeConflict aims to obtain an _asserting_ clause, which is a clause that will force an immediate BCP implication after backtracking.

AnalyzeConflict, shown in Fig. 6, first extracts the conflicting clause \(cl\) (line 1), represented by the edges connecting to the conflicting node \(\kappa\) in the implication graph. Next, the algorithm refines this clause to achieve an asserting clause (lines 2- 6). It obtains the literal \(lit\) that was assigned last in \(cl\) (line 3), the variable \(\underline{var}\) associated with \(lit\) (line 4), and the antecedent clause \(\underline{ante}\) of that \(\underline{var}\) (line 5), which contains \(\overline{lit}\) as the only satisfied literal in the clause. Now, AnalyzeConflict resolves \(cl\) and \(\underline{ante}\) to eliminate literals involving \(\underline{var}\) (line 6). The result of the resolution is a clause, which is then refined in the next iteration.

_Resolution._ We use the standard _binary resolution rule_ to learn a new clause implied by two (_resolving_) clauses \(a_{1}\lor...\lor a_{n}\lor\beta\) and \(b_{1}\lor...\lor b_{m}\lor\overline{\beta}\) containing complementary literals involving the (_resolution_) variable \(\beta\):

\[\frac{(a_{1}\lor...\lor a_{n}\lor\beta)}{(a_{1}\lor...\lor a_{n}\lor b_{1}\lor...\lor b_{m}\lor\overline{\beta})}\quad(\text{Binary-Resolution}) \tag{5}\]

Figure 5. (a) A set of clauses, (b) an implication graph, and (c) learning a new clause.

Figure 6. AnalyzeConflict
The resulting (_resolvant_) clause \(a_{1}\lor...\lor a_{n}\lor b_{1}\lor...\lor b_{m}\) contains all the literals that do not have complements \(\beta\) and \(\neg\beta\).

Example.Fig.5(c) demonstrates AnalyzeConflict using the example in SS4.2.2 with the BCP implication order \(v_{2},v_{4},v_{3}\) and the conflicting clause \(cl\) (connecting to node \(\kappa\) in the graph in Fig.5(b)) \(c_{4}=\overline{v_{3}}\lor\overline{v_{4}}\). From \(c_{4}\), we determine the last assigned literal is \(lit=\overline{v_{3}}\), which contains the variable \(var=v_{3}\), and the antecedent clause containing \(v_{3}\) is \(c_{2}=\overline{v_{1}}\lor v_{3}\lor v_{5}\) (from the implication graph in Fig.5(b), we determine that assignments \(v_{1}\)@\(6\) and \(\overline{v_{5}}\)@\(3\) cause the BCP implication \(v_{3}\)@\(6\) due to clause \(c_{2}\)). Now we resolve the two clauses \(cl\) and \(c_{2}\) using the resolution variable \(v_{3}\) to obtain the clause \(\overline{v_{4}}\lor\overline{v_{1}}\lor v_{5}\). Next, from the new clause, we obtain \(lit=\overline{v_{4}},var=v_{4},ante=c_{3}\) and apply resolution to get the clause \(\overline{v_{1}}\lor v_{5}\lor\overline{v_{2}}\). Similarly, from this clause, we obtain \(lit=\overline{v_{2}},var=v_{2},ante=c_{1}\) and apply resolution to obtain the clause \(v_{1}\lor v_{5}\).

At this point, AnalyzeConflict determines that this is an asserting clause, which would force an immediate BCP implication after Backtracking. As will be shown in SS4.2.4, NeuralSAT will backtrack to level \(3\) and erases all assignments after this level (so the assignment \(\overline{v_{5}}\)@\(3\) is not erased, but assignments after level \(3\) are erased). Then, BCP will find that \(c_{5}\) is a unit clause because \(\overline{v_{5}}\)@\(3\) and infers \(\overline{v_{1}}\). Once obtaining the asserting clause, AnalyzeConflict stops the search, and NeuralSAT adds \(v_{1}\lor v_{5}\) as the new clause \(c_{5}\) to the set of existing four clauses.

The process of learning clauses allows NeuralSAT to learn from its past mistakes. While such clauses are logically implied by the formula in Eq.4 and therefore do not change the result, they help prune the search space and allow DPLL and therefore NeuralSAT to scale. For example, after learning the clause \(c_{5}\), together with assignment \(v_{5}\)@\(3\), we immediately infer \(v_{1}\mapsto F\) through BCP instead of having to guess through Decide.

#### 4.2.4. Backtrack

From the clause returned by AnalyzeConflict, Backtrack (Fig.4, line12) computes a backtracking level and erases all decisions and implications made after that level. If the clause is _unary_ (containing just a single literal), then we backtrack to level \(0\).

Currently, NeuralSAT uses the standard _conflict-drive backtracking_ strategy (Barrett, 2013), which sets the backtracking level to the _second most recent_ decision level in the clause. Intuitively, by backtracking to the second most recent level, which means erasing assignments made _after_ that level, this strategy encourages trying new assignments for more recently decided variables.

Example.From the clause \(c_{5}=\overline{v_{1}}\lor v_{5}\) learned in AnalyzeConflict, we backtrack to decision level \(3\), the second most recent decision level in the clause (because assignments \(v_{1}\)@\(6\) and \(\overline{v_{5}}\)@\(3\) were decided at levels \(6\) and \(3\), respectively). Next, we erase all assignments from decision level \(4\) onward (i.e., the assignments to \(v_{1},v_{2},v_{3},v_{4}\) as shown in the implication graph in Fig.5). This thus makes these more recently assigned variables (after decision level \(3\)) available for new assignments (in fact, as shown by the example in SS4.2.2, BCP will immediately infer \(v_{1}=T\) by noticing that \(c_{5}\) is now a unit clause).

### Deduction (Theory Solving)

Deduce (Fig.4, line8) is the theory solver, i.e., the T in DPLL(T). The main purpose of the theory solver is to check the feasibility of the constraints represented by the current propositional variable assignment; as shown in the formalization in SS5 this amounts to just _linear equation_ solving for verifying piecewise linear DNNs. However, NeuralSAT is able to leverage specific information from the DNN problem, including input and output properties, for more aggressive feasibility checking. Specifically, Deduce has three tasks: (i) checking feasibility using linear programming (LP) solving, (i) further checking feasibility with input tightening and abstraction, and (iii) inferring literals that are unassigned and are implied by the abstracted constraint.
```
input:current assignment \(\sigma\) and decision level \(dl\), DNN \(\alpha\), input property \(\phi_{in}\), output property \(\phi_{out}\) output:false if infeasibility occurs, true otherwise
1 solver=newLPSolver(solver, \(\alpha,\sigma\land\phi_{in}\land\overline{\phi_{out}}\))
2ifSolve(solver)\(\equiv\)INFEASIBLEthenreturnfalse
3ifisTotal(\(\sigma\))then
4returntrue//origprob(Eq. 4)issatisfiable
5 input_bounds=TightenInputBounds(solver, \(\phi_{in}\)) output_bounds,hidden_bounds=Abstract(\(\alpha,\sigma,\text{input\_bounds}\))
6ifCheck(output_bounds, \(\overline{\phi_{out}}\))\(\equiv\)INFEASIBLEthen
7 returnfalse
8for\(v\in\)hidden_boundsdo
9\(x\leftarrow\)ActivationStatus(\(v\))
10if\(x\in\sigma\lor\neg x\in\sigma\)thencontinue
11ifLowerBound(\(v\))\(>0\)then\(\sigma\leftarrow\sigma\cup x\)@\(dl\)
12elseifUpperBound(\(v\))\(\leq 0\)then\(\sigma\leftarrow\sigma\cup\overline{x}\)@\(dl\)
13returntrue
```

**Fig. 7**: Deduce

Fig. 7 describes Deduce, which returns False if infeasibility occurs and True otherwise. First, it creates a linear constraint system from the input assignment \(\sigma\) and \(\alpha\land\phi_{in}\land\overline{\phi_{out}}\), i.e., the formula in Eq. 4 representing the original problem (line 1). The key idea is that we can remove ReLU activation for hidden neurons whose activation status have been decided. For constraints in \(\alpha\) associated with variables that are not in the \(\sigma\), we ignore them and just consider the cutting planes introduced by the partial assignment. For example, for the assignment \(v_{3}\mapsto T,v_{4}\mapsto F\), the non-linear ReLU constraints \(x_{3}=ReLU(-0.5x_{1}+0.5x_{2}+1)\) and \(x_{4}=ReLU(x_{1}+x_{2}-1)\) for the DNN in Fig. 2 become linear constraints \(x_{3}=-0.5x_{1}+0.5x_{2}\) and \(x_{4}=0\), respectively.

Next, an LP solver checks the feasibility of the linear constraints (line 2). If the solver returns infeasible, Deduce returns False so that NeuralSAT can analyze the assignment and backtrack. If the constraints are feasible, then there are two cases to handle. First, if the assignment is total (i.e., all variables are assigned), then that means that the original problem is satisfiable (line 4) and NeuralSAT returns sat.

ReLU AbstractionSecond, if the assignment is not total then Deduce applies abstraction to check satisfiability (lines 5-8). Specifically, we over-approximate ReLU computations to obtain the upper and lower bounds of the output values and check if the output properties are feasible with respect to these bounds. For example, the output \(x_{5}>0\) is _not_ feasible if the upperbound is \(x_{5}\leq 0\) and _might be_ feasible if the upperbound is \(x_{5}\leq 0.5\) ("might be" because this is an upper-bound). If abstraction results in infeasibility, then Deduce returns False for NeuralSAT to analyze the current assignment (line 8).

NeuralSAT uses abstraction to approximate the lower and upper bounds of hidden and output neurons. Fig. 8 compares the interval [Wang et al.2018] (a), zonotope [Singh et al.2018] (b), and polytope [Singh et al.2019, Wang et al.2021, Xu et al.2020] (c,d) abstraction domains to compute the lower \(l_{y}(x)\) and upper \(u_{y}(x)\) bounds of a ReLU computation \(y=\)ReLU(x) (non-convex red line). NeuralSAT can employ any existing abstract domains, though currently it adopts the _LiRPA_ polytope (Fig. 8c) [Wang et al.2021, Xu et al.2020] because it has a good trade-off between precision and efficiency.
Note that in some cases we can compute a better abstraction for output bounds by first tightening the input bounds (line 5). We discuss this input bound tightening heuristic in SS4.4.1.

InferenceIf abstraction results in feasible constraints, Deduce next attempts to infer implied literals (lines 9- 13). To obtain the bounds of the output neurons, abstraction also needs to compute the bounds of hidden neurons, including those with undecided activation status (i.e., not yet in \(\sigma\)). This allows us to assign the activation variable of a hidden neuron the value True if the lowerbound of that neuron is greater than \(0\) (the neuron is active) and False otherwise. Since each literal is considered, this would be considered exhaustive theory propagation. Whereas the literature (Kroening and Strichman, 2016; Nieuwenhuis et al., 2006) suggests that this is an inefficient strategy, we find that it does not incur significant overhead (average overhead is about \(4\%\) and median is \(2\%\) with outliners being large CIFAR2020 networks described in SS6).

ExampleFor the illustrative example in SS3.1, in iteration 3, the current assignment \(\sigma\) is \(\{v_{4}=1\}\), corresponding to a constraint \(x_{1}+x_{2}-1>0\). With the new constraint, we optimize the input bounds and compute the new bounds for hidden neurons \(0.5\leq x_{3}\leq 2.5\), \(0<x_{4}\leq 2.0\) and output neuron \(x_{5}\leq 0.5\) (and use this to determine that the postcondition \(x_{5}>0\) might be feasible). We also infer \(v_{3}=1\) because of the positive lower bound \(0.5\leq x_{3}\).

### Optimizations

NeuralSAT implements several optimizations to quickly deal with "easy" problems, such as those with _small input_ sizes or can be _easily disproved_ (of course NeuralSAT does not know this in advance, it just tries the heuristics in hope that it could help). As we will see in SS7, these techniques are also employed by many current state-of-the-art DNN verification tools.

#### 4.4.1. Input Bounds Tightening

For networks with small inputs (currently set to those with \(\leq 50\) inputs), NeuralSAT uses a more aggressive abstraction process in the theory solver described in SS4.3. Specifically, we use LP solving to compute the tightest bounds for all input variables from the generated linear constraints. This computation is efficient when the number of inputs is small. After tightening input bounds we apply abstraction (line 6, Fig. 7) to approximate the output bounds, which can be more precise with better input bounds. For networks with large number of inputs, we obtain input bounds from the input property \(\phi_{in}\).

#### 4.4.2. Decision Heuristics

Decision or branching heuristics decide free variables to make assignments and thus are crucial for the scalability of DPLL by reducing assignment mistakes (Beyer, 2022; Kroening and Strichman, 2016). NeuralSAT currently adopts two decision heuristics.

Figure 8. Abstractions for ReLU: (a) interval, (b) zonotope, (c) LiRPA polytope, and (d) DeepPoly polytope. Notice that ReLU is a non-convex region (red line) while all abstractions are convex regions
For networks with small inputs, NeuralSAT prioritizes variables representing neurons with the _furthest bounds_ from the decision value 0 of ReLU, i.e., the 0 in \(\max(x,0)\). Such neurons have wider bounds and therefore are more difficult to tighten during abstraction compared to other neurons. This heuristic helps input bounds tightening as described in SS4.4.1 (which is also applied only for networks with small inputs). It is also cheap because we can reuse the computed boundaries of hidden neurons during abstraction.

For other networks, NeuralSAT applies the Filtered Smart Branching (FSB) heuristic (Bunel et al., 2018; De Palma et al., 2021). For each unassigned variable, FSB assumes that it has been decided (i.e., the corresponding neuron has been split) and computes a fast approximation of the lower and upperbounds of the network output variables. FSB then prioritizes unassigned variables with the best differences among the bounds that would help make the input formula unsatisfiable (which helps prove the property of interest). We note that several well-known DNN verification techniques and tools (OVAL-group, 2023; Wang et al., 2021) use variants of FSB with slight difference on the approximation computation.

#### 4.4.3. Multiprocessing

For networks with small inputs, NeuralSAT uses a simple approach to create and solve subproblems in parallel. Given a verification problem \(N_{orig}=(\alpha,\phi_{in},\phi_{out})\), where \(\alpha\) is the DNN and \(\phi_{in}\Rightarrow\phi_{out}\) is the desired property, NeuralSAT creates subproblems \(N_{i}=(\alpha,\phi_{in_{i}},\phi_{out})\), where \(\phi_{in_{i}}\) is the \(i\)-th subregion of the input region specified by \(\phi_{in}\). Intuitively, each subproblem checks if the DNN produces the output \(\phi_{out}\) from a smaller input region \(\phi_{in_{i}}\). The combination of these subproperties \(\bigwedge\phi_{in}\Rightarrow\phi_{out}\) is logically equivalent to the original property \(\phi_{in}\Rightarrow\phi_{out}\).

Given \(k\) available threads, NeuralSAT splits the original input region to obtain subproblems as described and and runs DPLL(T) on \(k\) subproblems in parallel. NeuralSAT returns unsat if it verifies all subproblems and sat if it found a counterexample in any subproblem. For example, we split the input region \(\{x_{1}\in[-1,1],x_{2}\in[-2,2]\}\) into four subregions \(\{x_{1}\in[-1,0],x_{2}\in[-2,0]\}\), \(\{x_{1}\in[-1,0],x_{2}\in[0,2]\}\), \(\{x_{1}\in[0,1],x_{2}\in[-2,0]\}\), and \(\{x_{1}\in[0,1],x_{2}\in[0,2]\}\). Note that the formula \(-1\leq x_{1}\leq 1\land-2\leq x_{2}\leq 2\) representing the original input region is equivalent to the formula \((-1\leq x_{1}\leq 0\lor 0\leq x\leq 1)\land(-2\leq x_{2}\leq 0\lor 0\leq x_{2}\leq 2)\) representing the combination of the created subregions.

#### 4.4.4. Falsification using Adversarial Attacks

Our NeuralSAT tool attempts to disprove or falsify the property before running DPLL(T). This helps solve "easy" cases when the properties can be disproved easily and adopted by many state-of-the-art DNN verification tools such as ERAN(Muller et al., 2022) and \(\alpha\beta\)-CROWN(Zhang et al., 2022).

NeuralSAT uses two adversarial attack algorithms to find counterexamples to falsify properties. First, we try a randomized attack approach (Das et al., 2021), which is a derivative-free sampling-based optimization (Yu et al., 2016), to generate a potential counterexample. If this approach fails, we then use a gradient-based approach (Madry et al., 2017) to create another potential counterexample.

If either attack algorithm gives a valid counterexample, NeuralSAT returns sat, indicating that property is invalid. If both algorithms cannot find a valid counterexample or they exceed a predefined timeout, NeuralSAT continues with its DPLL(T) search.

## 5. NeuralSAT DPLL(T) Formalization

In SS4 we describe NeuralSAT and its optimizations, here we formalize the NeuralSAT DPLL(T) framework. By abstracting away heuristics, optimizations, and implementation details, we can focus on the core NeuralSAT algorithm and establish its correctness and termination properties.

NeuralSAT can be described using the states and transition rules of the standard DPLL(T) framework described in (Nieuwenhuis et al., 2006) and therefore inherits the theoretical results established there. We also highlight the differences between NeuralSAT and standard DPLL(T), but
these differences do not affect any of the main results. The section aims to be self-contained, but readers who are familiar with the work in (Nieuwenhuis et al., 2006) can quickly skim through it.

### Preliminaries

Formulae, Theory, and Satisfiability.Let \(P\) be a finite set of atoms (e.g., linear constraints in our context). For an atom \(p\in P\), \(p\) is a positive literal and \(\neg p\) is a negative literal of \(P\). A _clause_ is a set of literals and a CNF _formula_ is a set of clauses. A model \(M\) is a sequence of literals and never contains both a literal and its negation.

A literal \(l\) is _true_ in \(M\) if \(l\in M\), is _false_ in \(M\) if \(\neg l\in M\), and is _undefined_ otherwise (i.e., \(l\notin M\)). \(M\) is _total_ if every atom \(p\in P\) has a literal in \(M\), and is _partial_ otherwise. A clause \(C\) is true in \(M\), written as \(M\models C\), if \(\exists l\in C\). \(l\in M\), and is false in \(M\), written as \(M\models\neg C\), if \(\forall l\in C\). \(\neg l\in M\). A CNF \(F\) is true in (or satisfied by) \(M\), written as \(M\models F\), if all clauses of \(F\) are true in \(M\). In that case, \(M\) is called a _model_ of \(F\). If F has no models then it is _unsatisfiable_. If \(F\) and \(F^{\prime}\) are formulae, then \(F\)_entails_\(F^{\prime}\), written as \(F\models F^{\prime}\), if \(F^{\prime}\) is true in all models of \(F\). Note that we consider literals and clauses as purely boolean variables and check satisfiability using propositional logic (we could also treat literals as syntactical items and check satisfiability using set operations, e.g., \(M\models C\) is \(C\cap M\neq\emptyset\)).

A theory T is a set of formulas. A formula F is _T-satisfiable_ or _T-consistent_ if \(F\wedge T\) is satisfiable. Otherwise, it is called _T-unsatisfiable_ or _T inconsistent_. An assignment \(M\) can be thought as a conjunction of its literals and hence as a formula. If \(M\) is a T-consistent and \(F\) is a formula such that \(M\models F\), then \(M\) is also a _T-model_ of F, written as \(M\models_{T}F\). If F and G are formulae, then F entails G in T, written \(F\models_{T}G\) if \(F\wedge\neg G\) is T-inconsistent. Note when checking satisfiability in the theory, i.e., \(\models_{T}\), we use a theory solver to reason about the linear constraints represented by the literals.

**NeuralSAT Algorithm.** For NeuralSAT, each atom \(p_{i}\) in \(P=\{p_{1},p_{2},\ldots,p_{N}\}\) is the linear constraint representing activation status of neuron \(i\), e.g., for the DNN example in Fig. 2, \(p_{3}\) is \(-0.5x_{1}+0.5x_{2}+1>0\), the constraint that neuron \(x_{3}\) is active (thus \(p_{3}\) is a positive literal and \(\neg p_{3}\) is a negative literal). \(M\) represents the (partial) truth assignment \(\sigma\), and \(F\) represents the set or conjunction of clauses that NeuralSAT needs to satisfy. Adding \(l\) to \(M\) is the truth assignment \(p\mapsto T\) if \(l\) is \(p\), and is the assignment \(p\mapsto F\) if \(l\) is \(\neg p\). Moreover, the theory we consider is LRA (Linear Real Arithmetic) and our customized T-solver, described in 4.3 uses LP solving and abstraction to decide satisfiability of DNN properties.

Note that in NeuralSAT we use Boolean Abstraction to create variables \(v_{i}\) to represent linear constraints capturing activation status. Here we do not use Boolean Abstraction and capture its effects with atoms \(p_{i}\) representing the Boolean variables \(v_{i}\) and adding to \(M\) the literals \(p_{i},\neg p_{i}\) corresponding to truth assignments \(v_{i}\mapsto T,v_{i}\mapsto F\) in \(\sigma\), respectively.

### Transition Rules

We formalize the NeuralSAT DPLL(T) using _transition rules_ that move from a state to another state of the algorithm. A _state_ is either a assignment \(M\) and a CNF formula \(F\), written as \(M\parallel F\), or the special state \(\mathsf{Fail}\), which indicates that the formula is unsatisfiable. We write \(S\Longrightarrow S^{\prime}\) as a transition from state \(S\) to \(S^{\prime}\). We write \(S\Longrightarrow^{*}S^{\prime}\) to indicate any possible transition from \(S\) to \(S^{\prime}\) (i.e., reflexive-transitive closure). In a state \(M\parallel F,C\), we say the clause \(C\) is conflicting if \(M\models\neg C\).

Tab. 2 gives the conditional transition rules for NeuralSAT. _Decision_ literals, written with suffix \(l^{d}\), are non-deterministically decided (i.e., guessed), while other literals are deduced deterministically through implication. Intuitively, mistakes can happen with decision literals and require backtracking. In contrast, rules that add non-decision literals help prune the search space.

The rules _Decide_, _BCP_, _Fail_ describe transitions that do not rely on theory solving. _Decide_ non-deterministically selects and adds an undefined literal \(l\) to \(M\) (i.e., \(l\) is a decision literal and can be backtracked to when conflict occurs). _BCP_ (or UnitPropagate) infers and adds the unit literal \(l\) to
to satisfy the clause \(C\lor l\), where \(M\models\neg C\). _Fail_ moves to a Fail state (i.e., \(F\) is unsatisfiable) when a conflicting clause \(C\) occurs and \(M\) contains no decision literals to backtrack to.

The rules _T-Learn_, _T-Forget_, _T-Backjump_, _TheoryPropagate_ describe transitions that rely on theory solving, e.g., \(\models_{T}\). _T-Backjump_ analyzes a conflicting clause \(C\) to determine an "incorrect" decision literal \(l^{d}\) and computes a "backjump" clause \(C^{\prime}\lor l^{\prime}\) (which will be used by _T-learn_ to ensure that the incorrect decision literal \(l\) will not be added to \(M\) in the future). The rule also adds \(l^{\prime}\) to \(M\) (since \(M\models\neg C^{\prime}\)) and removes \(l^{d}\) and the set \(N\) of subsequent literals added to \(M\) after \(l^{d}\) (i.e., it backtracks and removes the "incorrect" decision \(l^{d}\) and subsequent assignments). _T-Learn_ strengthens \(F\) with a clause \(C\) that is entailed by \(F\) (i.e., learned clauses are _lemmas_ of \(F\)). As mentioned, clause \(C\) is the "backjumping" clause \(C^{\prime}\lor l^{\prime}\) in _T-Backjump_. Finally, _TheoryPropagate_ infers literals that are T-entailed by literals in \(M\) (thus \(l\) is a non-decision literal).

**NeuralSAT Algorithm.** The Decide and BCP rules align to the Decide and BCP components of NeuralSAT, respectively. The other rules are also implemented in NeuralSAT through the interactions of Deduction, Analyze-Conflict, and Backtrack components. For example, the T-Backjump rule is implemented as part of Deduction and AnalyzeConflict. Also note that while implication graph is a common way to detect conflicts and derive backjumping clause, it is still an implementation detail and therefore not mentioned in T-Backjump (which states there exists a way to obtain a backjumping clause). T-Learn, which adds lemmas to existing clauses, is achieved in the main loop of the NeuralSAT algorithm (Fig. 4, line 13). TheoryPropagate is implemented as part of _Deduction_ (Fig. 7, lines 9-13). Finally, theory solving, i.e., \(\models_{T}\), is implemented in Deduction by using LP solving and abstraction to check satisfiability of linear constraints.
Note that DPLL and DPLL(T) algorithms used in modern SAT and SMT solvers often include Restart and T-Forget rules, which remove learned clauses periodically. To date, we have not seen the need for these in NeuralSAT, but they could easily be incorporated.

### Termination and Correctness of NeuralSAT DPLL(T)

In SS5.2 we describe NeuralSAT DPLL(T) using transition rules of the standard DPLL(T) approach. This allows us to establish the the formal properties NeuralSAT DPLL(T), which are similar to those of standard DPLL(T). Below we summarize the main results and refer the readers to [Nieuwenhuis et al. 2006] for complete proofs.

Note that the work in [Nieuwenhuis et al. 2006] covers multiple variants of DPLL with various rule configurations. Here we focus on the DPLL(T) of NeuralSAT, e.g., no Restart and Forget. This significantly simplify our demonstration of termination and correctness of NeuralSAT DPLL(T).

We first establish several invariants for the transition rules of NeuralSAT DPLL(T).

**Lemma 5.1**.: _If \(\emptyset\parallel F\Longrightarrow^{*}M\parallel G\), then the following hold:_

1. _All atoms in_ \(M\) _and all atoms in_ \(G\) _are atoms of_ \(F\)_._
2. \(M\) _is indeed an assignment, i.e., it contains no pair of literals_ \(p\) _and_ \(\neg p\)_._
3. \(G\) _is equivalent to_ \(F\) _in the theory T._

All properties hold trivially in the initial state \(\emptyset\parallel F\), so we will use induction to show the transition rules preserve them. Consider a transition \(M^{\prime}\parallel F^{\prime}\Longrightarrow M^{\prime\prime}\parallel F^{ \prime\prime}\). Assume the properties hold for \(M\parallel F\). Property 1 holds because the only atoms can be added to \(M^{\prime\prime}\) and \(F^{\prime\prime}\) are from \(M^{\prime}\) and \(F^{\prime}\), all of which belong to \(F\). Property 2 preserves the requirement that \(M\) never shares both negative and positive literals of an atom (the condition of each rule adding a new literal ensures this). Property 3 holds because only T-Learn rule can modify \(F^{\prime}\), but learning a clause \(C\) that is a logical consequence of \(F^{\prime}\) (i.e., \(F^{\prime}\models_{T}C\)) will preserve the equivalence between \(F^{\prime}\) and \(F^{\prime\prime}\).

**Lemma 5.2**.: _If \(\emptyset\parallel F\Longrightarrow^{*}S\), and \(S\) is final state, then \(S\) is either Fail, or of the form \(M\parallel F^{\prime}\), where \(M\) is a T-model of \(F\)._

This states that if \(M\models F^{\prime}\) then \(M\models F\). This is true because \(F\) and \(F^{\prime}\) are logical equivalence by Lemma 5.1(3).

Now we prove that NeuralSAT DPLL(T) **terminates**.

**Theorem 5.3** (Termination).: _Every derivation \(\emptyset\parallel F\Longrightarrow S_{1}\Longrightarrow\dots\) is finite._

This proof uses a well-founded strict partial ordering on _states_\(M\parallel F\). First, consider the case without T-Learn, in which only the assignment M is modified and the formula F remains constant. Then we can show no infinite derivation by (i) using Lemma 5.1(1,2) that the number of literals in M and M' are always less than or equal to the number of atoms in F and (ii) show that the number of "missing" literals of M is strictly greater than those of M'. Now, consider the case with T-learn. While F' can now be modified, i.e., learning new clauses, the number of possible clauses can be added to \(F^{\prime}\) is finite as clauses are formed from a finite set of atoms and the conditions of T-learn disallow clause duplication.

Note that if NeuralSAT involved the Restart and Forget rules, which periodically remove learned clauses, then its termination argument becomes more complicated (but still holds) as shown in the work [Nieuwenhuis et al. 2006].

Now we prove that NeuralSAT DPLL(T) is **sound** and **complete**.

**Theorem 5.4**.: _If \(\emptyset\parallel F\Longrightarrow^{*}S\) where the state \(S\) is final, then_

1. _Sound_: \(S\) _is Fail if, and only if,_ \(F\) _is T-unsatisfiable_
2. **Complete:**_If \(S\) is of the form \(M\parallel F^{\prime}\), then \(M\) is a T-model of \(F\)._

Property 1 states that NeuralSAT DPLL(T) ends at Fail state iff the problem F is unsatisfiable. Property 2 asserts that if NeuralSAT DPLL(T) ends with an assignment \(M\), then \(M\) is the model of \(F\), i.e, \(F\) is satisfiable. This property requires showing that if \(M\models_{T}F^{\prime}\), then \(M\models_{T}F\), which is established in Lemma 5.2.

Together, these properties of soundness, completeness, and termination make NeuralSAT DPLL(T) a decision procedure. Note that the presented results are independent from the theory under consideration. The main requirement of T-solver is its decidability for T-satisfiability or T-consistency checking. NeuralSAT uses LRA, a theory of real numbers with linear constraints, including linear equalities and inequalities, which is decidable (Kroening and Strichman, 2016).

## 6. Implementation and Experimental Settings

ImplementationNeuralSAT is written in Python, and uses PyTorch (Paszke et al., 2019) for matrix multiplications and Gurobi (Gurobi Optimization, LLC, 2022) for linear constraint solving. We use the LiRPA abstraction library (Wang et al., 2021; Xu et al., 2020) for bounds approximation and tightening and adapt the randomized (Das et al., 2021) and Projected Gradient Descent (PGD) (Madry et al., 2017) adversarial attack techniques for falsification. Note that unlike some other DNN verifiers, NeuralSAT does not require hyperparameter tuning and all of our experiments use its default settings.

Currently, NeuralSAT supports feedforward (FNN), convolutional (CNN), and Residual Learning Architecture (ResNet) neural networks that use ReLU. NeuralSAT automatically preprocesses these networks into Boolean variables and linear constraints representing the computation graph of the networks for DPLL(T). This preprocessing step is relatively standard and is used by various tools (e.g., \(\alpha\)-\(\beta\)-CROWN, ERAN, MN-BaB). Moreover, NeuralSAT supports the specification formats ONNX (Bai et al., 2023) for neural networks and VNN-LIB (Tacchella et al., 2023) for properties. These formats are standard and supported by major DNN verification tools.

BenchmarksWe evaluate NeuralSAT using five standard, ReLU-based benchmarks obtained VNN-COMP'22 and shown in Tab. 3. In total these benchmarks consist of 53 networks, spanning multiple layer types and architectures, and 447 correctness properties. A problem instance pairs a
property with a network. Across the benchmark 389 problem instances are known to be unsat (U) and 136 are known to be sat (S). For the remaining 98 problem instances no verifier in our study or in VNN-COMP'22 was able to solve the problem. We do not include these _unknown_ (?) problem instances in our study since they add no value in our comparative evaluation of DNN verifier performance.

**ACAS Xu** consists of 45 FNNs to issue turn advisories to aircrafts to avoid collisions. Each FNN has 5 inputs (speed, distance, etc). We use all 10 safety properties as specified in [14] and VNN-COMP'22, where properties 1-4 are used on 45 networks and properties 5-10 are used on a single network. **MNISTFC** consists of 3 FNNs for handwritten digit recognition and 30 robustness properties. Each FNN has 28x28 inputs representing a handwritten image. **CIFAR2020** has 3 CNNs for objects detection and 203 robustness properties (each CNN has a set of different properties). Each network uses 3x32x32 RGB input images. For **RESNET_A/B**, each benchmark has only one network with the same architecture and 72 robustness properties. Each network uses 3x32x32 RGB input images.

Tab. 3 provides more details. Column **Instances (U/S/7)** shows the number of verification instances and U/S/? indicate the number of instances that are unsat (valid property), sat (invalid property), and unknown (cannot be solved by any tools and we also do not know if it is sat or unsat), e.g., CIFAR10\(2\)255 has 82 instances (65 unsat, 13 sat, and 4 unknown). The last two columns give the sizes of individual networks: **neurons** are the numbers of hidden neurons and **parameters** are the numbers of weights and biases. For example, each FNN in ACAS Xu has 5 inputs, 6 hidden layers (each with 50 neurons), 5 outputs, and thus has 300 neurons (\(6\times 50\)) and 13305 parameters (\(5\times 50\times 50+2\times 50\times 5+6\times 50+5\)). Observe that networks from ACAS Xu have very few inputs (5), which is leveraged by many DNN verification tools as shown in SS7.

_Verification Tools._ We compare NeuralSAT to six well-known DNN verifiers. \(\alpha-\beta-\texttt{CRONN}\)[22, 23] employs multiple abstractions and algorithms for efficient analysis (input splitting for networks with small input dimensions and parallel Branch-and-Bound [1] (BaB) otherwise). **ERAN[22, 24, 23]** uses input splitting optimizations with various abstractions. **MN-BaB** uses multiple abstractions and BaB. **Marabou'21** (VNN-COMP'21 version) and **Marabou'22** (VNN-COMP'22 version) [14] are a simplex-based solver that employs various optimizations such as parallel Split-and-Conquer [25] (SnC) and uses polytope abstraction [22] and MILP/LP-based bound tightening. **nnenum**[1] combines optimizations such as parallel case splitting and multiple levels of abstractions, e.g., three types of zonotopes with imagestar/starset [20].

Among tools competing in recent VNN-COMPs'21 [1] and '22 [23], \(\alpha-\beta-\texttt{CRONN}\), MN-BaB, ERAN, and nnenum are consistently considered the top. For example, in VNN-COMP'22, \(\alpha-\beta-\texttt{CRONN}\) is the winner for MNISTFC and also the overall winner, MN-BaB ranked 3rd on MNISTFC and second overall, and nnenum was the only one that can solve all instances in ACAS Xu and was 4th overall. Marabou'22 ranked 6th on MNISTFC and 7th overall. We also include Marabou'21, which only participated in VNN-COMP'21 and ranks 5th overall, because it outperforms Marabou'22 in many cases as shown in SS7.

_Hardware and Setup._ Our experiments were run on a Linux machine with an AMD Threadripper 64-core 4.2GHZ CPU, 128GB RAM, and a NVIDIA GeForce RTX 4090 GPU with 24 GB VRAM. All tools use multiprocessing (even external tools/libraries including Gurobi, LiRPA, and Pytorch are multi-thread). ERAN, \(\alpha-\beta-\texttt{CRONN}\), and MN-BaB leverage GPU processing for abstraction. The LiRPA library adopted by NeuralSAT uses the GPU for large benchmarks in MNISTFC, CIFAR2020 and RESNET.
To maximize the performance of the DNN verifiers in comparisons, we leverage the benchmarks and installation scripts available from VNN-COMP ([https://github.com/ChristopherBrix/vnncomp2022_benchmarks](https://github.com/ChristopherBrix/vnncomp2022_benchmarks)). These scripts were tailored by the developers of each verifier to optimize performance on each benchmark. The VNN-COMP setting used varying runtimes for each problem instance ranging from 120 seconds to more than 12 minutes. We experimented with timeouts on our machine and settled on 200 seconds per instance which allowed the verifiers to achieve the scoring performance reported in VNN-COMP'22. For each benchmark instance we run three times and obtain the median results.

## 7. Results

We evaluate NeuralSAT using the following research questions:

* (SS7.1) How NeuralSAT compares to state-of-the-art DNN verifiers?
* (SS7.2) How it compare to other tools in sat and unsat instances?
* (SS7.3) How NeuralSAT compares to state-of-the-art DPLL(T)-based DNN verifiers?

We note that in our experiments all tools provide _correct results_. If a tool was able to solve an instance, then it solves it correctly, i.e., no tool returned sat for unsat instances and vice versa.

### VNN-COMP Ranking

We adopt the rules in VNN-COMP'22 to score and rank tools. This gives an overall view of how NeuralSAT compares to others in a VNN-COMP setting which accounts for both runtime and ability to solve problems. As mentioned in 6, we use the exact scripts from VNN-COMP'22 to setup and run this experiment.

_Scoring Rules_. For each benchmark instance, a tool scores 10 points if it correctly verify an instance, 1 point if it correctly falsifies an instance4, 0 points if it cannot solve (e.g., timeouts, has errors, or returns unknown), -100 points if it gives incorrect results (does not apply to any tool we consider), 2 points for being the fastest among other tools competing on that instance, 1 point for being the second fastest (runtime within a 0.2s differences are considered the same).

Footnote 4: VNN-COMP’22 assigns different scores for falsification: 1 point if the tool found a counterexample using an external adversarial attack technique, and 10 points if the tool found a counterexample using its core search algorithm. It is difficult for us to determine how a tool solves individual SAT instances, so we simply assign 1 point for correct falsification results as our experiments in §7.2.1 show that most SAT instances were solved using adversarial attacks.

Tab. 4 shows the results. Columns # and **tool** show the rankings of the tools. Note that for some tool do not work on certain benchmarks and therefore are not shown (e.g., for MNISTFC, MN-BaB has errors for all problems). The next two columns give the **scores** and **percent**, computed by the score of the tool divided by the highest score (thus the tool with the highest score always has 100%). The last three columns give additional statistics: the number of instances that a tool **verified** or **falsified**, and the number of those that the tool ran the **fastest** - tools with runtimes within 0.2 seconds of each other are considered tied.

Across these benchmarks NeuralSAT ranks second to \(\alpha\)-\(\beta\)-CROWN, which was the top performer in VNN-COMP'22 and thus the state-of-the-art. It trails \(\alpha\)-\(\beta\)-CROWN both in the number of problems verified and in the speed of verification, though it can falsify as many problems as any other verifier across the benchmark.

A number of verifiers, e.g., Marabou'21 and nennum, exhibit good performance on benchmarks with small networks - **MNISTFC** and **ACAS Xu** - and outperform NeuralSAT. Our goal in developing NeuralSAT was to explore the potential for scaling constraint-based DNN verification and NeuralSAT's performance on the **CIFAR2020** and **RESNET** benchmarks, which have networks with an order of magnitude more neurons, indicates the potential of the technique. While it ranks
second to \(\alpha\)-\(\beta\)-CROWN across those benchmarks it falsifies only 1 fewer property (64/65) and verifies 5 fewer (191/196). We note that the developers of \(\alpha\)-\(\beta\)-CROWN tuned 10 hyperparameters on average for each benchmark to optimize its performance. In contrast, NeuralSAT has no hyperparameters which suggests that its performance on large models may generalize better in practice.

Compared to the other tools, NeuralSAT ranks _second_ to and solves 97.7% of the large problem instances solved by the state-of-the-art \(\alpha\)-\(\beta\)-CROWN.
### SAT vs. Unsat instances

We show more details for the results presented in SS7.1, focusing on the performance of tools for sat and unsat instances. Tab. 5 lists the runtime of each tool for each benchmark (median over 3 runs, as mentioned in SS6). Each benchmark has two rows showing unsat and sat results of each tools. The information given in these rows has the form **runtime** (# **problems solved**, # **problems unsolved**). For example, for ACAS Xu, NeuralSAT took 551.5s, solved 136 unsat instances, and failed 3 unsat instances. The mark - indicates the tool fails to run the benchmark (e.g., both Marabou'21 and Marabou'22 cannot run CIFAR2020).

#### 7.2.1. SAT instances

As shown in Tab. 5, tools are more successful in solving sat than unsat instances (i.e., the number of unsolved sat instances are often 0 or few for most tools). We also found that using external adversarial attacks or random counterexample generation as a quick and cheap way to find satisfying assignment is highly effective as expected. For example, out of the 136 sat instances NeuralSAT successfully solved 134, all of which were solved using these quick techniques. We observe this behavior consistently across all tools on all benchmarks.

Example of difficult SAT instances (i.e., cannot be solved easily using these random or attack methods) include properties 7 and 8 of ACAS Xu. Both \(\alpha\)-\(\beta\)-CROWN and Marabou'21 timed out for

\begin{table}
\begin{tabular}{l|l|l l l|r r} \hline \hline
**BMs** & **\#** & **Tool** & **Score** & **\%** & **Falsif.** & **Fast.** \\ \hline \multirow{8}{*}{**Courtesy**} & 1 & NeuralSAT & 366 & 100.0\% & 134 & 104 \\  & 2 & \(\alpha\)-\(\beta\)-CROWN & 341 & 93.2\% & 133 & 87 \\  & 3 & ERAN & 233 & 63.7\% & 134 & 32 \\  & 4 & MN-BaB & 184 & 50.3\% & 105 & 31 \\  & 5 & Marabou’22 & 90 & 24.6\% & 58 & 1 \\  & 6 & Marabou’21 & 87 & 23.8\% & 66 & 3 \\  & 7 & nnenum & 80 & 21.9\% & 71 & 2 \\ \hline \hline \end{tabular}
\end{table}
Table 6. VNN-COMP results for sat instances

\begin{table}
\begin{tabular}{c|c|c c c c c c} \hline \hline
**BM** & **Networks** & **NeuralSAT** & **EBM** & **NN-BaB** & **Marabou’21** & **Marabou’22** & **nnenum** & \(\alpha\)-\(\beta\)**-CROWN** \\ \hline \multirow{3}{*}{ACAS Xu} & \multirow{3}{*}{45 FNNs} & 551.5 (136, 3) & 3867.8 (133, 6) & 1251.0 (105, 34) & 321.1 (138, 1) & 533.4 (85, 54) & 233.5 (139, 0) & 335.5 (139, 0) \\  & & 63.9 (47, 0) & 811.9 (45, 2) & 339.0 (47, 0) & 75.4 (46, 1) & 172.8 (41, 6) & 62.9 (47, 0) & 132.1 (46, 1) \\ \hline \multirow{8}{*}{MNISTFC} & \multirow{3}{*}{MNIST\_256x4} & 15.2 (18, 0) & 315.0 (18, 0) & - & 78.4 (17, 1) & 430.7 (14, 4) & 150.1 (17, 1) & 74.6 (18, 0) \\  & & 10.6 (12, 0) & 67.6 (12, 0) & - & 66.0 (12, 0) & 85.0 (12, 0) & 89.6 (12, 0) & 1.5 (11, 1) \\ \cline{1-1} \cline{2-9}  & & 15.4 (7, 13) & 303.8 (10, 10) & - & 172.6 (10, 10) & 30.8 (7, 13) & 163.4 (11, 9) & 783.3 (20, 0) \\ \cline{1-1}  & & 5.3 (6, 0) & 8.9 (6, 0) & - & 66.9 (6, 0) & 346.3 (5, 1) & - & 1.1 (6, 0) \\ \cline{1-1} \cline{2-9}  & & 19.7 (8, 0) & 18.0 (8, 0) & - & 42.9 (8, 0) & 50.2 (8, 0) & 26.3 (8, 0) & 407.9 (16, 0) \\ \cline{1-1}  & & 4.6 (5, 0) & 11.0 (5, 0) & - & 16.2 (2, 3) & - & - & 1.1 (5, 0) \\ \hline \multirow{8}{*}{CIFAR2020} & \multirow{3}{*}{CIFAR10\_255} & 726.1 (65, 0) & 784.9 (51, 14) & 820.9 (65, 0) & - & - & - & 2252 (65, 0) \\  & & 15.9 (13, 0) & 48.8 (13, 0) & 274.3 (11, 2) & - & - & - & 173.3 (10, 0) \\ \cline{1-1} \cline{2-9}  & & 331.9 (30, 0) & 1170.4 (21, 9) & 380.7 (28, 2) & - & - & 1238.4 (16, 14) & 253.7 (30, 0) \\ \cline{1-1}  & & 24.1 (20, 2) & 90.9 (22, 0) & 87.1 (17, 5) & - & - & 1730.7 (12, 10) & 26.9 (21, 1) \\ \cline{1-1} \cline{2-9}  & & 940.7 (53, 0) & 813.4 (42, 11) & 668.7 (49, 4) & - & - & - & 349.6 (53, 0) \\ \cline{1-1}  & & 9.9 (8, 0) & 33.3 (8, 0) & 97.6 (7, 1) & - & - & - & 9.9 (8, 0) \\ \hline \multirow{2}{*}{RESNET\_A} & \multirow{2}{*}{3B2\_ADV} & 383.7 (17, 3) & 132.0 (8, 12) & 177.6 (13, 7) & - & - & - & 438.4 (20, 0) \\  & & 14.6 (12, 0) & 47.8 (12, 0) & 14.0 (12, 0) & - & - & - & 27.6 (12, 0) \\ \hline \multirow{2}{*}{RESNET\_B} & \multirow{2}{*}{3B2\_SSADV} & 678.4 (26, 2) & 405.2 (16, 12) & 302.1 (21, 7) & - & - & - & 335.0 (28, 0) \\  & & 13.5 (11, 0) & 31.4 (11, 0) & 12.5 (11, 0) & - & - & - & 25.6 (11, 0) \\ \hline \hline \end{tabular}
\end{table}
Table 5. Results for sat and unsat instances. Time are wall-clock and in seconds. Each benchmark has two rows listing runtime (solved, unsolved) results for unsat and sat instances. - means the tool cannot run the benchmark.
property 7 (but NeuralSAT solved it). NeuralSAT took around 34s over multiple DPLL(T) iterations to find a counterexample for property 8. In general, the effectiveness of falsification is mainly due to external techniques, and not part of the main algorithm of DNN verification tool (this explains why most modern tools, including NeuralSAT, runs these external techniques initially).

Tab. 6 shows the VNN-COMP rankings over sat instances. Here, NeuralSAT ranked first, \(\alpha-\beta-\)CROWN second, and ERAN third. While all three tools was able to solve similar sat instances (133 and 134), NeuralSAT appears to solve them quicker (104 instances) and therefore had the most points. This is rather surprising as we, just like other tools, mainly rely on external adversarial techniques to generate counterexamples as described in SS4.

#### 7.2.2. Unsat instances

Unlike sat instances that can be effectively handled by external techniques, unsat instances truly exercise the power of DNN verification algorithms. As shown in Tab. 5, solving unsat instances often take more time and result in more unsolved results.

Both nnenum and Marabou'21 were heavily optimized for networks with small input dimensions. These tools performed well for ACAS Xu networks, e.g., nnenum solved all 139 unsat instances in ACAS Xu and while Marabou'21 solved 1 fewer unsat instances, it has the most fastest solved instances for ACAS Xu. However, these tools failed to run on the larger benchmarks CIFAR2020 or RESNET_A/_B. Note that \(\alpha-\beta-\)CROWN, NeuralSAT, ERAN also perform well in ACAS Xu because they all have heuristics in some way to leverage low dimension inputs.

MNISTFC is difficult and has 10 unsat instances that no tool can solve. \(\alpha-\beta-\)CROWN used a MILP solver in a preprocessing step to tighten the bounds of all hidden neurons. This helps \(\alpha-\beta-\)CROWN to solve 20 difficult unsat instances on larger MNIST_256x4 and MNIST_256x6 networks that other tools failed. For other benchmarks CIFAR2020 and RESNET_A/B, \(\alpha-\beta-\)CROWN ranked first and NeuralSAT followed closely (solved 2 fewer unsat CIFAR2020 instances and 5 fewer RESNET). It is worth recalling that \(\alpha-\beta-\)CROWN has custom run scripts that on average tuned 10 hyperparmeters for each benchmark.

Tab. 7 shows the VNN-COMP rankings over unsat instances. Here, \(\alpha-\beta-\)CROWN ranked first, NeuralSAT second, and ERAN third. Marabou'21 and Marabou'22 ranked last because they fail to run many benchmarks. In summary, for unsat, the overall ranking is consistent with the overall VNN-COMP ranking given in Tab. 4.

### Comparison with DPLL(T)-based DNN verification

The state-of-the-art in DPLL(T)-based DNN verification is Marabou. It improves on Reluplex, incorporates abstraction and deduction techniques, and has been entered in VNN-COMP'22 in recent years. This makes it a reasonable point of comparison for NeuralSAT especially in understanding the benefit of the addition of CDCL on the scalability of DNN verification.

Overall both versions of Marabou ranked poorly. While Marabou'21 is the best performer for ACAS Xu, which consists of networks with low input dimensions, it does not scale for larger benchmarks and often either cannot handle such networks (CIFAR2020, RESNET_A/B) or ranked last compared to other tools (MNIST). Below we consider the case of smaller and larger networks separately.

_Small networks._ ACAS Xu networks are small in two ways. First, they have very few neurons (300). Second, they only have 5 input dimensions. Marabou'21 employs multiple optimizations to target the scale of these networks. For example, a variant of the Split and Conquer algorithm (Wu et al., 2020) subdivides the input space to generate separate verification problems. Partitioning a 5 dimensional input space is one thing, but the number of partitions grows exponentially with input dimension and this approach is not cost effective for the other networks in the benchmarks.
Tab. 5 shows how for MNIST networks with larger input dimension (784) the performance of Marabou degrades with increasing number of neurons. As the network sizes increase the number of problems solved by Marabou'21 decreases - from 29, to 16, and then to 10. There is a similar reduction in problems solved, from 30 to 13, for NeuralSAT going from the 512 neuron MNIST network to the 1024 neuron network, but then there is no reduction in problems solved going from the 1024 to the 1536 neuron networks. This is due to the fact that the parameters of the 1536 neuron network define a set of theory constraints that can be efficiently over-approximated. In fact, NeuralSAT only takes a single iteration to prove this property and, consequently, other algorithmic features of NeuralSAT, such as CDCL, do not have a chance to show their benefit.

_Larger Networks._ Marabou could not scale to any of the larger CIFAR2020 or RESNET problems, so a direct comparison with NeuralSAT is not possible. Instead, we observe that NeuralSAT performed well on these problems - ranking better than it did on the smaller problems. We conjecture that this is because problems of this scale give ample time for clause learning and CDCL to significantly prune the search performed by DPLL(T). Evidence for this can be observed in data on the learned clauses recorded during runs of NeuralSAT on unsat problems. Since NeuralSAT's propositional encodings have a number of variables proportional to the number of neurons (\(n\)) in the network the effect of a learned clause of size \(c\) is that it has the potential to block a space of assignments of size \(2^{n-c}\). In other words, as problems grow the reduction through CDCL grows combinatorially. In the largest problem in the benchmarks, with \(n=62464\) we see clauses on average of size \(c=16\) which allows BCP to prune an enormous space of assignments - of size \(2^{62448}\). The ability of NeuralSAT to scale well beyond other DPLL(T) approaches to DNN verification suggests that other constraint-based DNN verification approaches may want to incorporate CDCL.

## 8. Related Work

The literature on DNN verification is rich and is steadily growing (cf. (Liu et al., 2021; Urban and Mine, 2021)). Here we summarize well-known techniques with tool implementations.

**Constraint-based** approaches such as DLV (Huang et al., 2017), Planet (Ehlers, 2017), and Reluplex (Katz et al., 2017) and its successor Marabou (Katz et al., 2022, 2019) transform DNN verification into a constraint problem, solvable using an SMT (Planet, DLV) or DPLL-based search with a customized simplex and MILP solver (Reluplex, Marabou) solvers. **Abstraction-based** techniques and tools such as AI\({}^{2}\)(Gehr et al., 2018), ERAN (Muller et al., 2021; Singh et al., 2018, 2019) (DeepZ (Singh et al., 2018), RefineZono (Singh et al., 2018), DeepPoly (Singh et al., 2019), K-ReLU (Singh et al., 2019)), MN-BaB (Ferrari et al., 2022)), Reluval (Wang et al., 2018), Neurify (Wang et al., 2018), VeriNet (Henriksen and Lomuscio, 2020), NNV (Tran et al., 2021), nnenum (Bak, 2021; Bak et al., 2020), CROWN (Zhang et al., 2018), \(\alpha\)-\(\beta\)-CROWN (Wang et al., 2021), use abstract domains such as interval (Reluval/Neurify), zonotope (DeepZ, nnenum), polytope (DeepPoly), starset/imagestar (NNV, nnenum) to scale verification. OVAL (OVAL-group, 2023) and DNNV (Shriver et al., 2021) are frameworks employing various existing DNN verification tools. Our NeuralSAT, which is most related to Marabou, is a DPLL(T) approach that integrates clause learning and abstraction in theory solving.

Well-known **abstract domains** for DNN verification include interval, zonotope, polytope, and starset/imagestar. Several top verifiers such as ERAN, MN-BaB and nnenum use multiple abstract domains (e.g., ERAN uses zonotope and polytope, nnenum adopts deeply, zonotope and imagestar. The work in (Goubault et al., 2021) uses the general max-plus abstraction (Heidergott et al., 2006) to represent the non-convex behavior of ReLU. NeuralSAT currently uses polytope in its theory solver though it can also use other abstract domains.
Modern SAT solvers benefit from effective heuristics, e.g., VSIDS and DLIS strategies for decision (branching), random restart (Moskewicz et al., 2001) and shortening (Chinneck and Dravnieks, 1991) or deleting clauses (Moskewicz et al., 2001) for memory efficiency and avoiding local maxima caused by greedy strategies. Similarly, modern DNN verifiers such as nnenum, ERAN, \(\alpha-\beta-\)CROWN, and Marabou include many **optimizations** to improve performance, e.g., Branch-and-Bound (Bunel et al., 2020) and Split-and-Conquer (Katz et al., 2022, 2019; Wu et al., 2020) for parallelization, and various optimizations for abstraction refinement (Bak, 2021; Singh et al., 2018)) and bound tightening (Bak, 2021; Katz et al., 2019; Wang et al., 2021). NeuralSAT has many opportunities for improvements such as new decision heuristics and parallel DPLL(T) search algorithms (SS9).

## 9. Conclusion and Future Work

We introduce NeuralSAT, a DPLL(T) approach and prototype for DNN verification. NeuralSAT includes the standard DPLL components such as clause learning and backtracking and a theory solver for DNN reasoning. We formalize NeuralSAT DPLL(T) using conditional transition rules and evaluate the NeuralSAT prototype with standard FNNs, CNNs, and Resnets. Our evaluation shows that NeuralSAT is competitive to the state-of-the-art DNN verification tools.

We have many opportunities to improve the performance of NeuralSAT. For example, we plan to develop a native parallel DPLL(T) approach to exploit multiprocessing and exploring new decision heuristics and backtracking strategy for NeuralSAT (e.g., the first UIP strategy used in the CHAFF solver (Moskewicz et al., 2001) has been shown to create fewer clauses and have more effective backtracking in real-world scenarios(Marques-Silva et al., 2021) By using DPLL with implication graphs, NeuralSAT inherits a native mechanism to verify its own results, e.g., using these graphs and conflicting clauses to obtain resolution graphs/proofs and unsat cores as proofs of unsatisfiability (Asin et al., 2008; Kroening and Strichman, 2016; Zhang and Malik, 2003).
