# Safe Reinforcement Learning with Probabilistic
Control Barrier Functions for Ramp Merging

Soumith Udatha  Yiwei Lyu  John Dolan

###### Abstract

Prior work has looked at applying reinforcement learning and imitation
learning approaches to autonomous driving scenarios, but either the safety or
the efficiency of the algorithm is compromised.With the use of control barrier
functions embedded into the reinforcement learning policy, we arrive at safe
policies to optimize the performance of the autonomous driving vehicle.
However, control barrier functions need a good approximation of the model of
the car. We use probabilistic control barrier functions as an estimate of the
model uncertainty. The algorithm is implemented as an online version in the
CARLA (Dosovitskiy et al., 2017) Simulator and as an offline version on a
dataset extracted from the NGSIM Database. The proposed algorithm is not just
a safe ramp merging algorithm, but a safe autonomous driving algorithm applied
to address ramp merging on highways.

Safe Reinforcement Learning

##  1 Introduction

It is a well-known fact that real-word dynamics are more complicated than can
be easily modeled in an analytical form in simulators (AbuAli & Abou-zeid,
2016). This disparity between the real dynamics and the approximations
involved becomes more prominent when dealing with safety-critical systems. To
determine safety of a system we need to have a good idea of the world dynamics
involved.
The interaction of self-driving cars with other human drivers can be treated
as a safety-critical system.(Lyu et al., 2021). In the area of autonomous
vehicle control and planning (Gu et al., Ames et al., Luo et al.), safety is
always the primary focus. Ramp merging is a typical, relatively simple
scenario where autonomous vehicles interact with humans. Even for a simple
driving scenario, freeway on-ramp merging areas are high-risk areas for motor
vehicle crashes and conflicts due to the variety of driving styles (El abidine
Kherroubi et al., 2021). Human drivers introduce uncertainty into merge
scenarios, and Autonomous Vehicles (AV) will collide if they can’t plan and be
controlled safely (Zhu & Tasic, 2021). It is therefore important that we
address model uncertainty while modeling the control and planning of self-
driving cars.
In situations with rule-based systems designed to adhere to various driver
behaviors on a highway, strictly following the rules to maintain safety could
result in unsafe situations, where the autonomous vehicle might brake for an
instant when going very close to a vehicle, which may not be anticipated by
the human drivers of the tailgating vehicles, leading to collision (Zheng et
al., 2011). The efficiency and solution feasibility of rule-based systems
become even worse (Prakken, 2017) in situations with model uncertainty. Hence,
we need to take human behavior into account along with model uncertainty for
better safety guarantees.
We closely study a highway on-ramp merging scenario, where the goal is to
enable the AV to merge with human-driven cars safely and efficiently. Our main
contributions are in extending and providing a reinforcement learning (RL)
pipeline with probabilistically safe constrained barrier functional safety
(Luo et al., 2020)(Lyu et al., 2021)(Ames et al., 2019b) which can be extended
to any self-driving task in a simulation domain by changing the task-based
reward function. We perform experiments in CARLA (Dosovitskiy et al.) and an
offline training procedure on the NGSIM dataset for a one-on-one ramp merging
case. The emphasis of the paper is not on proposing a novel RL algorithm for
autonomous cars, but on addressing the problem of model uncertainty with
Control Barrier Functions (CBFs) (Ames et al. 2019b) combined with a RL
pipeline to extend the research on safe RL for both offline and online
environments.

##  2 Related Work

CBF-based methods (Ames et al. 2019b, Ames et al. 2017, Notomista et al. 2020,
Lindemann et al. 2021) are being increasingly used in the control application
domain due to their safety guarantees with the forward-invariant property when
a solution is feasible. In reality,a solution may not always be feasible as we
deal with approximations of complex non-linear dynamics and the systems resort
to hard-coded recovery control (Wang et al., 2017).
To address model uncertainty, several works (Notomista et al., 2020)(Khojasteh
et al., 2020) proposed to employ the CBF approach with noisy system dynamics.
Integrating CBF with Model Predictive Control (MPC) is also a common planning
method. (Zeng et al., 2020) and (Son & Nguyen, 2019) introduced MPC-based
safety-critical control. However, these works fail to take different driving
behavior styles into account. To address this problem, one possible solution
is to use CBFs with reinforcement learning-based methods, where the agent
trains for all the possible kinds of behaviors, given enough training data and
even a black-box model. RL-CLF-CBFs proposed in (Choi et al., 2020) is used to
reduce the uncertainty in plant dynamics. (Ma et al., 2021a) implemented an RL
algorithm with Constrained Policy Optimization (CPO) (Achiam et al., 2017) and
with the added safety of control barrier functions.
Generalized CBFs are introduced in (Ma et al., 2021b) to consider higher-order
dynamics, Parametric CBFs (Taylor & Ames, 2020) and Exponential CBFs (Nguyen &
Sreenath, 2016) are popular methods to model approximate higher-order
dynamics. In our work, we integrate Probabilistic CBFs (Clark, 2019)(Luo et
al., 2020)(Lyu et al., 2021) to model uncertainty owing to its ability to use
a simpler dynamics model and linear constraints for the optimization problem
compared to other methods. Ma et al. is closely relevant prior work, which
uses Generalized Discrete CBFs to generate safety certificates and combine
with a Model Based Policy Optimization (MBPO) (Janner et al., 2019) framework
for an intersection scenario. Although we have a similar RL pipeline to Ma et
al., ours is not a model-based approach and is similar to a CPO formulation.
Further, we also introduced a reinforcement learning approach to CARLA and an
offline NGSIM Dataset to show the generalization capabilities of our approach.

Figure 1:  Ramp merging scenario (Dong et al., 2017). The ego vehicle (green)
is the host vehicle; the merging vehicle (red) is the ego vehicle, running on
the ramp. The figure below shows a two-dimensional version of ramp-merging
that we will be using. The merge is along a curve rather than a straight line.

##  3 Problem Formulation

###  3.1 Setting up the problem and Dynamics

Ramp merging has previously been studied in one dimension. We have extended
the approach to two dimensions to include a wider range of ramp-merging
scenarios and easy generalization to other scenarios. The goal is to control
the ego vehicle on the ramp to merge safely with the human-driven vehicles
(host vehicles) already on the highway. The system dynamics of a vehicle can
be described by double integrators as follows, since acceleration plays a key
role in the safety considerations.

$\footnotesize\begin{split}\dot{X}&=\begin{bmatrix}\dot{x}\\\ \dot{y}\\\
\dot{v_{x}}\\\ \dot{v_{y}}\end{bmatrix}=\begin{bmatrix}0_{2\times
2}\;I_{2\times 2}\\\ 0_{2\times 2}\;0_{2\times
2}\end{bmatrix}\begin{bmatrix}x\\\ y\\\ v_{x}\\\
v_{y}\end{bmatrix}+\begin{bmatrix}0_{2\times 2}\;I_{2\times 2}\\\ I_{2\times
2}\;0_{2\times 2}\end{bmatrix}\begin{bmatrix}u_{x}\\\ u_{y}\\\ \epsilon_{x}\\\
\epsilon_{y}\end{bmatrix}\\\ \end{split}$ (1)

where
$x\in\mathcal{X}\subset\mathbb{R},y\in\mathcal{Y}\subset\mathbb{R},v\in\mathbb{R}^{2}$
are the position and linear velocity of each car respectively and
$u\in\mathbb{R}^{2}$ represents the acceleration control input.
$\epsilon\sim\mathcal{N}(\hat{\epsilon},\Sigma)$ is a random Gaussian variable
with known mean $\hat{\epsilon}\in\mathbb{R}^{2}$ and variance
$\Sigma\in\mathbb{R}^{2\times 2}$, representing the uncertainty in each
vehicle’s motion.

###  3.2 Probabilistic Control Barrier Functions

In (Lyu et al., 2021), an optimization framework with probabilistically safe
CBFs was proposed as an alternative to deterministic CBFs with perfect model
information to address motion uncertainty, specifically for ramp merging
scenarios in one dimension. Consider the admissible space equation for linear
CBF with parameter $\alpha$ of one dimension, x: $\dot{h}(x,u)+\alpha h(x)\geq
0$ with $h=(x_{e}-x_{m})^{2}-R_{safe}^{2}$. By substituting Eq. 1 we have:

$\dot{h}^{s}_{em}(x,u)+\alpha h^{s}_{em}(x)\geq 0;\implies 2\Delta
x_{em}^{T}\Delta\epsilon_{em}\geq-2\Delta x_{em}^{T}(\Delta v_{em}+u_{e}\Delta
t)-\alpha h^{s}_{em}(x)$ (2)

 where $\Delta x_{em}=x_{e}-x_{m},\Delta
v_{em}=v_{e}-v_{m},\Delta\epsilon_{em}=\epsilon_{e}-\epsilon_{m}\sim\mathcal{N}(\Delta\hat{\epsilon}_{em},\Delta\Sigma_{em})$
for ego vehicle $e$ and each merging vehicle $m$, $\Phi^{-1}(\cdot)$ is the
inverse cumulative distribution function (CDF) of the standard zero-mean
Gaussian distribution with unit variance. We reorganize
$\Pr\Big{(}\dot{h}^{s}_{em}(x,u)+\alpha h^{s}_{em}(x)\geq 0\Big{)}\geq\eta$
into the form of $\Pr(a^{T}c\leq b)\geq\eta\Leftrightarrow
b-\bar{a}^{T}c\geq\Phi^{-1}(\eta)||\Sigma^{1/2}c||^{2}$ from Blackmore et al.
with $a=\Delta\epsilon_{em},c=-2\Delta x_{em},b=2\Delta x_{em}^{T}(\Delta
v_{em}+u_{e}\Delta t)+\alpha h^{s}_{em}(x)$ and eventually get a constraint:
$\footnotesize A_{em}u_{x}\leq b_{em},\quad A_{em}\in\mathbb{R}^{1\times
2},b_{em}\in\mathbb{R}$ with

$A_{em}=-2\Delta x_{em}^{T}\Delta t;\text{ }b_{em}=2\Delta x_{em}^{T}(\Delta
v_{em}+\Delta\hat{\epsilon}_{em})+\alpha
h^{s}_{em}(x)-\Phi^{-1}(\eta)\sqrt{\Delta x_{em}^{T}\Delta\Sigma_{em}\Delta
x_{em}}$ (3)

where $\Delta t$ is a time unit. We derived linear control constraints for
pairwise chance-constrained safety between ego vehicle and each merging
vehicle $m$. The equations in (3) can be extended to the y-dimension as well
for 2-dimensional decoupled CBFs. For a more detailed derivation, we refer the
reader to Lyu et al. ∎

###  3.3 Reinforcement Learning with Probabilistically Safe CBFs

For better safety guarantees, we use a reinforcement learning policy to
compute high-level desired nominal velocity and choose a CBF control as
output. However, it is computationally expensive to solve two different
optimization problems while interacting with a simulator. Our constrained RL
framework solves it with a single constrained optimization with linear
probabilistic safety certificates. Using the optimization framework defined in
Achiam et al. for constrained RL problems, we extend the constraints obtained
in both dimensions from 3.2 for the total return objective, $\mathcal{G}$, and
set of safe states, $\mathcal{C}$, as:

Figure 2: Reinforcement Learning Pipeline: We initialize rollouts from random
initial states and run an optimization on the set of collected trajectories to
train a policy for each epoch.

