Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cubing for Tuning

Haoze Wu, Clark Barrett, Nina Narodytska

TL;DR

This work addresses the challenge of tuning high-level solver strategies for a single problem instance by learning online from the instance itself. It introduces taco, a general framework that extends cube-and-conquer with online strategy learning, comprising cubing, tuning, validation, and solving stages. Across SAT solving and neural network verification, taco yields consistent performance gains, discovers novel instance-specific strategies, and in many cases surpasses state-of-the-art baselines. The approach demonstrates the practical potential of per-instance, online configuration to boost challenging automated reasoning tasks and highlights directions for deeper integration and cloud-scale applications.

Abstract

We are exploring the problem of building an automated reasoning procedure that adaptively tunes the high-level solving strategy for a given problem. There are two main distinctive characteristics of our approach: tuning is performed solely online, unlike the common use of tuning as an offline process; and tuning data comes exclusively from the given instance, so we do not rely on the availability of similar benchmarks and can work with unique challenging instances. Our approach builds on top of the divide-and-conquer paradigm that naturally serves partitioned sub-problems for an automated tuning algorithm to obtain a good solving strategy. We demonstrate performance improvement on two classes of important problems--SAT-solving and neural network verification--and show that our method can learn unconventional solving strategies in some cases.

Cubing for Tuning

TL;DR

This work addresses the challenge of tuning high-level solver strategies for a single problem instance by learning online from the instance itself. It introduces taco, a general framework that extends cube-and-conquer with online strategy learning, comprising cubing, tuning, validation, and solving stages. Across SAT solving and neural network verification, taco yields consistent performance gains, discovers novel instance-specific strategies, and in many cases surpasses state-of-the-art baselines. The approach demonstrates the practical potential of per-instance, online configuration to boost challenging automated reasoning tasks and highlights directions for deeper integration and cloud-scale applications.

Abstract

We are exploring the problem of building an automated reasoning procedure that adaptively tunes the high-level solving strategy for a given problem. There are two main distinctive characteristics of our approach: tuning is performed solely online, unlike the common use of tuning as an offline process; and tuning data comes exclusively from the given instance, so we do not rely on the availability of similar benchmarks and can work with unique challenging instances. Our approach builds on top of the divide-and-conquer paradigm that naturally serves partitioned sub-problems for an automated tuning algorithm to obtain a good solving strategy. We demonstrate performance improvement on two classes of important problems--SAT-solving and neural network verification--and show that our method can learn unconventional solving strategies in some cases.
Paper Structure (49 sections, 6 theorems, 2 equations, 35 figures, 7 tables, 2 algorithms)

This paper contains 49 sections, 6 theorems, 2 equations, 35 figures, 7 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Methodology
  3. Overview
  4. Cubing.
  5. Strategy learning.
  6. Solving.
  7. Collecting Suitable Cubes
  8. Efficiently implementing Alg. \ref{['alg:createCubes']}.
  9. Extending Cube-and-Conquer with Online Strategy Learning
  10. Design choice: strategy validation.
  11. Design choice: strategies for collection.
  12. Tuning the solving strategy on the cubes
  13. Design choice: proposal distribution.
  14. Design choice: MCMC initialization.
  15. Instantiations of taco
  16. ...and 34 more sections

Key Result

Theorem 1

If $\textsc{collect}\xspace(f\xspace, C\xspace, t\xspace, \mathcal{V}\xspace)$ returns $\left<\texttt{UNKNOWN}\xspace, C'\xspace\right>$, then $\left\lvert C'\xspace \right\rvert = t\xspace$ and for each cube $c$ in $C'$, there is some solving strategy $v\xspace\in\mathcal{V}\xspace$ such that $\mat

Figures (35)

  • Figure 1: taco learned a new strategy on a challenging SAT benchmark (eq.atree.braun.13). CnC with taco solved the benchmark in 139 seconds, while it took plain CnC, Painless, and sequential kissat 242, 1088, 5279 seconds, respectively. The benchmark deals with hardware multiplier equivalence checking and was found especially suitable to be tackled by CnCheule2011cube.
  • Figure 2: Overview of the taco-based solving procedure.
  • Figure 3: Ablation studies of the effect of, from top to bottom, less tuning cubes (-Cubes), no validation (-Cubes-Val.), larger strategy space (+Stra.), and no probing for MCMC initialization (+Stra.-Prob.). Vanilla CnC took 746 seconds.
  • Figure 4: 9dlx_vliw_at_b_iq8
  • Figure 5: 9dlx_vliw_at_b_iq9
  • ...and 30 more figures

Theorems & Definitions (11)

  • Theorem 1
  • Theorem 2
  • Definition 1: Cubing trace
  • Theorem 3: Termination via bounded cost reduction
  • proof
  • Theorem 3: Termination via bounded cost reduction
  • proof
  • Lemma 1: Bounded cost reduction for SAT solving
  • proof
  • Lemma 2: Bounded cost reduction for Neural Network Verification
  • ...and 1 more