More Like this

1. Preprocessing of Propagation Redundant Clauses

   Reeves, Joseph E. ; Bryant, Randal E. ; Heule, Marijn J. ( August 2022 , Lecture notes in computer science)

   Blanchette, Jasmin ; Kovacs, Laura ; Pattinson, Dirk (Ed.)

   The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven clause learning (CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solver SaDiCaL incorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We present prExtract, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large portion of SAT competition benchmarks we found that preprocessing with prExtract improves solver performance. In addition, there were several satisfiable and unsatisfiable formulas that could only be solved after preprocessing with prExtract. prExtract supports proof logging, giving a high level of confidence in the results. 

   more » « less
2. Encoding Redundancy for Satisfaction-Driven Clause Learning

   https://doi.org/10.1007/978-3-030-17462-0_3  

   Heule, Marijn ; Kiesl, Benjamin ; Biere, Armin ( April 2019 , International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   Satisfaction-Driven Clause Learning (SDCL) is a recent SAT solving paradigm that aggressively trims the search space of possible truth assignments. To determine if the SAT solver is currently exploring a dispensable part of the search space, SDCL uses the so-called positive reduct of a formula: The positive reduct is an easily solvable propositional formula that is satisfiable if the current assignment of the solver can be safely pruned from the search space. In this paper, we present two novel variants of the positive reduct that allow for even more aggressive pruning. Using one of these variants allows SDCL to solve harder problems, in particular the well-known Tseitin formulas and mutilated chessboard problems. For the first time, we are able to generate and automatically check clausal proofs for large instances of these problems. 

   more » « less
3. Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers

   Li, C ; Fleming, N ; Vinyals, M ; Pitassi, T ; Ganesh, V. ( June 2020 , SAT 2020: International Conference on Theory and Applications of Satisfiability Testing)

   Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical understanding of whether restarts are indeed crucial to the power of CDCL solvers is missing. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a drunk randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection. 

   more » « less
4. Generating Extended Resolution Proofs with a BDD-Based SAT Solver

   https://doi.org/10.1145/3595295  

   Bryant, Randal E. ; Heule, Marijn J. ( October 2023 , ACM Transactions on Computational Logic)

   In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a BDD-based solver, implemented by extending an existing BDD package, to several challenging Boolean satisfiability problems. Our results demonstrate scaling for parity formulas as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers. 

   more » « less
5. (Nearly) Model-independent Constraints on the Neutral Hydrogen Fraction in the Intergalactic Medium at z ∼ 5–7 Using Dark Pixel Fractions in Lyα and Lyβ Forests

   https://doi.org/10.3847/1538-4357/aca678  

   Jin, Xiangyu ; Yang, Jinyi ; Fan, Xiaohui ; Wang, Feige ; Bañados, Eduardo ; Bian, Fuyan ; Davies, Frederick B. ; Eilers, Anna-Christina ; Farina, Emanuele Paolo ; Hennawi, Joseph F. ; et al ( January 2023 , The Astrophysical Journal)

   Cosmic reionization was the last major phase transition of hydrogen from neutral to highly ionized in the intergalactic medium (IGM). Current observations show that the IGM is significantly neutral atz> 7 and largely ionized byz∼ 5.5. However, most methods to measure the IGM neutral fraction are highly model dependent and are limited to when the volume-averaged neutral fraction of the IGM is either relatively low (${\overline{x}}_{\mathrm{H}\mathrm{I}}\lesssim {10}^{-3}$) or close to unity (${\overline{x}}_{\mathrm{H}\mathrm{I}}\sim 1$). In particular, the neutral fraction evolution of the IGM at the critical redshift range ofz= 6–7 is poorly constrained. We present new constraints on${\overline{x}}_{\mathrm{H}\mathrm{I}}$atz∼ 5.1–6.8 by analyzing deep optical spectra of 53 quasars at 5.73 <z< 7.09. We derive model-independent upper limits on the neutral hydrogen fraction based on the fraction of “dark” pixels identified in the Lyαand Lyβforests, without any assumptions on the IGM model or the intrinsic shape of the quasar continuum. They are the first model-independent constraints on the IGM neutral hydrogen fraction atz∼ 6.2–6.8 using quasar absorption measurements. Our results give upper limits of${\overline{x}}_{\mathrm{H}\mathrm{I}}(z=6.3)<0.79\pm 0.04$(1σ),${\overline{x}}_{\mathrm{H}\mathrm{I}}(z=6.5)<0.87\pm 0.03$(1σ), and${\overline{x}}_{\mathrm{H}\mathrm{I}}(z=6.7)<{0.94}_{-0.09}^{+0.06}$(1σ). The dark pixel fractions atz> 6.1 are consistent with the redshift evolution of the neutral fraction of the IGM derived from Planck 2018.

    

   more » « less