$\footnotesize\begin{split}&\min_{\theta}L_{a}={\mathbb{E}_{a_{\sim}\pi,s_{\sim}C}}[\mathcal{G}]\\\
s.t\quad&{U}_{min}\leq u_{e}\leq{U}_{max}\\\
&J_{c_{x}}=\mathbb{E_{u_{e}\sim\pi}}[A_{em_{x}}u_{e_{x}}]\leq b_{em_{x}}\\\
&J_{c_{y}}=\mathbb{E_{u_{e}\sim\pi}}[A_{em_{y}}u_{e_{y}}]\leq b_{em_{y}}\\\
&D_{p}(\theta,\theta_{k})=\frac{1}{2}\Delta\theta^{T}H\Delta\theta\leq\delta\end{split}$
(4)

Using RL objective in Eq. 4, we use the approximate actor-critic constrained
policy gradient formulation in (Ma et al., 2021a) to solve this optimization.
The critic objective is
$L(\phi)=E_{s_{t}\sim\mathcal{C}}[\frac{1}{2}(\mathcal{G}-V(s_{t},\phi))^{2}]$,
where $\phi$ is the parameters of the critic network and $V(s_{t},\phi)$ is
the critic’s state-dependent value function. The actor objective (Eq.4) is
optimized by transforming into a dual problem and applying KKT (Boyd &
Vandenberghe) conditions. The analytical optimal solution is
$\Delta\theta^{*}=\frac{H^{-1}(g-C\nu^{*})}{\lambda^{*}}$, where $\theta$ is
the actor parameters, $\lambda^{*},\nu^{*}$ are dual variables, H is the
hessian from the trust region condition,
$g=\frac{dL_{a}}{\partial\theta}/||\frac{dL_{a}}{\partial\theta}||^{2}$, and
$C=\frac{dJ}{\partial\theta}/||\frac{dJ}{\partial\theta}||^{2}$, combining
both $J_{x}$ and $J_{y}$. If there is no feasible solution, an iterative line
search method is applied using
$\theta_{k+1}=\theta_{k}+-\sqrt{\frac{2*\delta}{C^{\mathbb{T}}H^{-1}C}}H^{-1}C$.
A more detailed derivation can be found in the appendix (B). From the RL
pipeline in Fig. 2, we use multiple rollouts sampled from various initial
states, similar to Janner et al. (2019), to capture the uncertainty in the
environment and to generalize to a larger section of the state space.
Algorithm 1 gives the pseudocode for our method, Safety Assured Policy
Optimization for Ramp Merging (SAPO-RM).

Algorithm 1 SAPO-RM

0: $\Delta x_{em},\Delta v_{em},\Delta t,R_{safe},{\alpha}$

0: $\theta,\phi$

repeat

Sample trajectories $\mathcal{D}=\mathcal{T}\sim\pi(\theta_{k})$

Compute Constraints in the objective

Estimate $\phi$ from $\mathcal{D}$

Calculate g,C,H

if feasible then

$\Delta\theta^{*}=\frac{H^{-1}(g+C\nu^{*})}{\lambda^{*}}$

else

$\theta_{k+1}=\theta_{k}+-\sqrt{\frac{2*\delta}{C^{\mathbb{T}}H^{-1}C}}H^{-1}C$

end if

until convergence

##  4 Experiments

###  4.1 CARLA

####  4.1.1 Setting up the Simulation Environment

We use CARLA (Dosovitskiy et al.) v.9.12 to modify the existing Town-06
environment to a ramp merging scenario. The scenario considered in Fig. 1 has
a curved ramp. We use a PID Controller to track the steering control of the
Ego Vehicle (On-Ramp) between waypoints generated by the default Global
Planner to the specified goal position. The control for the Host (Off-Ramp)
Vehicle uses both steering and longitudinal PID control. Further, the control
of the host vehicle is not reactive. This assumption deals with a conservative
case and satisfying this also maintains safety for the case where host control
is reactive to the ego vehicle. We optimize the safe reinforcement learning
objective (Eq.5) to learn a policy to control the ego-vehicle throttle
position.

####  4.1.2 Online Experiments on CARLA

We implemented SAPO-RM in the Simulator set-up in 4.1.1. The RL pipeline
introduced in Fig. 2 is followed, where the host vehicle is initialized at a
specified initial position with a random offset. If the host vehicle reaches
the destination before the ego vehicle, the host vehicle is re-initialized
with random offset. The simulation is terminated only when the ego vehicle
reaches the destination.The safety distance for the CBFs is 8m. Fig. 3 below
shows the results for SAPO-RM for a case where the target host velocity is 40
kph. Training parameters and results for other cases are discussed in the
appendix ( C).

Figure 3: Results for Online SAPO-RM: The host velocity is 40 kph, as seen in
the center image. The image on the left depicts the distance between the ego
and host vehicle.The image on the right is the output of the policy for the
evaluated case. From the plots of the ego control (Right) we observe that when
distance is close to $R_{safe}$, the throttle position goes to full-braking,
forcing the ego vehicle to maintain the safety condition. Whenever the
distance again increases, the ego control goes towards full throttle to
optimize performance.

###  4.2 NGSIM

####  4.2.1 Data Extraction

An offline dataset for US I-80 highway ramp-merging was extracted from the
NGSIM Database. We considered merging vehicles that go from on-ramp to an
auxiliary ramp. To ease the complexity, the dataset was simplified into a one-
on-one merging. The trajectories are first classified based on the condition:
distance between host and the ego vehicle is less than 12m in the auxiliary
lane. This condition leads to degenerate values as instances of freeway
oscillations are observed in real data (Zheng et al.). We constrained by
sorting the data of the ego vehicle with respect to the frame number and
considered the first case where the merging condition is satisfied. Further
dataset extraction details are in the appendix ( D).

####  4.2.2 Implementing Offline SAPO-RM

The offline dataset obtained in section 4.2.1 is then used to train the
offline SAPO-RM policy. Similar to the online case, a rollout is initialized
at a random state in the dataset. For each step in a rollout, only the
parameters of the ego vehicle are updated according to the dynamics equation
(Eq. 1). The vehicle heading direction ($\psi$) is used as a tracking
parameter for the ego vehicle. We used a rollout length of 4 and 5000
trajectories for each epoch of training the offline RL policy for 100 epochs.
In Fig. 4, we observe that the black trajectory (Ego policy) deviates from the
tracking control to maintain the safe distance.

Figure 4: The black trajectory is generated by a policy, the blue one is the
real host vehicle trajectory and the green one is the real ego vehicle
trajectory.

##  5 Conclusion and Future Work

We can clearly see from Figs. 3 and 4 that safety conditions are maintained by
ego-vehicles while performing ramp-merging.The algorithm we used here is not
just a ramp-merging algorithm but is a safe-reinforcement learning algorithm
applied to ramp-merging. By relieving some of the assumptions made on the
dynamics, the safe-RL algorithm can be extended to other scenarios of lane-
changing and intersections. We observe that trajectories maintain the safe
distance and are efficient with SAPO-RM. Possible future extensions are
extending to situations with more merging vehicles, introducing complicated
dynamics models (Lindemann et al., 2021), (Ge et al., 2020) for a better
approximation and to alleviate modeling uncertainty, understanding the effect
of $\alpha$ on SAPO-RM behavior, and implementing prior methods for the
offline approach and other implementations to compare other methods’ ability
to address modeling uncertainty.

## References

  * AbuAli & Abou-zeid (2016) AbuAli, N. and Abou-zeid, H.  Driver behavior modeling: Developments and future directions.  _Int. J. Veh. Technol._ , 2016:1–12, December 2016.
  * Achiam et al. (2017) Achiam, J., Held, D., Tamar, A., and Abbeel, P.  Constrained policy optimization.  In Precup, D. and Teh, Y. W. (eds.), _Proceedings of the 34th International Conference on Machine Learning_ , volume 70 of _Proceedings of Machine Learning Research_ , pp. 22–31. PMLR, 06–11 Aug 2017.  URL https://proceedings.mlr.press/v70/achiam17a.html.
  * Ames et al. (2014) Ames, A. D., Grizzle, J. W., and Tabuada, P.  Control barrier function based quadratic programs with application to adaptive cruise control.  In _53rd IEEE Conference on Decision and Control_ , pp. 6271–6278, 2014.
  * Ames et al. (2017) Ames, A. D., Xu, X., Grizzle, J. W., and Tabuada, P.  Control barrier function based quadratic programs for safety critical systems.  _IEEE Transactions on Automatic Control_ , 62(8):3861–3876, 2017.
  * Ames et al. (2019a) Ames, A. D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., and Tabuada, P.  Control barrier functions: Theory and applications.  In _2019 18th European Control Conference (ECC)_ , pp. 3420–3431. IEEE, 2019a.
  * Ames et al. (2019b) Ames, A. D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., and Tabuada, P.  Control barrier functions: Theory and applications, 2019b.  URL https://arxiv.org/abs/1903.11199.
  * Blackmore et al. (2011) Blackmore, L., Ono, M., and Williams, B. C.  Chance-constrained optimal path planning with obstacles.  _IEEE Transactions on Robotics_ , 27(6):1080–1094, 2011.
  * Boyd & Vandenberghe (2004) Boyd, S. and Vandenberghe, L.  _Convex Optimization_.  Cambridge University Press, 2004.  doi: 10.1017/CBO9780511804441.
  * Choi et al. (2020) Choi, J., Castañeda, F., Tomlin, C. J., and Sreenath, K.  Reinforcement learning for safety-critical control under model uncertainty, using control lyapunov functions and control barrier functions, 2020\.
  * Clark (2019) Clark, A.  Control barrier functions for complete and incomplete information stochastic systems.  In _2019 American Control Conference (ACC)_ , pp. 2928–2935, 2019\.  doi: 10.23919/ACC.2019.8814901.
  * Dong et al. (2017) Dong, C., Dolan, J. M., and Litkouhi, B.  Intention estimation for ramp merging control in autonomous driving.  In _IEEE 28th Intelligent Vehicles Symposium (IV’17)_ , pp. 1584 – 1589, June 2017.
  * Dosovitskiy et al. (2017) Dosovitskiy, A., Ros, G., Codevilla, F., López, A. M., and Koltun, V.  CARLA: an open urban driving simulator.  _CoRR_ , abs/1711.03938, 2017.  URL http://arxiv.org/abs/1711.03938.
  * Duan et al. (2022) Duan, J., Liu, Z., Li, S. E., Sun, Q., Jia, Z., and Cheng, B.  Adaptive dynamic programming for nonaffine nonlinear optimal control problem with state constraints.  _Neurocomputing_ , 484:128–141, 2022.  ISSN 0925-2312.  doi: https://doi.org/10.1016/j.neucom.2021.04.134.  URL https://www.sciencedirect.com/science/article/pii/S0925231221015848.
  * El abidine Kherroubi et al. (2021) El abidine Kherroubi, Z., Aknine, S., and Bacha, R.  Novel decision-making strategy for connected and autonomous vehicles in highway on-ramp merging.  _IEEE Transactions on Intelligent Transportation Systems_ , pp. 1–13, 2021.  doi: 10.1109/TITS.2021.3114983.
  * Ge et al. (2020) Ge, Q., Li, S. E., Sun, Q., and Zheng, S.  Numerically stable dynamic bicycle model for discrete-time control, 2020\.  URL https://arxiv.org/abs/2011.09612.
  * Gu et al. (2015) Gu, T., Atwood, J., Dong, C., Dolan, J. M., and Lee, J.-W.  Tunable and stable real-time trajectory planning for urban autonomous driving.  In _Intelligent Robots and Systems (IROS), IEEE/RSJ International Conference on_ , pp. 250–256. IEEE, 2015.
  * Janner et al. (2019) Janner, M., Fu, J., Zhang, M., and Levine, S.  When to trust your model: Model-based policy optimization, 2019.  URL https://arxiv.org/abs/1906.08253.
  * Khojasteh et al. (2020) Khojasteh, M. J., Dhiman, V., Franceschetti, M., and Atanasov, N.  Probabilistic safety constraints for learned high relative degree system dynamics.  In _Learning for Dynamics and Control_ , pp. 781–792. PMLR, 2020\.
  * Lindemann et al. (2021) Lindemann, L., Robey, A., Jiang, L., Tu, S., and Matni, N.  Learning robust output control barrier functions from safe expert demonstrations.  _ArXiv_ , abs/2111.09971, 2021.
  * Luo et al. (2016) Luo, W., Chakraborty, N., and Sycara, K.  Distributed dynamic priority assignment and motion planning for multiple mobile robots with kinodynamic constraints.  In _American Control Conference (ACC), 2016_ , pp. 148–154. IEEE, 2016.
  * Luo et al. (2020) Luo, W., Sun, W., and Kapoor, A.  Multi-robot collision avoidance under uncertainty with probabilistic safety barrier certificates.  _Advances in Neural Information Processing Systems_ , 33, 2020.
  * Lyu et al. (2021) Lyu, Y., Luo, W., and Dolan, J. M.  Probabilistic safety-assured adaptive merging control for autonomous vehicles.  In _2021 IEEE International Conference on Robotics and Automation (ICRA)_ , pp. 10764–10770, 2021.  doi: 10.1109/ICRA48506.2021.9561894.
  * Ma et al. (2021a) Ma, H., Chen, J., Eben, S., Lin, Z., Guan, Y., Ren, Y., and Zheng, S.  Model-based constrained reinforcement learning using generalized control barrier function.  In _2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)_ , pp. 4552–4559, 2021a.  doi: 10.1109/IROS51168.2021.9636468.
  * Ma et al. (2021b) Ma, H., Zhang, X., Li, S. E., Lin, Z., Lyu, Y., and Zheng, S.  Feasibility enhancement of constrained receding horizon control using generalized control barrier function.  In _2021 4th IEEE International Conference on Industrial Cyber-Physical Systems (ICPS)_ , pp. 551–557, 2021b.  doi: 10.1109/ICPS49255.2021.9468220.
  * Nguyen & Sreenath (2016) Nguyen, Q. and Sreenath, K.  Exponential control barrier functions for enforcing high relative-degree safety-critical constraints.  In _2016 American Control Conference (ACC)_ , pp. 322–328, 2016\.  doi: 10.1109/ACC.2016.7524935.
  * Notomista et al. (2020) Notomista, G., Wang, M., Schwager, M., and Egerstedt, M.  Enhancing game-theoretic autonomous car racing using control barrier functions.  In _IEEE International Conference on Robotics and Automation (ICRA)_ , pp. 5393–5399, 2020.
  * Prakken (2017) Prakken, H.  On the problem of making autonomous vehicles conform to traffic law.  _Artif. Intell. Law_ , 25(3):341–363, September 2017.
  * Son & Nguyen (2019) Son, T. D. and Nguyen, Q.  Safety-critical control for non-affine nonlinear systems with application on autonomous vehicle.  In _IEEE 58th Conference on Decision and Control (CDC)_ , pp. 7623–7628, 2019.
  * Taylor & Ames (2020) Taylor, A. J. and Ames, A. D.  Adaptive safety with control barrier functions.  In _2020 American Control Conference (ACC)_. IEEE, jul 2020.  doi: 10.23919/acc45564.2020.9147463.  URL https://doi.org/10.23919%2Facc45564.2020.9147463.
  * Wang et al. (2017) Wang, L., Ames, A. D., and Egerstedt, M.  Safety barrier certificates for collisions-free multirobot systems.  _IEEE Transactions on Robotics_ , 33(3):661–674, 2017.
  * Zeng et al. (2020) Zeng, J., Zhang, B., and Sreenath, K.  Safety-critical model predictive control with discrete-time control barrier function, 2020.
  * Zheng et al. (2011) Zheng, Z., Ahn, S., Chen, D., and Laval, J.  Freeway traffic oscillations: Microscopic analysis of formations and propagations using wavelet transform.  _Procedia Soc. Behav. Sci._ , 17:702–716, 2011.
  * Zhu & Tasic (2021) Zhu, J. and Tasic, I.  Safety analysis of freeway on-ramp merging with the presence of autonomous vehicles.  _Accid. Anal. Prev._ , 152(105966):105966, March 2021.

