SHapley Additive exPlanations (SHAP) is a key tool for interpreting decision tree ensembles by assigning contribution values to features. It is widely used in finance, advertising, medicine, and other domains. Two main approaches to SHAP calculation exist: Path-Dependent SHAP, which leverages the tree structure for efficiency, and Background SHAP, which uses a background dataset to estimate feature distributions. We introduce Woodelf, a SHAP algorithm that integrates decision trees, game theory, and Boolean logic into a unified framework. For each consumer, Woodelf constructs a pseudo-Boolean formula that captures their feature values, the structure of the decision tree ensemble, and the entire background dataset. It then leverages this representation to compute Background SHAP in linear time. Woodelf can also compute Path-Dependent SHAP, Shapley interaction values, Banzhaf values, and Banzhaf interaction values. Woodelf is designed to run efficiently on CPU and GPU hardware alike. Available via the Python package woodelf, it is implemented using NumPy, SciPy, and CuPy without relying on custom C++ or CUDA code. This design enables fast performance and seamless integration into existing frameworks, supporting large-scale computation of SHAP and other game-theoretic values in practice. For example, on a dataset with 3,000,000 rows, 5,000,000 background samples, and 127 features, Woodelf computed all Background Shapley values in 162 seconds on CPU and 16 seconds on GPU—compared to 44 minutes required by the best method on any hardware platform, representing 16x and 165x speedups, respectively.

We introduce Backtrackable Inprocessing (BI), a framework that enables applying inprocessing under the current trail at any decision level, at any point during incremental SAT solving. Our approach lifts the long-standing restriction that inprocessing must be performed only at the global decision level, thereby substantially increasing its potential effectiveness. We focus on three highly efficient core techniques: subsumption, self-subsuming resolution, and Bounded Variable Elimination (BVE). We show how to ensure sound backtracking in the presence of inprocessing, and demonstrate that applying BI for incremental preprocessing after propagating assumptions yields significant performance improvements on Bounded Model Checking (BMC) benchmarks from the Hardware Model Checking Competition 2017. Implemented in the Island SAT solver (IntelSAT’s fork), BI enables solving ∼1.5× as many difficult bounds as the baseline global-level incremental preprocessor.

Boolean matching, a fundamental problem in circuit design, determines whether two Boolean circuits are equivalent under input/output permutations and negations. While most works focus on finding a single match or proving its absence, the problem of enumerating all matches remains largely unexplored, with BooM being a notable exception. Motivated by timing challenges in Intel’s library mapping flow, we introduce EBat - an open-source tool for enumerating all matches between single-output circuits. Built from scratch, EBat reuses BooM’s SAT encoding and introduces novel high-level algorithms and performance-critical subroutines to efficiently identify and block multiple mismatches and matches simultaneously. Experiments demonstrate that EBat substantially outperforms BooM’s baseline algorithm, solving 3 to 4 times more benchmarks within a given time limit. EBat has been productized as part of Intel’s library mapping flow, effectively addressing the timing challenges.

Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.

Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.

Abstract NP-hard combinatorial optimization problems are pivotal in science and business. There exists a variety of approaches for solving such problems, but for problems with complex constraints and objective functions, local search algorithms scale the best. Such algorithms usually assume that finding a non-optimal solution with no other requirements is easy. However, what if it is NP-hard? In such case, a SAT solver can be used for finding the initial solution, but how can one continue solving the optimization problem? We offer a generic methodology, called Local Search with SAT Oracle (), to solve such problems. facilitates implementation of advanced local search methods, such as variable neighbourhood search, hill climbing and iterated local search, while using a SAT solver as an oracle. We have successfully applied our approach to solve a critical industrial problem of cell placement and productized our solution at Intel.

Given a propositional formula $F$ in Conjunctive Normal Form (CNF), a SAT solver decides whether it is satisfiable or not. It is often required to find a solution to a satisfiable CNF formula F, which optimizes a given Pseudo-Boolean objective function Ψ, that is, to extend SAT to optimization. MaxSAT is a widely used extension of SAT to optimization. A MaxSAT solver can be applied to optimize a Pseudo-Boolean objective function Ψ, given a CNF formula F, whenever Ψ is a linear function. MaxSAT has a diverse plethora of applications, including applications in computer-aided design, artificial intelligence, planning, scheduling and bioinformatics. A variety of approaches to MaxSAT have been developed over the last two decades. In this tutorial, we focus on anytime MaxSAT algorithms, where an anytime algorithm is expected to find better and better solutions, the longer it keeps running. The anytime property is crucial in industrial applications, since it allows the user to: 1) get an approximate solution even for very difficult instances, and 2) trade quality for performance by regulating the timeout. Anytime MaxSAT solvers have been evaluated at yearly MaxSAT Evaluations since 2011 in the so-called incomplete tracks. We trace the evolvement of anytime MaxSAT algorithms over the last decade and lay out the algorithms, applied by the winners of MaxSAT Evaluation 2020. Furthermore, we touch upon anytime algorithms for optimization problems beyond MaxSAT, such as bit-vector optimization and the problem of optimizing an arbitrary not-necessarily-linear function, given a CNF formula. Finally, we discuss challenges and future work.

