Orthologic for SAT Solving

• URL: http://arxiv.org/abs/2605.16421v1
• Date: Thu, 14 May 2026 13:05:57 GMT
• Title: Orthologic for SAT Solving
• Abstract summary: We introduce a family of synthetic SAT benchmarks based on the observation that, for any formula $$, the equivalence $leftrightarrow mathrmNF_mathrmOL()$ is a tautology.<n>We show that using orthologic normalization as a preprocessing step can improve SAT solving time on some hard problems.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• 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 $φ$, the equivalence $φ\leftrightarrow \mathrm{NF}_{\mathrm{OL}}(φ)$ 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 can improve SAT solving time on some hard problems.

Related papers

• A parallel and distributed fixed-point quantum search algorithm for solving SAT problems [6.341973606434514]
  Solving the SAT problem requires $mathcalO(sqrt2n)$ queries--where n denotes the number of logic variables in the problem.<n>We propose a parallel fixed-point (PFP) search algorithm to solve the SAT problem.
  arXiv  Detail & Related papers  (2026-04-11T01:28:20Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  We propose two algorithms that enjoy provable scaling laws for the test-time compute of large language models.<n>One is a two-stage knockout-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.<n>The other is a two-stage league-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.
  arXiv  Detail & Related papers  (2024-11-29T05:29:47Z)
• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• Can Transformers Reason Logically? A Study in SAT Solving [17.15701291424892]
  We study the logical reasoning capabilities of decoder-only Transformers in the context of the satisfiability (SAT) problem.<n>We prove by construction that decoder-only Transformers can decide 3-SAT, in a non-uniform model of computation, using backtracking and deduction via Chain-of-Thought (CoT)
  arXiv  Detail & Related papers  (2024-10-09T21:01:52Z)
• Sum-of-Squares inspired Quantum Metaheuristic for Polynomial Optimization with the Hadamard Test and Approximate Amplitude Constraints [76.53316706600717]
  Recently proposed quantum algorithm arXiv:2206.14999 is based on semidefinite programming (SDP) We generalize the SDP-inspired quantum algorithm to sum-of-squares. Our results show that our algorithm is suitable for large problems and approximate the best known classicals.
  arXiv  Detail & Related papers  (2024-08-14T19:04:13Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• Longest Common Substring and Longest Palindromic Substring in $\tilde{\mathcal{O}}(\sqrt{n})$ Time [0.0]
  The Longest Common Substring (LCS) and Longest Palindromic Substring (LPS) are classical problems in computer science. We present a quantum algorithm for both LCS and LPS working in the circuit model of computation.
  arXiv  Detail & Related papers  (2023-09-03T19:27:57Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SAT is a fundamental NP-complete problem with many applications, including automated scheduling. To solve large instances, SAT solvers have to rely on Booleans, e.g., choosing a branching variable in DPLL and CDCL solvers. We suggest a strategy of making a few initial steps with a trained ML model and then releasing control to classical runtimes.
  arXiv  Detail & Related papers  (2023-07-18T10:46:28Z)
• Accelerating Inexact HyperGradient Descent for Bilevel Optimization [84.00488779515206]
  We present a method for solving general non-strongly-concave bilevel optimization problems. Our results also improve upon the existing complexity for finding second-order stationary points in non-strongly-concave problems.
  arXiv  Detail & Related papers  (2023-06-30T20:36:44Z)
• 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)
• 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)
• Randomized Stochastic Variance-Reduced Methods for Stochastic Bilevel Optimization [62.87181271021217]
  We consider non-SBO problems that have many applications in machine learning. This paper proposes fast randomized algorithms for non-SBO problems.
  arXiv  Detail & Related papers  (2021-05-05T18:28:42Z)

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.