##  Appendix A Arriving at Probabilistic Safe Constraints

The chance-constrained optimization framework introduced in (Lyu et al., 2021)
to handle stochastic world dynamics can be extended into two dimensions, x and
y, explicitly in our implementation to accommodate uncertainty in the model
information. The equation below shows the CBF-QP with a probabilistic chance
constraint in one dimension:

$\footnotesize\begin{split}&\min_{u_{e}\in\mathcal{U}_{e}}||u_{e}-\bar{u}||^{2}\\\
s.t\quad&{U}_{min}\leq u_{e}\leq{U}_{max}\\\
&\Pr\Big{(}\dot{h}^{s}_{em}(x,u)+\alpha h^{s}_{em}(x)\geq
0\Big{)}\geq\eta,\qquad\forall m\end{split}$ (5)

where $\bar{u}$ is the nominal expected acceleration for the ego vehicle to
follow, and $U_{max}$ and $U_{min}$ are the ego vehicle’s maximum and minimum
allowed acceleration. $\text{Pr}(\cdot)$ denotes the probability of a
condition to be true. $\Pr\Big{(}\dot{h}^{s}_{em}(x,u)+\alpha
h^{s}_{em}(x)\geq 0\Big{)}\geq\eta\implies\Pr\Big{(}h^{s}_{em}(x)\geq
0\Big{)}\geq\eta$ given the forward invariance set theory in a deterministic
setting, $\dot{h}(x,u)+\alpha h(x)\geq 0\implies h(x)\geq 0$ as proved in
(Ames et al., 2019a) through a chance constraint.

From (Blackmore et al., 2011), a general chance constraint problem can be
transformed to a deterministic constraint as

$\footnotesize\begin{split}&\Pr(a^{T}c\leq
b)=\Phi(\frac{b-\bar{a}^{T}c}{\sqrt{c^{T}\Sigma c}})\\\
\implies&\Pr(a^{T}c\leq b)\geq\eta\Leftrightarrow
b-\bar{a}^{T}c\geq\Phi^{-1}(\eta)||\Sigma^{1/2}c||^{2}\end{split}$ (6)

##  Appendix B Constrained Policy Gradient Approximation

The Reinforcement Learning objective of the actor in Eq. 4 can be transformed
into a dual objective as:

$\footnotesize\begin{split}&\min_{\Delta\theta}g^{\mathbb{T}}\Delta\theta\\\
&s.t.\text{ }z+C^{T}\Delta\theta\leq 0\\\
&\tilde{D_{p}}\sim\frac{1}{2}\Delta^{\mathbb{T}}H\Delta\theta\leq\delta\\\
\end{split}$ (7)

where
$g=\frac{dL_{a}}{\partial\theta}/||\frac{dL_{a}}{\partial\theta}||^{2}$,$C=\frac{dJ}{\partial\theta}/||\frac{dJ}{\partial\theta}||^{2}$,
$z=J_{c}-b_{m}$. Using a Lagrange multiplier, the Lagrangian function then is:

$\mathbf{L(\theta,\nu)}=g^{\mathbb{T}}\Delta\theta+\lambda(\frac{1}{2}\Delta\theta^{\mathbb{T}}H\Delta\theta-\delta)+\nu(z+C^{\mathbb{T}}\Delta\theta)$

$\lambda,\nu$ are dual variables. Using KKT Conditions (Boyd & Vandenberghe,
2004),we get the equations:

$\displaystyle\frac{\partial\mathbf{L}}{\partial\Delta\theta}=g+\lambda
H\Delta\theta+\nu C$
$\displaystyle\lambda(\frac{1}{2}\Delta\theta^{\mathbb{T}}H\Delta\theta-\delta)=0$
$\displaystyle\nu(z+C^{\mathbb{T}}\Delta\theta)=0$
$\displaystyle\lambda,\nu\geq 0$
$\displaystyle(\frac{1}{2}\Delta\theta^{\mathbb{T}}H\Delta\theta-\delta)\leq
0$ $\displaystyle(z+C^{\mathbb{T}}\Delta\theta)\leq 0$

solving which, an optimal update direction can be obtained. If there is a
feasible solution, the optimal update direction is

$\Delta\theta^{*}=\frac{H^{-1}(g-C\nu^{*})}{\lambda^{*}}$

where $\nu^{*},\lambda^{*}$ are optimal dual variables. For the retrieval
update, we ignore the objective function and take the gradient descent with
respect to the constraints to force the policy back to the safety region.
Similar to (Achiam et al., 2017),
$\theta_{k+1}=\theta_{k}+-\sqrt{\frac{2*\delta}{C^{\mathbb{T}}H^{-1}C}}H^{-1}C$
is the retrieval policy.
The check for feasibility can be done by solving the optimization problem,
proposed in (Duan et al., 2022):

$\footnotesize\begin{split}&\min_{\Delta\theta}\Delta\theta^{T}H\Delta\theta\\\
&s.t.\text{ }z+C^{T}\Delta\theta\leq 0\\\ \end{split}$ (8)

If the optimal value of the optimization problem above is $\delta_{min}$, the
feasible solution set is empty if $\delta_{min}\geq\delta$ and contains a
solution otherwise. This problem is optimized efficiently using the Lagrangian
Dual Problem:

$\max_{\nu\geq 0}\frac{-\nu^{T}C^{T}H^{-1}C\nu}{2}+\nu^{T}z$

A feasibility check can be done by comparing $\delta_{min}$ with $\delta$.

##  Appendix C Running experiments with CARLA Environments

###  C.1 Training Parameters and Environment Setup

The state dimension is 37. Since we have to reproduce the entire state of an
initial state distribution, we save the positions, velocities, angular
velocities, throttle and steering positions in three dimensions of both the
ego and merging vehicle.The action dimension is 1, as we are only controlling
the throttle position. We use 100 trajectories with a rollout length of 20.
The actor policy has 2 MLP layers with a size of 256, and the critic is also
MLP of size 256. The parameter $\alpha$ is set to 0.75, the uncertainty
parameter $\eta$ is 0.99, and $\Delta t$ is 0.01. The reward function we use
is the negative weighted sum of error from the current position to the merging
position chosen on the Town-06 environment map and the error of the velocity
to the desired velocity. We used a desired velocity of 35 kmph for the ego-
vehicle. There are no bounds on the throttle position, other than the
specified range in Carla from [-1,1].

###  C.2 Variation with Host Velocity

We saw the results for the host velocity of 40 kph in section 4.1.2. In the
figure below, we can see the results with the cases where the host velocities
are 30 kph and 20 kph. From the Figures 5 & 6 below it is evident that the
minimum distance of 8m is respected with a range of initial conditions that we
train our policy on. However, once we step outside the training distribution,
we cannot guarantee that this will generalize.

Figure 5: Host velocity - 30 kmph

Figure 6: Host velocity - 20 kmph

###  C.3 Variation with $\alpha$ parameter of the CBF

In Figure 7, we repeat the experiment of the ramp merging case with Host
velocity 20 kph, as observed in Figure 6. With a higher value of alpha,
ideally we should observe more aggressive behavior, which is also the case
from the plots in Fig. 7. One main difference between the two versions is that
the merging agent waits before the merge for $\alpha=0.75$ and merges behind
the host vehicle. For the case with higher $\alpha$, the merging vehicle
accelerates from the beginning and would merge the host vehicle in front of
it.

Figure 7: Host velocity - 20 kmph and $\alpha$ = 15

##  Appendix D NGSIM Dataset Extraction