The goal of this study is to improve the scalability of today's SAT-based solutions for optimization problems and to pave the way towards extending the range of optimization problems solvable with SAT in practice.Let OptSAT be the problem of optimizing a generic Pseudo-Boolean function, given a satisfiable propositional formula F .We introduce an incremental and anytime incomplete algorithm for solving OptSAT, called Polosat.We show that integrating Polosat into a state-of-theart open-source anytime MaxSAT solver significantly improves the solver's performance.Furthermore, we demonstrate that Polosat substantially improves the solution quality of an industrial placement tool, where placement is a sub-stage of the physical design stage of chip design.

This paper introduces a new anytime algorithm for Weighted MaxSAT consisting of two main algorithmic components. First, we propose a new efficient polarity selection heuristic and an enhancement to the variable decision heuristic for SAT-based anytime Weighted MaxSAT solving (and, more generally, for solving any optimization problem with a SAT-based anytime algorithm). Second, we enhance an existing Bit-vector Optimization-based algorithm for solving Unweighted MaxSAT and generalize it to Weighted MaxSAT. Our resulting Weighted MaxSAT solver outscores the state-of-the-art solvers in the settings of both the 60-second and 300-second weighted incomplete tracks of MaxSAT Evaluation 2018. In addition, we describe a new application of incremental anytime Weighted MaxSAT solving: placement at the physical design stage of Computer-aided Design (CAD).

We present LIAMC, a novel decision procedure for (quantifier-free) linear arithmetic over both integers modulo 2N(LIAn) and integers (LIA). There is no need to explain our motivation to design a new efficient decision procedure for the widely used LIA logic. A LIAndecision procedure can be extremely useful in the context of software (SW) verification. SW verification usually requires to reason about arithmetic constraints over finite integers. To that end, modern SW verification tools commonly use fixed-width bit-vector (BV) solvers. However, BV solvers' efficiency drops dramatically as the width increases. To solve the performance problem, LIA solvers are applied, but they are imprecise as they cannot handle integer overflow. An efficient LIANsolver would be the ideal solution in this context. Our decision procedure LIAMC is based on a transformation of linear arithmetic into safety verification. We treat integers as unbounded streams of bits over time. More precisely, for each input integer, the least significant bit (LSB) corresponds to time 0 in the corresponding stream, and the k-th bit corresponds to the bit received at time k. LIAMC then uses SAT-based model checking (SATMC) to solve the resulting problem. In order to achieve efficiency, LIAMC uses two forms of generalization. First, if it finds a formula to be unsatisfiable for width N, it tries to generalize this result for all the widths. Second, if LIAMC finds a formula to be satisfiable for width N, it tries to “extend” and thus generalize the assignment to a wider target width. To evaluate LIAMC we used the QF_LIA subset of SMT-COMP'16, and ran two sets of experiments. First, we reinterpreted the QF_LIA over fixed-width bit-vectors of varying widths and compared LIAMC in LIAn mode to both Boolector and Z3. LIAMC solved the most satisfiable instances out of the three even for the shortest width 32. Second, we compared LIAMC to CVC4 and Z3 on the original QF_LIA benchmarks. LIAMC was able to solve many instances that had not been solved by the other solvers.

Routing is an essential stage in physical design, where already placed components are connected by wires. Routing must satisfy various manufacturing requirements, referred to as design rules. We formalize the problem of design-rule-aware routing and introduce a solver, called DRouter, for the resulting problem. Plain routing is often modeled as follows: given an undirected weighted graph and a set of m disjoint nets (each net being a set of vertices), a routing is a (minimal) forest of m disjoint trees, where each tree spans a net. DRouter's input comprises a plain routing instance and a bit-vector formula, whose variables include the edges of the graph as Boolean variables (along with other variables). DRouter looks for a satisfying assignment to F, such that the satisfied edges comprise a routing. DRouter implements an A*-based router inside a SAT solver. It overrides the solver's decision and restart strategies and enhances its learning with routing-aware algorithms. We demonstrate that, on a set of crafted routing instances, DRouter has substantially better capacity than either plain reduction to bit-vector reasoning or Monosat, a solver that is able to reason about SAT and graph predicates. We show that DRouter can route large clips from Intel designs while obeying up to millions of applications of the design rules - a task two industrial routers failed to accomplish.