ABSTRACT. We present a methodology for designing SAT encodings of integer multiplication guided by proof trace analysis. By examining DRAT proofs, we identify structural bottlenecks—the top bottleneck variable in standard Comba encoding appears in 31% of all proof steps—and use these findings to redesign the encoding. This methodology produced comba-cs, a carry-save Comba encoding that separates column reduction from carry propagation, achieving 2.6–71× speedup across four SAT solvers. We further show that carry propagation is the dominant driver of SAT hardness for multiplication—not merely correlated with it. A controlled experiment holds the partial-product layout and accumulation topology fixed and varies only the accumulator (integer addition vs. GF(2) XOR): integer commutativity is at least 1000× harder than GF(2) at bitwidth 12, and structural variations (sequential vs. parallel-tree accumulation) change running time by less than 5×. This establishes causation for the commutativity pattern on CaDiCaL. Comparing comba-cs with pre-existing alternative encodings (Booth radix-4, 4-bit blocks, sorting networks), we find that no single encoding dominates: Booth is 17× faster on strength-reduction benchmarks, while comba-cs is 2× faster on bfloat16 commutativity. The optimal encoding depends on problem structure, motivating adaptive selection.

ABSTRACT. Cardinality constraints in Boolean satisfiability (SAT) problems are typically encoded as sets of clauses in conjunctive normal form, which serves as the standard input format of SAT solvers. The ordering of data variables within a cardinality constraint can have a substantial impact on the quality of the resulting encoding and on solver performance, motivating the development of various pre-processing and reordering techniques. In this work, we address the scenario in which a cardinality constraint has already been encoded into clauses. We introduce a proof-producing reencoding method that systematically transforms an existing encoding into a new encoding with reordered data variables, while producing a certificate that establishes satisfiability equivalence between the original and transformed formulas. To illustrate the practical advantages of our approach, we evaluate it using a family of vertex cover benchmarks specifically designed with adversarial variable orderings.

ABSTRACT. In modern combinatorial solving and automated reasoning systems, proof logging and checking is a highly effective way to provide trust in solver outputs. For Boolean satisfiability (SAT), a technique called proof trimming is vital to allow rapid proof checking and reduce the size of stored proofs. However, trimming remains a challenge for richer proof systems. In this work, we design, implement, and evaluate a proof trimmer for the VeriPB proof format, bringing the advantages of trimming to a wide range of certifying solvers, including those for pseudo Boolean optimisation, MaxSAT, constraint programming, and subgraph solving, and for SAT solvers that use techniques like symmetry or cardinality reasoning. We describe and justify the overall architecture of our system, and give details of how the more challenging proof rules are handled. Our experiments demonstrate large reductions in proof size, without compromising correctness, as well as significant speedups for proof checking including formally verified checking.

ABSTRACT. We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4. Key to our approach is REFLECTION: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code. Our method scales to proofs with tens of thousands of steps that would exhaust memory under explicit proof-term construction. Our checker parses all \veripb kernel rule types and verifies unsatisfiability via cutting-plane derivations, proof-by-contradiction subproofs, and redundance/dominance for symmetry breaking; soundness is established in Lean for the rules used along the UNSAT path. In contrast to external verified checkers that produce verdicts, our integration yields Lean theorems that can serve as composable lemmas in larger formal developments. To derive theorems about the original combinatorial problems rather than about PB constraints alone, we support verified encodings. This closes the trust gap between solver output and problem semantics since the constraint translation and its correctness proof are both formalized in Lean. We demonstrate the approach on various combinatorial problems.

ABSTRACT. Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZKUNSAT, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZKUNSAT demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability. Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZkUnsat without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZkUnsat on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.

ABSTRACT. Maximum Satisfiability (MaxSAT) is an approach for solving NP-hard optimization problems expressed in propositional logic. Among the known approaches for solving MaxSAT is the Implicit Hitting Set approach that combines SAT solvers and Integer Linear Programming solvers. No Implicit Hitting solver participated in the most important evaluation of state-of-the-art MaxSAT solvers—the annual MaxSAT Evaluation—since MaxHS did in 2022. Since then, MaxHS remains unmaintained and is not allowed to participate under the current ruleset. Further, recent advances in MaxSAT testing have revealed numerous bugs in MaxHS. In this paper, we describe our revision of MaxHS, which include numerous bugfixes, the integration of an open source Integer Linear Programming solver that allows MaxHS to participate in the evaluation, and an exact mode that avoids numerical problems.