Of the possible 11,850,526 data points in the NGSIM Dataset we have extracted
a train, validation and test split of the merging dataset of about 100,000
data points of the merging trajectories for an one-on-one situation. The
figure below shows the trajectories of the merging condition we have applied
on the US I-80 highway dataset. We filter the ego vehicles that start in lane
7. Of the possible combinations to go to lane 5 and lane 6, we only consider
the case where vehicles merge into lane 6. For the host vehicles, we consider
the vehicles that are within a specified distance of 12m, when the ego vehicle
is merging into lane 6. We also sort the data in terms of frame numbers of ego
vehicles for time-based trajectories. The trajectories generated can be seen
in Figure 7. The network parameters of actor and critic, and the parameters of
$\alpha,\eta\text{ and}\Delta t$ are the same as that for the online case. The
reward function in this case is negative tracking error between the current
trajectory and the dataset trajectory for ego-vehicle. More results from
different initial positions are shown in Figure 8. We will report more results
on the average increase in distance and time performance gain on the dataset
in our future work.

Figure 8: Merging Dataset: It depicts all the trajectories extracted for the
I-80 dataset for one-on-one ramp merging.Trajectories in blue are that of the
host vehicle and in black are of the ego vehicle.

Figure 9: Offline Sapo RM: The results trajectories shown here compare the
green and black trajectories, which are the orignal trajectory in the dataset
and the RL policy trajectory respectively.

Figure 10: Observing Trajectory: On the image to the left we observe the
entire trajectory of Fig.4 and on the figure on the right we looked at a
zoomed in version to observe the same trajectory in more detail.As the figure
on the left has a different scale, it appears that the trajectories are very
sharp but with a detailed trajectory on the right, the change in the heading
direction of the car is not very sharp but rather an illusion of scale.


# Augment with Care: Contrastive Learning for the Boolean Satisfiability
Problem

Haonan Duan<EMAIL_ADDRESS>
University of Toronto. Vector Institute These authors contributed equally
Pashootan Vaezipoor11footnotemark: 1<EMAIL_ADDRESS>
University of Toronto. Vector Institute  Max B. Paulus<EMAIL_ADDRESS>
ETH Zürich  Yangjun Ruan<EMAIL_ADDRESS>
University of Toronto. Vector Institute  Chris J. Maddison
<EMAIL_ADDRESS>
University of Toronto. Vector Institute

###### Abstract

Supervised learning can improve the design of state-of-the-art solvers for
combinatorial problems, but labelling large numbers of combinatorial instances
is often impractical due to exponential worst-case complexity. Inspired by the
recent success of contrastive pre-training for images, we conduct a scientific
study of the effect of augmentation design on contrastive pre-training for the
Boolean satisfiability problem. While typical graph contrastive pre-training
uses label-agnostic augmentations, our key insight is that many combinatorial
problems have well-studied invariances, which allow for the design of label-
preserving augmentations. We find that label-preserving augmentations are
critical for the success of contrastive pre-training. We show that our
representations are able to achieve comparable test accuracy to fully-
supervised learning while using only 1% of the labels. We also demonstrate
that our representations are more transferable to larger problems from unseen
domains.

##  1 Introduction

Combinatorial problems, e.g., Boolean satisfiability (SAT) or mixed-integer
linear programming (MILP), have many applications in the industry and can
encode many fundamental computational tasks. These problems are NP-complete,
so solvers that perform efficiently in the worst case are not within reach.
However, learning can be used to improve the average complexity of solvers on
the population of combinatorial problems found in the wild (Nair et al.,
2020).

Supervised learning is a promising approach to combinatorial solver design
(e.g., Selsam and Bjørner, 2019; Nair et al., 2020). Unfortunately, the need
for labels is a severe limitation. Many read-world problems, such as
cryptography SAT instances, are extremely hard or, in some cases, even
impossible to solve (Nejati and Ganesh, 2019). Computing expert branching
labels for large-scale MILPs requires sophisticated parallel solvers (Nair et
al., 2020).

In order to scale learning for combinatorial problems, we ask: how much can we
learn from _unlabelled_ combinatorial instances? In this work, we consider a
contrastive learning approach, which begins by creating multiple “views” of
every unlabelled instance, a process called augmentation. An encoder is
trained to maximize the similarity between the representations of
augmentations that come from the same instance, while minimizing the
similarity between those of distinct ones (Chen et al., 2020a). This has been
successful in computer vision: contrastive representations can be used with
linear predictors to achieve competitive accuracies on ImageNet using a
fraction of the labelled instances (Chen et al., 2020a; He et al., 2020; Chen
et al., 2020b).

Our key insight is that combinatorial problems have well-studied invariances
that can be used to design extremely effective augmentations for contrastive
learning. Contrastive learning theory indicates that augmentations should be
(roughly) label-preserving in order to confer guarantees on downstream
prediction (Arora et al., 2019; Tosh et al., 2021; HaoChen et al., 2021). This
is in contrast to the majority of label-agnostic graph contrastive frameworks
(e.g., You et al., 2020; Hassani and Khasahmadi, 2020). For some combinatorial
problems, label-preserving transformations are available from subroutines of
existing solvers, e.g., variable elimination modifies SAT formulas while
preserving their satisfiability. Our augmentations produce new formulas by
randomly applying such satisfiability-preserving transformations. Crucially,
our augmentations do not require full solves and are much cheaper to compute
than the labels.

We study data augmentations for contrastive learning for Boolean
satisfiability. We demonstrate that:

  * •

Augmentation design is critical for contrastive pre-training on combinatorial
problems. In particular, our augmentations are sufficient for strong
performance, while existing graph augmentations are not.

  * •

Our contrastive method matches the best supervised baseline while using
$100\times$ fewer training labels.

  * •

Our contrastive representations transfer better to new problem types than
supervised representations.

##  2 Background

SAT. A Boolean formula in propositional logic consists of Boolean variables
composed by logical operators “and” ($\land$), “or” ($\lor$) and “not”
($\lnot$). A _literal_ is a variable $v$ or its negation $\lnot v$. A _clause_
is a disjunction of literals $\bigvee_{i=1}^{n}l_{i}$. A Boolean formula is in
_Conjunctive Normal Form_ (CNF) if it is a conjunction of clauses. We assume
that all formulas are in CNF. A variable assignment satisfies a clause when at
least one of its literals is satisfied. A formula $\phi$ is satisfied under
$\pi$ when all of its clauses are satisfied, and $\pi$ is a _satisfying
assignment_ for $\phi$. _SAT_ is the problem of deciding, for a given formula
$\phi$, if there exists a satisfying assignment (SAT) or not (UNSAT).

We can represent a SAT formula $\phi$ by a bipartite graph called _literal-
clause incidence graph_ (LIG) (Figure 1). The graph contains a node for every
clause and literal of $\phi$. An edge connects a clause node and a literal
node iff the clause contains that literal. We define $\text{LIG}^{+}$ when the
literal nodes of the same variable in LIG are connected.

Figure 1: A bipartite graph representation ($\text{LIG}^{+}$) of a SAT formula
$\phi:=(x\vee\neg y\vee\neg z)\wedge(\neg x\vee y\vee z)$. The subgraph
without  edges is the LIG of $\phi$.

NeuroSAT. Selsam et al. (2018) proposed NeuroSAT to classify satisfiability of
Boolean formulas. NeuroSAT consists of two parts: 1) _Encoder:_ a special
_Graph Neural Network_ (GNN) that takes in the $\text{LIG}^{+}$ representation
of a formula and produces an embedding for its literals; 2) _Aggregator_ : A
function that maps each literal representation to a vote and then aggregates
them into a prediction about satisfiability. More details can be found in
Appendix B.

##  3 Related Work

Graph Contrastive Learning. Existing graph contrastive frameworks can, in
principle, be used to learn representations for combinatorial problems. Common
augmentations in graph contrastive frameworks include: 1) perturbing
structures, such as, node dropping, subgraph sampling or graph diffusion, and
2) perturbing features, such as, masking or adding noise to the node features
(Hassani and Khasahmadi, 2020). These augmentations have achieved success in
multiple graph-level tasks (You et al., 2020; Hassani and Khasahmadi, 2020),
as well as node-level tasks (Zhu et al., 2020; Wan et al., 2021; Tong et al.,
2021).

Supervised Learning for Combinatorial Optimization (CO). Almost all modern
approaches to machine learning for CO, use variations of a GNN architecture.
On the supervised front, the work of Nowak et al. (2018) on _Quadratic
Assignment Problem_ , Joshi et al. (2019) and Prates et al. (2019) on
_Travelling Salesman Problem_ (TSP) have shown encouraging results. Gasse et
al. (2019) trained a branching heuristic for MILPs by imitating an expert
policy. Later, Nair et al. (2020) extended those ideas to make them scalable
to substantially larger instances. In SAT, Selsam et al. (2018) proposed a way
to train GNNs to solve SAT problems in an end-to-end fashion. The same
architecture was used in Selsam and Bjørner (2019) to guide variable branching
across conventional solvers.

Reinforcement Learning for CO. Supervised learning is bottlenecked by the need
for labels. Consequently, many have explored the use of _Reinforcement
Learning_ (RL). Node selection policy of Dai et al. (2017) for TSP and Kool et
al. (2018) for _Vehicle Routing Problem_ are examples of that effort. Lederman
et al. (2020) and Yolcu and Póczos (2019) used REINFORCE to train variable
branching heuristic for _quantified Boolean formulas_ and local search
algorithm WalkSAT, respectively. Kurin et al. (2019) used DQN for SAT and
Vaezipoor et al. (2021) improved a SOTA #SAT solver via _Evolution Strategy_.
We refer to (Cappart et al., 2021; Bengio et al., 2021) for more comprehensive
record of efforts in this area.

Unsupervised Learning for CO. Toenshoff et al. (2021) proposed an unsupervised
approach to solve constrained optimization problems on graphs by minimizing a
problem dependent loss function. Amizadeh et al. (2019a, b) solved SAT and
CircuitSAT problems by minimizing an energy function. Lastly, inspired by
probabilistic method, Karalias and Loukas (2020) trained a GNN in an
unsupervised way to act as a distribution over possible solutions of a given
problem, by minimizing a probabilistic penalty loss. Our method is distinct
from other unsupervised techniques in that we do not minimize a problem-
dependent loss function and rather learn problem representations through
contrastive learning. To the best of our knowledge this is the first attempt
at applying contrastive learning in the domain of combinatorial optimization.

##  4 Framework Overview

$c_{1}:x_{1}$$c_{2}:x_{2}\lor x_{3}$$c_{3}:x_{1}\lor\neg x_{3}\lor
x_{4}$$c_{4}:\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg
x_{4}$$c_{1}:x_{1}$$c_{2}:x_{2}\lor x_{3}$$c_{3}:x_{1}\lor\neg x_{3}\lor
x_{4}$$c_{4}\\!\\!:$$\neg x_{1}\lor$ $x_{2}\lor x_{3}\lor\neg
x_{4}$$c_{1}:x_{1}$$c_{2}:x_{2}\lor x_{3}$$c_{3}:x_{1}\lor\neg x_{3}\lor
x_{4}$$c_{4}:\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg x_{4}$$c_{5}:x_{1}\lor
x_{2}\lor
x_{4}$LabelPreservingAugmentationsEncoderEncoder$G_{1}$$G_{2}$$\mathcal{E}$$\mathcal{E}$$\mathbf{z_{1}}$$\mathbf{z_{2}}$$\phi$$\hat{\phi}_{1}$$\hat{\phi}_{2}$$\mathcal{L(.)}$
Figure 2: Our contrastive learning framework for combinatorial problems. Given
an instance $\phi$, a pair of augmented samples $(\hat{\phi}_{1}$,
$\hat{\phi}_{2})$ are formed using label-preserving augmentations.
$(\hat{\phi}_{1}$, $\hat{\phi}_{2})$ are then transformed to graph formats
$(G_{1},G_{2})$. An encoder is used to extract graph representations
$(\mathbf{z}_{1},\mathbf{z}_{2})$. Lastly, a standard contrastive loss is
applied over a mini-batch of instances.

