Orbitopal Fixing in SAT

• URL: http://arxiv.org/abs/2601.16855v1
• Date: Fri, 23 Jan 2026 16:01:48 GMT
• Title: Orbitopal Fixing in SAT
• Authors: Markus Anders, Cayden Codel, Marijn J. H. Heule,
• Abstract summary: We present a practical static symmetry breaking approach based on orbitopal fixing.<n>Our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.
• Score: 0.688204255655161
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones already explored. While symmetry handling is routine in other solving paradigms, integrating it into state-of-the-art proof-producing SAT solvers is difficult: added reasoning must be fast, non-interfering with solver heuristics, and compatible with formal proof logging. To address these issues, we present a practical static symmetry breaking approach based on orbitopal fixing, a technique adapted from mixed-integer programming. Our approach adds only unit clauses, which minimizes downstream slowdowns, and it emits succinct proof certificates in the substitution redundancy proof system. Implemented in the satsuma tool, our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.

Related papers

• Evaluating Robustness of Reasoning Models on Parameterized Logical Problems [20.78623024814435]
  Logic provides a controlled testbed for evaluating LLM-based reasoners.<n>Standard SAT-style benchmarks often conflate surface difficulty (length, wording, clause order) with the structural phenomena that actually determine satisfiability.<n>We introduce a diagnostic benchmark for 2-SAT built from parameterized families of structured 2--CNF formulas.
  arXiv  Detail & Related papers  (2026-02-13T06:54:25Z)
• Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning [52.23804865017831]
  We address the problem of verifying closed-loop contraction in nonlinear control systems whose controller and contraction metric are both parameterized by neural networks.<n>We derive a tractable and scalable sufficient condition for closed-loop contractivity that reduces to checking that the dominant eigenvalue of a symmetric Metzler matrix is nonpositive.
  arXiv  Detail & Related papers  (2025-12-01T23:06:56Z)
• Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables [11.274339621648565]
  Most successful approach to deal with bugs is to make solvers certify, so that they output a mathematical proof of correctness in a standard format.<n>This requires justifying symmetry reasoning within the proof, but developing efficient methods for this has remained a long-standing open challenge.<n>We show that this leads to orders-of-magnitude speed-ups in both theory and practice by running experiments on proof logging and checking for SAT symmetry breaking.
  arXiv  Detail & Related papers  (2025-11-20T18:43:05Z)
• Exploiting Symmetries in MUS Computation (Extended version) [11.266189935383476]
  In eXplainable Constraint Solving (XCS), it is common to extract a Minimal Unsatisfiable Subset (MUS) from a set of unsatisfiable constraints.<n>Finding MUSes can be computationally expensive for highly symmetric problems.<n>In this paper, we take inspiration from existing symmetry-handling techniques and adapt well-known MUS-computation methods to exploit symmetries in the specification.
  arXiv  Detail & Related papers  (2024-12-18T08:34:32Z)
• How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization [1.4796543791607086]
  This paper proposes a novel branch-and-bound algorithm for finding the shortest resolution proofs. We show that this representation breaks all permutational symmetries, thereby improving upon the state-of-the-art symmetry-breaking. Our experiments suggest that the proofs from state-of-the-art solvers could be shortened by 30-60% on the instances from SAT Competition 2002 and by 25-50% on small synthetic formulas.
  arXiv  Detail & Related papers  (2024-11-12T17:31:35Z)
• Fully Stochastic Trust-Region Sequential Quadratic Programming for Equality-Constrained Optimization Problems [62.83783246648714]
  We propose a sequential quadratic programming algorithm (TR-StoSQP) to solve nonlinear optimization problems with objectives and deterministic equality constraints. The algorithm adaptively selects the trust-region radius and, compared to the existing line-search StoSQP schemes, allows us to utilize indefinite Hessian matrices.
  arXiv  Detail & Related papers  (2022-11-29T05:52:17Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• Certified Symmetry and Dominance Breaking for Combinatorial Optimisation [13.333957453318744]
  We develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. We apply our method to maximum clique solving and constraint as a proof of concept that the approach applies to a wider range of problems.
  arXiv  Detail & Related papers  (2022-03-23T08:45:35Z)
• E-detectors: a nonparametric framework for sequential change detection [86.15115654324488]
  We develop a fundamentally new and general framework for sequential change detection. Our procedures come with clean, nonasymptotic bounds on the average run length. We show how to design their mixtures in order to achieve both statistical and computational efficiency.
  arXiv  Detail & Related papers  (2022-03-07T17:25:02Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.