ABSTRACT. Anytime MaxSAT solving is indispensable in applications that require finding near-optimal solutions within a flexible, user-controlled time budget. Recent years have seen substantial progress in anytime MaxSAT algorithms, including the introduction of SAT-based local search, the development of efficient approximation techniques, and significant advances in classical local search methods. However, all leading anytime solvers—including the winners of the three most recent MaxSAT Evaluations (MSEs) in the anytime categories—reuse the code base of a single solver, tt-open-wbo-inc. While highly efficient, this code base lacks an in-memory API, is non-incremental and incomplete, and contains a substantial amount of dead and legacy code. We introduce Aperture, a new solver for SAT-based optimization, including MaxSAT, written from scratch in C++ with in-memory APIs for C++ (IPAMIR-compliant) and Python. For MaxSAT, Aperture is anytime, incremental, and complete; algorithmically, it follows a similar high-level approach to tt-open-wbo-inc, but employs a unified flow for both weighted and unweighted MaxSAT. Performance-wise, Aperture is highly competitive as a MaxSAT solver. Under the benchmark sets and evaluation conditions of MSE 2024, it outperforms both the MSE 2024 winner SPB-MaxSAT-c and tt-open-wbo-inc in all four anytime categories, and in 8 out of 12 anytime categories across the three most recent MSEs (2022–2024). Moreover, Aperture outperforms leading non-anytime MaxSAT solvers on 2 out of the 6 incremental benchmark sets from MSE 2022, an evaluation setting in which—unlike the anytime categories—both incrementality and completeness are mandatory. Beyond MaxSAT, Aperture also supports other paradigms for optimizing an objective function under Boolean constraints, including Optimization Modulo Bitvectors (OBV) and black-box optimization. Across all supported paradigms, the solver is incremental and anytime; it is complete for MaxSAT and OBV, but incomplete for black-box optimization.

ABSTRACT. We revisit the problem of computing a smallest minimal unsatisfiable subset (SMUS) of a propositional CNF formula. The state-of-the-art algorithm by Ignatiev et al. frames SMUS extraction as finding a minimum-cardinality hitting set of the set of minimal correction sets (MCSes), and solves the resulting optimization problem by a generate-and-test loop over a growing MCS collection. We propose to replace the hitting-set loop with a full branch-and-cut solver—concretely, SCIP augmented with a custom constraint handler—so that every incumbent solution discovered during the search is a valid UNSAT subset, giving a monotonically improving anytime sequence. The feasibility is enforced by a separation oracle that, given a fractional point in the LP relaxation, identifies a violated MCS inequality by solving an instance of the weighted MaxSAT problem. Experimental evaluation suggests that, although the formulas with smaller gaps between the smallest MUS cardinality and the number of disjoint MCSes in a formula, such as the ones from the MUS track of the SAT Competition 2011, are favorable for implicit hitting set solving, our branch-and-cut approach is superior to the implicit hitting set approach on formulas with large gaps.

ABSTRACT. In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking to keep the clause database compact, thereby reducing the memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best.

ABSTRACT. State-of-the-art projected model counters have achieved remarkable advances by integrating a variety of methods, including those from SAT solvers. However, this has resulted in increasingly complex implementations. Furthermore, the integration of multiple methods may introduce unexpected inconsistencies, leading to incorrect model counts. To address these issues, we propose a declarative framework for describing the projected-model counting procedure that integrates practical methods. Our framework captures all methods implemented in GPMC, one of the state-of-the-art projected model counters, while remaining open to future extensions. We also present a proof sketch for the correctness of the framework, outlining the key ideas.

ABSTRACT. Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve due to their sophisticated algorithms and highly optimized data structures. Understanding these complex mechanics and evaluating the effectiveness of problem encodings is notoriously challenging for students and emerging researchers. To ease this learning process, we introduce the Interactive SAT Tracer (SAT-IT), an open-access web environment designed to make the foundations of SAT solving highly visible and interactive. SAT-IT offers a staged pedagogical progression—from naive backtracking to DPLL and full CDCL with the two-watched literals scheme. Users can clearly inspect fundamental data structures, search space trails, and solving statistics. The tool interactive search space exploration is boosted with literal-level breakpoints for targeted inspection, alongside versatile automatic solving modes that offer both continuous real-time execution and state-based subroutine automation. Combined with a powerful ``what-if'' capability for stepping backward to explore alternative decisions, an instance manager, and an extensible architecture ready to support additional algorithms, SAT-IT serves as a practical, granular lens for experimenting with SAT solving algorithms and analysing encodings efficiency.