Similar to contrastive algorithms in other domains (e.g., images), we learn
representations by contrasting augmented views of the same instance against
negative samples. Our framework (Figure 2) consists of four major components:

Augmentations. Given a combinatorial instance $\phi$, a stochastic
augmentation is applied to form a pair of positive samples, denoted by
$(\hat{\phi}_{1}$, $\hat{\phi}_{2})$. Our key insight is the tailored design
of augmentations for combinatorial problems should preserve the label of the
problem, e.g., satisfiability for SAT, as detailed in Section 5.

Format Transformation ($\mathcal{E}$). Formulas $(\hat{\phi}_{1}$,
$\hat{\phi}_{2})$ are transformed into (e.g., $\text{LIG}^{+}$) graphs
$(G_{1},G_{2})$.

Encoder. A neural encoder is trained to extract graph-level representations
$\mathbf{z}_{1},\mathbf{z}_{2}\in\mathbb{R}^{d}$ from the augmented graphs
$G_{1}$ and $G_{2}$. This encoder can be any GNN such as GCN (Kipf and
Welling, 2016) and the encoder proposed by NeuroSAT.

Contrastive Loss. In the end, SimCLR’s (Chen et al., 2020a) contrastive loss
$\mathcal{L}$ is applied to the graph representations
$\\{\mathbf{z}_{i}\\}_{i=1}^{2n}$, obtained from a mini-batch of $n$
instances. We follow Chen et al. (2020a) and use an MLP projection head to
project each $\mathbf{z}_{i}$ to $\mathbf{m}_{i}$. For a positive pair of
projected representations $(\mathbf{m}_{i},\mathbf{m}_{j})$, the loss
$\mathcal{L}_{i,j}$ is a cross-entropy loss of differentiating the positive
pair from the other $2(n-1)$ negative samples (i.e., augmented samples of
other instances):

$\displaystyle\mathcal{L}_{i,j}=-\log\frac{\exp(sim(\mathbf{m}_{i},\mathbf{m}_{j})\mathbin{/}\tau)}{\sum_{k=1}^{2N}\mathbf{1}_{k\neq
i}\exp(sim(\mathbf{m}_{i},\mathbf{m}_{k})\mathbin{/}\tau)},$ (1)

where $\tau$ is the temperature parameter, $\mathbf{1}$ is the indicator
function, and $sim$ measures the similarity between two representations:
$sim(\mathbf{m}_{i},\mathbf{m}_{j}):=\mathbf{m}_{i}^{T}\mathbf{m}_{j}/\left\|\mathbf{m}_{i}\right\|\left\|\mathbf{m}_{j}\right\|$.
The final loss $\mathcal{L}$ is the average of $\mathcal{L}_{i,j}$ over all
positive pairs. After training is completed, we only keep the encoder to
extract the representation $\mathbf{z}_{i}$ for downstream tasks.

##  5 Augmentations for Combinatorial Problems

###  5.1 Definition and Motivation

Intuitively, contrastive learning leads to representations that are invariant
across augmentations. Thus, to guarantee downstream predictive performance,
augmentations should (mostly) preserve the labels of downstream tasks (Arora
et al., 2019; Tosh et al., 2021; HaoChen et al., 2021; Dubois et al., 2021).
The augmentations found in computer vision, e.g., cropping and color jittering
of images, typically preserve the labels of classification tasks. This is not
the case for most previous graph contrastive frameworks (You et al., 2020;
Hassani and Khasahmadi, 2020), where simple graph augmentations like node
dropping and link perturbation are used without consideration of the
downstream task. For combinatorial problems, these _label-agnostic
augmentations_ (LAAs) are likely to produce many false positive pairs. For
example, in the SR dataset in NeuroSAT, each SAT can be turned into UNSAT by
flipping one literal in one clause.

Thus, we aim to design _label-preserving augmentations_ (LPAs), which are
transformations that preserve the instance label. Formally, given a problem
family $\Phi$ and a labelling function $f$, an augmentation distribution $A$
is an LPA iff:

$\displaystyle
f(\hat{\phi})=f(\phi),\quad\forall\hat{\phi}\in\texttt{supp}\left(A(\cdot|\phi)\right),\forall\phi\in\Phi,$

where supp denotes the support of a distribution.

Importantly, LPAs are well-studied for many combinatorial problems and are
much cheaper to obtain than labels. For SAT prediction, common preprocessing
techniques from SAT solvers such as variable elimination can be used as LPAs,
as discussed in Section 5.2. There are also LPAs for other combinatorial
problems, such as, adding cuts Achterberg et al. (2020) for MILPs and deleting
dominant vertices (Akiba and Iwata, 2016) for Minimum Vertex Cover.

The type of LPAs is also crucial. Intuitively, LPAs that make more significant
changes to an instance create harder positives from which better
representations can be learned. Indeed, LPAs that lead to larger augmentation
support $\texttt{supp}\left(A(\cdot|\phi)\right)$ will split $\Phi$ into
coarser equivalences classes, and thus (roughly speaking) a classifier can be
learned with fewer labelled instances.

###  5.2 Label-preserving Augmentations for SAT

The LPAs for SAT preserve satisfiability of any Boolean formula. In other
words, a (un)satisfiable instance remains (un)satisfiable after the
applications of LPAs. We review some common LPAs for SAT below, with examples
and time complexity results provided in Appendix A.

Unit Propagation (UP). A clause is a _unit clause_ if it contains only one
literal. If an instance $\phi$ contains a unit clause $\ell$, we can 1) remove
all clauses in $\phi$ containing the literal $\ell$ and 2) delete $\neg\ell$
from all other clauses.

Add Unit Literal (AU). The inverse of UP: 1) construct a unit clause from a
new literal $\ell$, 2) add its negation $\neg\ell$ to some other clauses and
3) create new clauses containing $\ell$.

Pure Literal Elimination (PL). A variable $v$ is called pure if it occurs with
only one polarity in $\phi$. We can delete all clauses in $\phi$ containing
$v$.

Subsumed Clause Elimination (SC). If a clause $c_{1}$ is a subset of $c_{2}$,
i.e., all literals in $c_{1}$ are also in $c_{2}$, then deleting $c_{2}$ does
not change satisfiability of $\phi$.

Clause Resolution (CR). Resolution produces a new clause implied by two
clauses containing complementary literals:

$\frac{\ell\lor a_{1}\lor\cdots\lor a_{n},\neg\ell\lor b_{1}\lor\cdots
b_{m}}{a_{1}\lor\cdots\lor a_{n}\lor b_{1}\lor\cdots b_{m}}$ (2)

The new clause $c$ is called the resolvent of $c_{1}$, $c_{2}$:
$c=c_{1}\otimes c_{2}$. Adding $c$ to $\phi$ does not change satisfiability.

Variable Elimination (VE). Let $S_{\ell}$ be a set of clauses containing the
literal $\ell$, and $S_{\neg\ell}$ be a set of clauses containing its negation
$\neg\ell$. Then a new set $S$ is obtained by pairwise resolving on clauses of
$S_{\ell}$ and $S_{\neg\ell}$: $S=\\{c_{1}\otimes c_{2}|c_{1}\in
S_{\ell},c_{2}\in S_{\neg\ell}\\}$. Replacing $S_{\ell}\cup S_{\neg\ell}$ with
$S$ does not change satisfiability Eén and Biere (2005).

Note that some augmentations, such as VE, have the worst-case exponential
complexity if run until convergence. However, in our paper, we only eliminate
a small and fixed number of variables. Therefore, all LPAs listed here are
cheap and have polynomial-time complexity.

##  6 Empirical Study of Augmentations for SAT

SR(10)PR(10)DP(20)PS(20)LPALAA Figure 3: Contrastive learning with LPAs learns
much better representations for SAT predictions than with LAAs. We evaluated
the linear classification performance of SSL models trained with different
single augmentations (diagonal) or paired combinations (off-diagonal). The
four heatmaps on the first row show results using LPAs, and the ones on the
second row using LAAs. Each column denotes different datasets. For off-
diagonal entries on each heatmap, the row corresponds to the first
augmentation applied.

Our first experiments study the role of augmentations in contrastive learning
for SAT prediction. We followed the standard linear evaluation protocol to
evaluate representations (Chen et al., 2020a), i.e., we report test accuracy
of a linear classifier trained on top of frozen representations.

Architecture. We primarily used the encoder of NeuroSAT (Selsam et al., 2018)
as the GNN architecture. We also re-ran a small number of experiments with
another type of GNN in Appendix E. Using the NeuroSAT architecture, we
obtained the graph-level representations by average-pooling over all literal
representations. We followed the design details of the original NeuroSAT
paper.

Experimental Setting. We used the contrastive loss in Equation 1 with the
temperature $0.5$. Appendix F also shows some experiments with other
contrastive objectives. We used Adam optimizer with learning rate $2\times
10^{-4}$ and weight decay $10^{-5}$. The batch size was $128$ and the maximum
training epoch was $5000$. The generator produced a set of new unlabelled
instances for each batch. We used 100 labelled instances to train our linear
evaluators, and another $500$ as the validation set to pick the
hyperparameters (ranging from $10^{-3}$ to $10^{3}$) of $L_{2}$
regularization. The test set consisted of $10^{4}$ instances.

Datasets. We experimented using four generators: SR (Selsam et al., 2018),
Power Random 3SAT (PR) (Ansótegui et al., 2009), Double Power (DP) and
Popularity Similarity (PS) (Giráldez-Cru and Levy, 2017). SR and PR are the
synthetic generators. DP and PS are pseudo-industrial generators producing
instances that mimic real-world problems. We generated instances of 10
variables for SR and PR, and 20 for DP and PS. The number inside the
parenthesis denotes the number of variables per instance. We also tweaked the
parameters of the generators so that they produce roughly balanced SAT and
UNSAT. More details are in Appendix D.

Augmentations. We used four of the LPAs from Section 5.2, namely: AU, SC, CR
and VE. The augmentations UP and PL were not studied because most of our
instances originally do not contain unit clauses or pure literals.

For our baseline we adopted four LAAs from GraphCL (You et al., 2020) with
some adjustments. The issue with the original augmentations was that they
operate directly on the graph. However, NeuroSAT requires the input to be in
the $\text{LIG}^{+}$ format, and blindly applying these augmentations might
break that structure. Thus, we adapted GraphCL augmentations to maintain the
$\text{LIG}^{+}$ structure, resulting in the following augmentations: drop
clauses (DC), drop variables (DV), link perturbation (LP) and subgraph (SG).
DC and DV correspond to node dropping. LP corresponds to edge perturbation,
where we randomly add/remove links between literals and clauses on a SAT
instance. Lastly, SG is similar to the one in GraphCL where we do a random
walk on an instance and keep the resulting subgraph.

All $8$ augmentations except SC are parameterized by $p$ which controls the
intensity of perturbations. For SC, we eliminate all subsumed clauses. In this
section, we chose the $p$ that achieved the best linear evaluation performance
when the corresponding augmentation was applied alone. The results for tuning
$p$ are shown in Appendix C.

###  6.1 Label-Preserving Augmentations are Necessary

Type Dataset | SR | PR | DP | PS
---|---|---|---|---
Random | 55.6 | 52.8 | 64.7 | 68.9
Resolution (ours) | 86.4 | 92.6 | 84.8 | 96.9
Table 1: Adding SAT-preserving clauses (Resolution) leads to much higher
accuracy than adding random ones (Random). The number of clauses added is
controlled to be the same for both.

Do LPAs learn better representations than LAAs? To investigate the effect of
using different augmentations, we evaluated the linear classification
performance of SSL models trained with different single augmentations or
paired combinations. As Figure 3 shows, the accuracy ($\%$) for the best LPA
pair is: $95.1$ for SR, $93.3$ for PR, $86.0$ for DP and $96.9$ for PS, while
the corresponding number ($\%$) for LAAs is much lower: $54.4,59.1,70.0$ and
$65.5$. These results show that SSL models trained with LPAs learn
significantly better representations than those with LAAs.

Do our gains simply come from adding clauses? The four LAAs from GraphCL do
not add new clauses to the original instance. To investigate whether this
explains the performance gap, we compared CR against adding the same number of
randomly generated clauses (adding random clauses). We eliminated subsumed
clauses (SC) after both augmentations. As shown in Table 1, adding SAT-
preserving resolvents achieved at least $20\%$ higher accuracy than adding
randomly generated clauses.

Does combining LPAs and LAAs hurt performance? In Table 2, we trained SSL
models with VE followed by $7$ different augmentations on SR(10). We compared
the accuracy change with the model trained with VE only. From Table 2, adding
LAAs resulted in $30\%$ drop in accuracy, while LPAs decreased the accuracy by
at most $3\%$.

In summary, the performance gap between LPAs and LAAs meets our intuition.
LAAs do not guarantee preserving satisfiability, which could result in false
positive pairs that hurt the SAT prediction performance.

LPAs | LAAs
---|---
AU | CR | SC | DC | DV | LP | SG
-1.5 | 0.7 | 1.2 | -34.4 | -32.4 | -33.7 | -35.9
Table 2: Adding LAAs to LPAs significantly hurts the performance. Cells
represent the difference of linear evaluation accuracy between training with
VE followed by another aug and with VE alone on SR(10). Yellow indicates
improved accuracy.

###  6.2 Type, Order, and Strengths of LPAs are Crucial

Previous studies of contrastive learning for image (Chen et al., 2020a) and
graph (You et al., 2020) have shown that the quality of learned
representations relies heavily on finding the right type and composition of
augmentations. We observe a similar pattern in SAT. In Figure 3, the accuracy
gap between the best LPA combination and the worst is between $20-40\%$ for
all datasets.

The conjecture in SimCLR (Chen et al., 2020a) is that stronger augmentations
lead to better representations. Intuitively, weaker augmentations often create
very correlated positive examples, providing shortcuts for neural networks to
cheat in the contrastive task without learning meaningful representations.
Based on this conjecture, we study what type, order, and strengths of LPAs
induce harder positive pairs and thus better representation quality.

Resolution-based augmentations are the most powerful. In Figure 3, the best
pair for each dataset includes either CR or VE. Both of them are based on the
resolution rule in Equation 2. Resolution is a powerful inference rule in
propositional logic. In fact, we can build a sound and complete propositional
theorem prover with only resolutions (Genesereth and Kao, 2013). The
Davis–Putnam algorithm (Davis and Putnam, 1960), the basis of practical SAT
solvers, iteratively applies resolution until reaching satisfiability
certificates. Resolution-based augmentations in contrastive learning may help
the neural work learn the essence of resolution, which leads to better
satisfiability prediction.

Composing different augmentations is beneficial across datasets. The highest
accuracy in Figure 3 always comes from off-diagonal entries, i.e., composition
of different augmentations. In PR, every singular augmentation failed to
obtain accuracy higher than $60\%$ by itself. While singular augmentations
achieved decent accuracy on SR and DP, combinations further improved the
accuracy. Similar to image and graph, composing different augmentations
resulted in harder positives and better representations.

Eliminating subsumed clauses after adding resolvents is particularly helpful.
CR followed by SC consistently produced high-quality representations across
all datasets. Using CR alone tended to perform substantially worse. The
accuracy drop without SC is: $28.1\%$ for SR, $33.4\%$ for PR, $7.0\%$ for DP,
$25.3\%$ for PS. Without SC, all original clauses are preserved by the
augmentation, leading to trivial positive pairs. In other words, without SC
the GNN may have solved the contrastive task by finding a common subgraph, not
by learning anything meaningful about resolution rules.

Interestingly, swapping the order of this pair also decreased accuracy by
$20-30\%$ for all datasets. We conjecture that this may be an artefact of our
specific generators. The percent of subsumed clauses in the original instances
(over $1000$ samples) was $43,0,76,69$ for SR, PR, DP and PS. Applying SC
first had no effect on PR due to no subsumed clauses present. For the other
three, SC may have eliminated too many clauses, which hurt the diversity of
resolvents created in the next phase.