ABSTRACT. Steiner triple systems (STS) and subsets of these known as partial STS (PSTS) are combinatorial objects that have received substantial interest from mathematicians since their introduction in 1847. Over the last three decades, (P)TS have found applications in diverse fields ranging from digital circuit testing to wireless transmission. Perhaps unsurprisingly, the ``triple'' in (P)STS allows for a mapping to 3-conjunctive normal form (3-CNF) formulas, the Boolean formula used as input to 3-SAT. Prompted by this ready conversion of (P)STS to 3-CNF formulas and numerous real-world applications of (P)STS, we explore the intersection of (P)STS with 3-SAT and its counting version #3-SAT. We explain the properties of (P)STS-generated 3-CNF formulas in terms familiar to the SAT community and experimentally compare them against randomly-generated 3-CNF formulas. We find that PSTS-3-CNF formulas are statistically distinct from randomly generated 3-CNF formulas, in both probability of satisfiability and expected solution count.

ABSTRACT. This paper addresses the Multi-Skill Project Scheduling Problem (MSPSP), an NP-hard optimization problem. We propose and evaluate MaxSAT and pseudo-Boolean optimization encoding for the MSPSP. We explore the fundamental trade-off between the expressive power of pseudo-Boolean (PB) constraints and the raw efficiency of MaxSAT solvers. By adapting implied constraints naturally expressed as PB constraints from the literature, we examine whether such additional reasoning provides a greater performance boost to MaxSAT or PB solvers. Our initial hypothesis---that including natural PB constraints into our MSPSP model would provide a greater incremental boost to PB solvers than to MaxSAT solvers---was tested through an exhaustive experimental evaluation using state-of-the-art solvers. Contrary to our expectations, MaxSAT solvers consistently outperform PB solvers on the MSPSP. Moreover, our results demonstrate the benefits of integrating implied constraints, as they significantly reduce the number of timeouts, regardless of the formalism used.

ABSTRACT. We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementations while retaining the same $\mathcal{O}(n^2(1+|A|))$ worst-case complexity. We then introduce a family of synthetic SAT benchmarks based on the observation that, for any formula $\phi$, the equivalence $\phi \leftrightarrow \mathrm{NF}_{\mathrm{OL}}(\phi)$ is a tautology whose Tseitin encoding yields unsatisfiable instances that are hard for state-of-the-art SAT solvers yet have short orthologic proofs. Applied to EPFL arithmetic circuits, our algorithm solves these instances efficiently while Kissat times out on a significant fraction. Finally, we show that using orthologic normalization as a preprocessing step reduces formula size and solving time by approximately 26\% on average over a large set of Boolean circuit benchmarks.

ABSTRACT. State-of-the-art SAT solvers from the SAT Competition are all using a local search component. Experimentally at the beginning of the search, many better assignment are found; so we developed a new method to not store those each time, based on caching flips. This method was already part of Kissat but was not described so far. We also describe the implementation in CaDiCaL which reuses watch lists instead of using full-occurrence lists. Finally, we ported the new \tassat algorithm to CaDiCaL improving the performance of CaDiCaL.

ABSTRACT. Local Search (LS) solvers for SAT can surpass CDCL solvers on some prominent satisfiable industrial and combinatorial benchmarks. They operate by flipping variable assignments and maintaining per-variable scores incrementally to guide variable selection, so performance is largely determined by how efficiently each flip is executed. We revisit a largely forgotten data structure that reduces per-flip overhead by eliminating costly clause scans. We dub this scheme NobleCount, integrate it into the leading LS solver ProbCCAnr, and evaluate it on industrial FCC spectrum-repacking instances and the SC22 anniversary track, two standard testbeds for modern LS solvers. ProbCCAnr with NobleCount achieves new state-of-the-art results on both benchmarks. On FCC, where it already overtook not only other LS solvers but also leading CDCL solvers, employing NobleCount further reduces PAR2 by 24.8% at a 20s timeout, with consistent PAR2 gains across all timeouts up to our final 300s timeout. On SC22, at longer timeouts where another LS solver, TaSSAT, originally overtakes ProbCCAnr, NobleCount lifts ProbCCAnr to outperform TaSSAT in PAR2 score.

ABSTRACT. Solving hard combinatorial problems such as the minimum Kochen-Specker problem requires finding all solutions to large Boolean satisfiability (ALLSAT) formulas, pushing the limits of existing parallel solver infrastructure. We present ams-dist, a new distributed hybrid solver that combines Cube & Conquer and portfolio solving. Building on AlphaMapleSAT-CnC, ams-dist introduces four key improvements: a fully distributed MPI manager-worker architecture, a portfolio clause-sharing simplification phase in which groups of workers collaboratively simplify subproblems in parallel, a distributed beam lookahead cubing procedure with a balanced scoring objective, and a progress-based work-stealing policy during the conquering phase that uses irredundant clause count to estimate subproblem difficulty. These improvements maintain substantially higher core utilization throughout execution compared to the baseline AlphaMapleSAT-CnC. We evaluate ams-dist on Kochen-Specker instances of orders 17-22 on a computing cluster at up to 3072 cores, comparing against the distributed pure portfolio solvers painless and MallobSat. ams-dist achieves consistent speedups of 1.5-3× on tractable instances and is the only solver to solve order-22 instances within a 6-hour timeout.

ABSTRACT. Majority Inverter Graphs (MIG) have been shown to be an excellent basis for circuit representation. However, no Circuit-SAT solvers that accept MIGs natively exist currently. Current Circuit-SAT solvers operate only on AND, OR, and XOR gates, not majority functions. Furthermore, majority gates are difficult for traditional CDCL solvers to tackle due to their large Tseitin transformation. This paper introduces a new CDCL Circuit-SAT solver, named MIGSat, that can efficiently operate on the majority basis by employing novel techniques, including: (1) a watchlist mechanism for the Majority function, (2) an efficient BCP mechanism, including a MiniSat-style blocker for the majority function, (3) a Tseytin clause derivation method for conflict analysis of the majority function, and (4) a MIG specific branching heuristic based on EVSIDS. We also implemented versions of existing heuristics, like LBD and activity-based clause deletion and clause simplification, to improve performance. Lastly, we demonstrated that our solver generally matches the performance of MiniSat on Miter circuits, and can be significantly faster than MiniSat and Kissat on Pigeonhole Circuits. Although still limited in its raw solving power, MIGSat can serve as a foundation for additional research in Circuit-SAT on the MIGs.

ABSTRACT. Compiling constraint models to conjunctive normal form (CNF) is commonly regarded as a one-way transformation, since auxiliary variables and clausal decomposition obscure the original problem structure. Related methods of structure recovery include gate extraction and cardinality detection, but those recover only fragments, not the complete encoding. We present an autonomous agent, powered by an LLM, that reverse-engineers a complete, semantically equivalent PySAT encoding from a DIMACS CNF file. We use a SAT-based equivalence checker to verify the high-level encoding and obtain counterexamples for iterative refinement. The agent queries the formula through bounded analysis tools. It combines structural with abductive reasoning to hypothesize the underlying combinatorial problem. We evaluate our approach on several combinatorial problems with instances generated by independent encoders (PySAT, Picat, Sugar, BEE), giving the agent no metadata. We obtain 85 reconstruction on 48 instances and demonstrate that the agent handles direct, order, and log encodings of the same problems. Our scaling study confirms feasibility up to 1.2 million clauses.

ABSTRACT. In The Art of Computer Programming, Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen’s graph: the minimum number of colors needed to color the squares of an n x n chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis substantially by comparing thousands of encodings for the same problem, thereby identifying additional factors that are important for solver performance. We obtain 1584 encodings for this problem by varying (a) the constraints that encode which color is assigned to each cell, (b) the constraints that forbid the same color appearing in a row, column, or diagonal line, and (c) the symmetry-breaking constraints. We find that the three most impactful encoding factors are (i) the choice of symmetry-breaking constraints, (ii) enabling so-called clique hints, and (iii) enforcing that each cell is assigned exactly one color through blocked clauses. Furthermore, while Knuth proposed clique hints as an advantage of the order encoding, we show in fact that they can be effectively employed for the one-hot encoding as well.

ABSTRACT. We introduce power term polynomial algebra, a representation language for Boolean formulae designed to bridge conjunctive normal form (CNF) and algebraic normal form (ANF). The language is motivated by the tiling mismatch between these representations: direct CNF↔ANF conversion may cause exponential blowup unless formulas are decomposed into smaller fragments, typically through auxiliary variables and side constraints. In contrast, our framework addresses this mismatch within the representation itself, compactly encoding structured families of monomials while representing CNF clauses directly, thereby avoiding auxiliary variables and constraints at the abstraction level. We formalize the language through power terms and power term polynomials, define their semantics, and show that they admit algebraic operations corresponding to Boolean polynomial addition and multiplication. We prove several key properties of the language: disjunctive clauses admit compact canonical representations; power terms support local shortening and expansion rewrite rules; and products of atomic terms can be systematically rewritten within the language. Together, these results yield a symbolic calculus that enables direct manipulation of formulas without expanding them into ordinary ANF. The resulting framework provides a new intermediate representation and rewriting calculus that bridges clause-based and algebraic reasoning and suggests new directions for structure-aware CNF↔ANF conversion and hybrid reasoning methods.