Linear Evaluation Accuracy (%)Rate of Clause Resolution (%) Figure 4: Adding
more resolvents improves the performance across all datasets. Each point
represents linear evaluation accuracy of an SSL model trained with CR of the
specified rate (i.e., # of added resolvents divided by # of original clauses)
followed by SC.

More resolvents lead to better representations. Figure 4 studies the effect of
the number of resolvents added in CR. In general, adding more resolvents
improved the linear evaluation performance across all datasets. More
resolvents not only add more new clauses, but also may help SC delete more
original clauses, which create harder positives.

###  6.3 Do Our Augmentations Reveal the True Label?

As mentioned before, CR and VE are powerful enough to build a sound and
complete solver. Because our instances are relatively small, it is important
to ask if our augmentations “accidentally” reveal the true label(SAT/UNSAT) to
the model. We do not believe this is the case for the following reasons.

Our augmentations (polytime complexity) cannot in general determine whether a
formula is satisfiable (exponential in the worst case). When applied to our
datasets, VE only eliminated between 1-4 variables, and CR added between
10-20% of the total number of original clauses. This amount of work alone is
not enough to solve SAT.

To assess whether our augmentations are effectively solving our _specific_
instances, we measured the number of decision steps of CryptoMiniSat solvers
Soos et al. (2009) on different datasets before and after our LPAs. If our
LPAs were close to solving the instance, the decision steps should have
decreased dramatically after LPAs were applied. However, Table 7 in Appendix I
shows the decision steps remain relatively stable after augmentations.

Linear EvaluationFine-TuningAccuracy (%)Accuracy (%)No. of Training LabelsNo.
of Training LabelsNo. of Training LabelsNo. of Training Labels Figure 5: Our
method (SSL + LPA) achieves significantly higher accuracy after linear
evaluation and fine-tuning than all baselines in low-label regime and is
comparable to supervised models that have been given more labels. We vary the
number of training labelled instances from $2$ to $10^{4}$ and report the
average accuracy and standard error over 3 trials for all methods.

##  7 Comparison with Other Methods

The second set of experiments compared our proposed framework with other
baselines in the setups of linear evaluation, fine-tuning and few-shot
transfer learning. In addition to our model (SSL with LPA), we studied 4
baselines: SSL with LAA, supervised models trained without augmentations,
supervised models trained with LPA or LAA. The details of training SSL models
follow Section 6. For supervised models, we used the same architecture as
NeuroSAT. The hyperparameters for supervised were the same as SSL in Section
6, except the learning rate was chosen to be $2\times 10^{-5}$, following
Selsam et al. (2018). For each dataset, we chose the best augmentation
combination for LPA and LAA according to Figure 3. The degree parameter
associated with each augmentation was tuned separately for SSL and supervised
models. We used $200$ instances as validation sets for early stopping of all
methods.

Unless otherwise specified, all datasets used in this section have 40
variables per instance; in the Appendix H we report results for the same
experiments on smaller instances. For SR datasets, following NeuroSAT, we
trained on SR(U(10, 40)) and tested on SR(40). Training procedures for all
models were the same as Section 7.1, except the batch size was $80$ for SR(40)
to avoid memory issues. When fine-tuning NeuroSAT, we used different learning
rates for the encoder and aggregator, which were separately tuned for
different models on each dataset.

###  7.1 Linear Evaluation

We first evaluated the linear evaluation accuracy of all methods following the
procedure in Section 6. We varied the number of labelled instances from $2$ to
$10^{4}$.

As shown in the first row of Figure 5, our method achieved substantially
higher accuracy than others across all datasets in the low-label regime. For
example, with $10$ training labelled instances, the improvement ($\%$) of ours
compared from the second best method was: $9.42$ for SR, $14.07$ for PR,
$30.81$ for DP, $22.18$ for PS. Our model’s accuracy was also on par with
supervised models that had access to significantly more labels: for all
datasets, the accuracy of our models trained with $100$ labels matched or
exceeded the accuracy of our best supervised baselines trained with $10^{4}$
labels, a $100\times$ reduction in the number of labels needed.

On the other hand, SSL models trained with LAAs were not much better than
random-initialized ones under linear evaluation. We also found that using LAAs
for supervised models even hurt performance, possibly because LAAs add label
noise. For example, with $10000$ labels on DP(40), adding LAAs gave $20.21\%$
lower accuracy than supervised without augmentations.

###  7.2 Fine-tuning

We evaluated the fine-tuning accuracy of different SSL models compared to the
supervised baselines. Specifically, we took the pre-trained SSL models and
optimized them end-to-end on labelled data for a few epochs.

As shown in the second row of Figure 5, the fine-tuning results resemble those
of linear evaluation. In the low-label regime, our model (SSL + LPA) dominated
across all datasets. In contrast, SSL with LAAs did not improve much from
supervised models that were randomly initialized. As with linear evaluation,
we observed a reduction in sample complexity of at least $100\times$.

###  7.3 Few-shot Transfer Learning

Target DatasetSource DatasetUR(40)CA(40)SR(10)PR(10)DP(20)PS(20) Figure 6: The
representations of our model (solid bars) transfer better from source to
unseen target dataset than those of supervised (hatched bars) trained on the
same source. 10-shot transfer accuracy (%) was evaluated for each setup. The
blue line is the accuracy of fully-supervised models trained on each target
dataset with $10k$ labels.

We investigated how well the SSL models trained in Section 7.1 perform in
10-shot transfer to unseen and larger datasets, Uniform Random 3SAT (UR) and
Community Attachment (CA) (Giráldez-Cru and Levy, 2015). UR is a synthetic
generator, and CA is pseudo-industrial. We trained a logistic regression
classifier on the fixed representations with $10$ SAT and $10$ UNSAT instances
from the target dataset. We compared transferability of representations from
SSL with those from supervised representations trained on the same source
dataset. In particular, the supervised baseline was trained using $100,000$
labelled source instances with the same augmentations as SSL. Only the encoder
of the supervised models was used for extracting representations on target
datasets.

Do our representations transfer better than supervised? As shown in Figure 6,
we found that our SSL models generally transferred better than the supervised
baseline. This improvement also tended to be larger when the source and target
domain were more distinct, such as from pseudo-industrial instances (DP, PS)
to random 3 SAT (UR), and from random 3SAT (PR) to pseudo-industrial instances
(CA). This meets our intuition, because SSL does not leverage labels in the
source dataset, and thus reduces overfitting on source labels Yang et al.
(2020).

Does transferability vary with the source dataset? We also found that
transferability of representations depended heavily on the source datasets.
Generally speaking, models trained on pseudo-industrial generators, DP and PS,
transferred worse than the synthetic generators, SR and PR. We conjecture that
small industrial instances are not challenging enough for models to learn
generalizable representation of unseen problem domains. In Appendix G, we also
performed an experiment to show how the model trained on SR, PR, DP and PS
transfer to each other, which supports similar conclusions: models trained on
SR and PR transferred better to DP and PS than vice verse.

##  8 Conclusions and Outlook

We studied the effect of data augmentations on contrastive learning for the
Boolean satisfiability problem. We designed label-preserving augmentations
using well-studied transformations, e.g., clause resolution or variable
elimination, and confirmed the hypothesis that data augmentations should be
label-preserving to help in downstream prediction. The design of our
augmentations was critical; we found that resolution-based augmentations,
which produced more distinct augmentations, were necessary for strong results.
Our contrastive method was able to learn strong SAT predictors (at least as
strong as our best supervised baselines) with $100\times$ fewer labelled
training instances.

Although our results are restricted to Boolean satisfiability, they hold
lessons for solver design more broadly. For example, the convex hull of MILP
feasible sets is invariant to cuts, which suggests that contrastive pre-
training could be used to improve Neural Diving (Nair et al., 2020). In
general, our results strongly suggest that studying and exploiting invariances
can dramatically improve the sample complexity of heuristics learned via
imitation learning.

The study of combinatorial problems is fruitful for the broader machine
learning community, because these problems are non-trivial and so much is
known about their invariances. In particular, experiments can be designed that
exactly satisfy the assumptions of invariant learning theory, making
combinatorial problems fantastic test beds for the emerging field of
contrastive and self-supervised learning.

We thank Roger Grosse and Guiliang Liu for valuable discussions and insights.
Resources used in preparing this research were provided, in part, by the
Province of Ontario, the Government of Canada through CIFAR, and companies
sponsoring the Vector Institute. We acknowledge the support of the Natural
Sciences and Engineering Research Council of Canada (NSERC), RGPIN-2021-03445.

## References

  * Achterberg et al. (2020) Tobias Achterberg, Robert E Bixby, Zonghao Gu, Edward Rothberg, and Dieter Weninger.  Presolve reductions in mixed integer programming.  _INFORMS Journal on Computing_ , 32(2):473–506, 2020.
  * Akiba and Iwata (2016) Takuya Akiba and Yoichi Iwata.  Branch-and-reduce exponential/fpt algorithms in practice: A case study of vertex cover.  _Theoretical Computer Science_ , 609:211–225, 2016.
  * Amizadeh et al. (2019a) Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer.  Learning to solve circuit-sat: An unsupervised differentiable approach.  In _ICLR_ , 2019a.
  * Amizadeh et al. (2019b) Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer.  Pdp: A general neural framework for learning constraint satisfaction solvers.  _arXiv preprint arXiv:1903.01969_ , 2019b.
  * Ansótegui et al. (2009) Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy.  Towards industrial-like random sat instances.  In _Twenty-First International Joint Conference on Artificial Intelligence_ , 2009.
  * Arora et al. (2019) Sanjeev Arora, Hrishikesh Khandeparkar, Mikhail Khodak, Orestis Plevrakis, and Nikunj Saunshi.  A theoretical analysis of contrastive unsupervised representation learning.  _arXiv preprint arXiv:1902.09229_ , 2019.
  * Bardes et al. (2021) Adrien Bardes, Jean Ponce, and Yann LeCun.  Vicreg: Variance-invariance-covariance regularization for self-supervised learning.  _arXiv preprint arXiv:2105.04906_ , 2021.
  * Bengio et al. (2021) Yoshua Bengio, Andrea Lodi, and Antoine Prouvost.  Machine learning for combinatorial optimization: a methodological tour d’horizon.  _European Journal of Operational Research_ , 290(2):405–421, 2021.
  * Cappart et al. (2021) Quentin Cappart, Didier Chételat, Elias Khalil, Andrea Lodi, Christopher Morris, and Petar Veličković.  Combinatorial optimization and reasoning with graph neural networks.  _arXiv preprint arXiv:2102.09544_ , 2021.
  * Chen et al. (2020a) Ting Chen, Simon Kornblith, Mohammad Norouzi, and Geoffrey Hinton.  A simple framework for contrastive learning of visual representations.  In _International conference on machine learning_ , pages 1597–1607. PMLR, 2020a.
  * Chen et al. (2020b) Xinlei Chen, Haoqi Fan, Ross Girshick, and Kaiming He.  Improved baselines with momentum contrastive learning.  _arXiv preprint arXiv:2003.04297_ , 2020b.
  * Dai et al. (2017) Hanjun Dai, Elias B Khalil, Yuyu Zhang, Bistra Dilkina, and Le Song.  Learning combinatorial optimization algorithms over graphs.  _arXiv preprint arXiv:1704.01665_ , 2017.
  * Davis and Putnam (1960) Martin Davis and Hilary Putnam.  A computing procedure for quantification theory.  _Journal of the ACM (JACM)_ , 7(3):201–215, 1960\.
  * Dubois et al. (2021) Yann Dubois, Benjamin Bloem-Reddy, Karen Ullrich, and Chris J Maddison.  Lossy compression for lossless prediction.  In _NeurIPS_ , 2021.
  * Eén and Biere (2005) Niklas Eén and Armin Biere.  Effective preprocessing in sat through variable and clause elimination.  In _International conference on theory and applications of satisfiability testing_ , pages 61–75. Springer, 2005.
  * Gasse et al. (2019) Maxime Gasse, Didier Chételat, Nicola Ferroni, Laurent Charlin, and Andrea Lodi.  Exact combinatorial optimization with graph convolutional neural networks.  _arXiv preprint arXiv:1906.01629_ , 2019.
  * Genesereth and Kao (2013) Michael Genesereth and Eric Kao.  Introduction to logic.  _Synthesis Lectures on Computer Science_ , 4(1):1–165, 2013.
  * Giráldez-Cru and Levy (2015) Jesús Giráldez-Cru and Jordi Levy.  A modularity-based random sat instances generator.  In _Twenty-Fourth International Joint Conference on Artificial Intelligence_ , 2015.
  * Giráldez-Cru and Levy (2017) Jesús Giráldez-Cru and Jordi Levy.  Locality in random sat instances.  International Joint Conferences on Artificial Intelligence, 2017.
  * HaoChen et al. (2021) Jeff Z HaoChen, Colin Wei, Adrien Gaidon, and Tengyu Ma.  Provable guarantees for self-supervised deep learning with spectral contrastive loss.  _arXiv preprint arXiv:2106.04156_ , 2021.
  * Hassani and Khasahmadi (2020) Kaveh Hassani and Amir Hosein Khasahmadi.  Contrastive multi-view representation learning on graphs.  In _International Conference on Machine Learning_ , pages 4116–4126. PMLR, 2020.
  * He et al. (2020) Kaiming He, Haoqi Fan, Yuxin Wu, Saining Xie, and Ross Girshick.  Momentum contrast for unsupervised visual representation learning.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 9729–9738, 2020.
  * Joshi et al. (2019) Chaitanya K Joshi, Thomas Laurent, and Xavier Bresson.  An efficient graph convolutional network technique for the travelling salesman problem.  _arXiv preprint arXiv:1906.01227_ , 2019.
  * Karalias and Loukas (2020) Nikolaos Karalias and Andreas Loukas.  Erdos goes neural: an unsupervised learning framework for combinatorial optimization on graphs.  In _NeurIPS 2020 34th Conference on Neural Information Processing Systems_ , 2020.
  * Kipf and Welling (2016) Thomas N Kipf and Max Welling.  Semi-supervised classification with graph convolutional networks.  _arXiv preprint arXiv:1609.02907_ , 2016.
  * Kool et al. (2018) Wouter Kool, Herke Van Hoof, and Max Welling.  Attention, learn to solve routing problems!  _arXiv preprint arXiv:1803.08475_ , 2018.
  * Kurin et al. (2019) Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro.  Improving SAT Solver Heuristics with Graph Networks and Reinforcement Learning.  _CoRR_ , abs/1909.11830, 2019.
  * Lederman et al. (2020) Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee.  Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning.  In _8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020_. OpenReview.net, 2020.
  * Nair et al. (2020) Vinod Nair, Sergey Bartunov, Felix Gimeno, Ingrid von Glehn, Pawel Lichocki, Ivan Lobov, Brendan O’Donoghue, Nicolas Sonnerat, Christian Tjandraatmadja, Pengming Wang, et al.  Solving mixed integer programs using neural networks.  _arXiv preprint arXiv:2012.13349_ , 2020.
  * Nejati and Ganesh (2019) Saeed Nejati and Vijay Ganesh.  Cdcl (crypto) sat solvers for cryptanalysis.  In _Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering_ , pages 311–316, 2019.
  * Nowak et al. (2018) Alex Nowak, Soledad Villar, Afonso S Bandeira, and Joan Bruna.  Revised note on learning quadratic assignment with graph neural networks.  In _2018 IEEE Data Science Workshop (DSW)_ , pages 1–5. IEEE, 2018\.
  * Prates et al. (2019) Marcelo Prates, Pedro HC Avelar, Henrique Lemos, Luis C Lamb, and Moshe Y Vardi.  Learning to solve np-complete problems: A graph neural network for decision tsp.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 33, pages 4731–4738, 2019.
  * Selsam and Bjørner (2019) Daniel Selsam and Nikolaj Bjørner.  Guiding high-performance sat solvers with unsat-core predictions.  In _International Conference on Theory and Applications of Satisfiability Testing_ , pages 336–353. Springer, 2019.
  * Selsam et al. (2018) Daniel Selsam, Matthew Lamm, B Benedikt, Percy Liang, Leonardo de Moura, David L Dill, et al.  Learning a sat solver from single-bit supervision.  In _International Conference on Learning Representations_ , 2018.
  * Soos et al. (2009) Mate Soos, Karsten Nohl, and Claude Castelluccia.  Extending sat solvers to cryptographic problems.  In _International Conference on Theory and Applications of Satisfiability Testing_ , pages 244–257. Springer, 2009.
  * Toenshoff et al. (2021) Jan Toenshoff, Martin Ritzert, Hinrikus Wolf, and Martin Grohe.  Graph neural networks for maximum constraint satisfaction.  _Frontiers in artificial intelligence_ , 3:98, 2021.
  * Tong et al. (2021) Zekun Tong, Yuxuan Liang, Henghui Ding, Yongxing Dai, Xinke Li, and Changhu Wang.  Directed graph contrastive learning.  _Advances in Neural Information Processing Systems_ , 34, 2021.
  * Tosh et al. (2021) Christopher Tosh, Akshay Krishnamurthy, and Daniel Hsu.  Contrastive learning, multi-view redundancy, and linear models.  In _Algorithmic Learning Theory_ , pages 1179–1206. PMLR, 2021.
  * Vaezipoor et al. (2021) Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris Maddison, Roger B Grosse, Sanjit A. Seshia, and Fahiem Bacchus.  Learning branching heuristics for propositional model counting.  _Proceedings of the AAAI Conference on Artificial Intelligence_ , 35(14):12427–12435, May 2021.
  * Wan et al. (2021) Sheng Wan, Yibing Zhan, Liu Liu, Baosheng Yu, Shirui Pan, and Chen Gong.  Contrastive graph poisson networks: Semi-supervised learning with extremely limited labels.  _Advances in Neural Information Processing Systems_ , 34, 2021.
  * Yang et al. (2020) Xingyi Yang, Xuehai He, Yuxiao Liang, Yue Yang, Shanghang Zhang, and Pengtao Xie.  Transfer learning or self-supervised learning? a tale of two pretraining paradigms.  _arXiv preprint arXiv:2007.04234_ , 2020.
  * Yolcu and Póczos (2019) Emre Yolcu and Barnabás Póczos.  Learning Local Search Heuristics for Boolean Satisfiability.  In _Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, 8-14 December 2019, Vancouver, BC, Canada_ , pages 7990–8001, 2019.
  * You et al. (2020) Yuning You, Tianlong Chen, Yongduo Sui, Ting Chen, Zhangyang Wang, and Yang Shen.  Graph contrastive learning with augmentations.  _Advances in Neural Information Processing Systems_ , 33:5812–5823, 2020.
  * Zhu et al. (2020) Yanqiao Zhu, Yichen Xu, Feng Yu, Qiang Liu, Shu Wu, and Liang Wang.  Deep graph contrastive representation learning.  _arXiv preprint arXiv:2006.04131_ , 2020.

##  Appendix A LPAs for SAT

###  A.1 Examples

Original | UP
---|---
$c_{1}:x_{1}$ | $x_{1}$
$c_{2}:x_{2}\lor x_{3}$ | $x_{2}\lor x_{3}$
$c_{3}:x_{1}\lor\neg x_{3}\lor x_{4}$ | $x_{1}\lor\neg x_{3}\lor x_{4}$
$c_{4}:\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg x_{4}$ |  $\neg x_{1}\lor$$x_{2}\lor x_{3}\lor\neg x_{4}$
AU | SC
$\color[rgb]{0.7890625,0.17578125,0.22265625}\definecolor[named]{pgfstrokecolor}{rgb}{0.7890625,0.17578125,0.22265625}\neg x_{5}$ |
$\color[rgb]{0.7890625,0.17578125,0.22265625}\definecolor[named]{pgfstrokecolor}{rgb}{0.7890625,0.17578125,0.22265625}x_{5}\lor$ $x_{1}$ | $x_{1}$
$x_{2}\lor x_{3}$ | $x_{2}\lor x_{3}$
$x_{1}\lor\neg x_{3}\lor x_{4}$ | $x_{1}\lor\neg x_{3}\lor x_{4}$
$\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg x_{4}$ | $\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg x_{4}$
$\color[rgb]{0.7890625,0.17578125,0.22265625}\definecolor[named]{pgfstrokecolor}{rgb}{0.7890625,0.17578125,0.22265625}\neg x_{5}\lor x_{1}\lor\neg x_{2}\lor x_{3}$ |
CR | VE
$x_{1}$ | $x_{1}$
$x_{2}\lor x_{3}$ | $x_{2}\lor x_{3}$
$x_{1}\lor\neg x_{3}\lor x_{4}$ | $x_{1}\lor\neg x_{3}\lor x_{4}$
$\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg x_{4}$ | $\neg x_{1}\lor x_{2}\lor x_{3}\lor\neg x_{4}$
$\color[rgb]{0.7890625,0.17578125,0.22265625}\definecolor[named]{pgfstrokecolor}{rgb}{0.7890625,0.17578125,0.22265625}x_{1}\lor x_{2}\lor x_{4}$ | $\color[rgb]{0.7890625,0.17578125,0.22265625}\definecolor[named]{pgfstrokecolor}{rgb}{0.7890625,0.17578125,0.22265625}x_{1}\lor x_{2}\lor x_{4}$
Table 3:  Examples of LPAs for SAT. UP: remove $c_{1},c_{3}$ and $\neg x$ from
$c_{4}$. AU: add unit literal $\neg x_{5}$, add $x_{5}$ to $c_{1}$ and create
a new random clauses containing $\neg x_{5}$ . SC: remove $c_{4}$ because
$c_{2}\subset c_{4}$. CR: add $c_{2}\otimes c_{3}$. VE: eliminate $x_{3}$ by
adding $c_{2}\otimes c_{3}$ and $c_{4}\otimes c_{3}$.

####  A.1.1 Time Complexity

Let $n$ denote the number of clauses in the instance.

Rule | Explanation | Time Complexity
---|---|---
UP | Eliminate one Unit Clause | $O(n)$
AU | Add one Unit Clause | $O(n)$
PL | Eliminate one pure literal | $O(n)$
SC | Eliminate all subsumed clauses | $O(n^{2})$
CR | Resolve one pair of clauses | $O(n)$
VE | Eliminate one variable | $O(n^{2})$
Table 4: Complexity results of LPAs

##  Appendix B NeuroSAT

##### Encoder

We use $L^{n}$ and $C^{n}$ to denote the embeddings for literals and clauses
at the message passing round $n$. In addition, we have hidden states for
literals and clauses, denoted by $L_{h}^{n},C_{h}^{n}$. Let $M$ be the
bipartite adjacency matrix of the $\text{LIG}^{+}$. NeuroSAT encoder is
parameterized by two MLPs ($L_{msg},C_{msg}$) and two layer-norm LSTMs
($L_{u},C_{u}$), which are shared for all rounds. Then for round $n$,
embeddings are updated as:

$\displaystyle(C^{n+1},C_{h}^{n+1})$ $\displaystyle\leftarrow
C_{u}([C_{h}^{n},M^{T}L_{msg}(L^{n})])$ $\displaystyle(L^{n+1},L_{h}^{n+1})$
$\displaystyle\leftarrow L_{u}([L_{h}^{n},FLIP(L^{n}),MC_{msg}(C^{n+1})]),$

where $FLIP$ swaps the literal and its negation in the embedding.

In this work, we always set the number of message passing rounds to $26$. We
use $L^{26}$ as the final literal embedding. The graph-level representation
can be computed as an average of the embeddings for all literals.

##### Aggregator

Given the embeddings $L^{N}$ from the encoder, we project each literal
representation to a single scalar using an MLP $L_{vote}$: $V\leftarrow
L_{vote}(L^{N})$. Then we minimize the cross-entropy loss between the true
label and $sigmoid(mean(L_{vote}))$

##  Appendix C Augmentation Rates for LAAs ans LPAs

We also investigated the effect of augmentation rates for LAAs and LPAs, with
results presented in Figure 7 and 8.

SR(10)PR(10)DP(20)PS(20)Augmentation Rate (%)Test Accuracy (%) Figure 7: The
effect of rate of LAAs on the accuracy across datasets. The diamond markers
indicate the maximum achieved accuracy which was the rate that was
subsequently chosen to produce the heatmap of Figure 3.
SR(10)PR(10)DP(20)PS(20)Augmentation Rate (%)Test Accuracy (%) Figure 8: The
effect of rate of our LPA augmentations on the accuracy across datasets. The
diamond markers indicate the maximum achieved accuracy which was the rate that
was subsequently chosen to produce the heatmap of Figure 3.

##  Appendix D Datasets

###  D.1 Brief Description

  * •

SR (Selsam et al., 2018) A random SAT generator proposed as a challenge for
neural networks to learn intrinsic properties about satisfiability without
cheating on some miscellaneous statistics about the dataset.

  * •

PR (Ansótegui et al., 2009) A random k-SAT generator where the frequency of
each variable is sampled from a power-law distribution.

  * •

DP (Ansótegui et al., 2009) A pseudo-industrial generator based on PR with
varying clause length

  * •

PS (Giráldez-Cru and Levy, 2017) A pseudo-industrial generator based on the
notion of locality.

  * •

UR A random k-SAT generator where each variable is sampled uniformly.

  * •

CA (Giráldez-Cru and Levy, 2015) A pseudo-industrial generator based on the
notion of modularity.

###  D.2 Parameters

For the purpose of reproducibility, we show the parameters of each generator
used in the paper below:

  * •

SR(10) / SR(40) All parameters follow NeuroSAT.

  * •

PR(10) Number of variables: 10. Number of clauses: 41. Variable per clause: 3.
Power-law exponents of variables: 1.7.

  * •

PR(40) Number of variables: 40. Number of clauses: 147. Variable per clause:
3. Power-law exponents of variables: 2.5.

  * •

DP(20) Number of variables: 20. Number of clauses: 34. Average variables per
clause: 4. Power-law exponents of variables: 1.7.

  * •

DP(40) Number of variables: 40. Number of clauses: 75. Average variables per
clause: 5. Power-law exponents of variables: 1.7.

  * •

PS(20) Number of variables: 20. Number of clauses: 58. Min variable per
clause: 2. Average variables per clause: 4.

  * •

PS(40) Number of variables: 40. Number of clauses: 73. Min variable per
clause: 2. Average variables per clause: 5.

##  Appendix E Does our method work with other GNN architectures?

We also studied if our framework could be used with more common architectures,
such as, graph convolutional networks (GCNs). We chose the GCN architecture in
NeuralDiver (Nair et al., 2020) without the residual connection. The number of
layers is set to be $10$. Table 5 shows that SSL + LPA still dominates in the
low-label regime.

| 2 | 10 | 100 | 1000 | 5000 | 10000
---|---|---|---|---|---|---
Supervised | 49.82 | 50.08 | 50.68 | 50.23 | 51.25 | 78.82
SSL + LPA | 60.35 | 70.26 | 73.17 | 75.29 | 75.27 | 77.54
SSL + LAA | 51.32 | 51.29 | 48.93 | 50.72 | 50.41 | 63.24
Table 5: Linear evaluation performance of different methods with GCNs on
SR(10).

##  Appendix F Does our method work with other contrastive loss functions?

We replaced the SimCLR’s loss function in Equation 1 with the VICReg loss
(Bardes et al., 2021). We set $\lambda=15,\mu=1,\nu=1$ for the hyperparameters
of VICReg. As shown in Table 6, linear evaluation performance for both
objective functions are quite close.

| 2 | 10 | 100 | 1000 | 5000 | 10000
---|---|---|---|---|---|---
Ours + SimCLR | 79.53 | 88.32 | 92.23 | 93.32 | 93.01 | 95.12
Ours + VICReg | 76.38 | 89.15 | 91.27 | 93.98 | 94.01 | 94.77
Table 6: Linear evaluation performance of our methods with SimCLR and VICReg
loss on SR(10)

##  Appendix G More Transfer Learning Results

See Figure 9.

Figure 9:  Each bar represents the SSL model trained on a different source
dataset, and each subplot is the target dataset $4$ SSL models are evaluated
on. The number on top of each bar is the linear evaluation accuracy with 20
labels from the target dataset. The blue line is the fully-supervised baseline
trained on $20$ labels on the target baseline, and the red line is the
supervised baseline trained on $10000$ labels. The $\blacklozenge$ symbol
emphasizes that the train and test datasets are from the same distribution.
_Left_ : Transfer to unseen problems of similar size. _right_ : Transfer to
unseen problems of larger size.

##  Appendix H Evaluation on Smaller Datasets

We also performed linear evaluation and fine-tuning experiments for the
smaller datasets in Section 6. The results are shown in Figure 10.

Linear EvaluationFine-tuningAccuracy (%)Accuracy (%)No. of Training LabelsNo.
of Training LabelsNo. of Training LabelsNo. of Training Labels Figure 10: Our
method (SSL + LPA) achieves significantly higher accuracy after linear
evaluation and fine-tuning than baselines in low-label regime and is
comparable to supervised models that have been given more labels. We vary the
number of training labelled instances from $2$ to $10^{4}$ and report the
average accuracy and standard error over 3 trials for all methods.

##  Appendix I Decision step

We measured the decision steps of CryptoMiniSat Soos et al. (2009) solvers
before and after our augmentations. The result is shown in Table 7.

| SR(40) | PR(40) | DP(40) | PS(40)
---|---|---|---|---
| SAT | UNSAT | SAT | UNSAT | SAT | UNSAT | SAT | UNSAT
Before | $17.54$ | $13.25$ | $18.21$ | $12.14$ | $32.78$ | $0.27$ | $33.26$ | $7.37$
After | $16.36$ | $16.40$ | $21.61$ | $12.64$ | $28.47$ | $0.36$ | $34.83$ | $6.92$
Table 7: Decision steps of CryptoMiniSat Soos et al. (2009) solvers before and
after augmentations used in Figure 5. We use the same augmentation as the
corresponding SSL model in Figure 5. The statistics is computed over $1000$
instances for each dataset.