Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to nonfederal websites. Their policies may differ from this site.

Bertot, Yves ; Kutsia, Temur ; Norrish, Michael (Ed.)A recent breakthrough in computerassisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem with a combination of geometric insights and automated reasoning techniques by constructing CNF formulas ϕ_n, with O(n⁴) clauses, such that if ϕ_n is unsatisfiable then every set of n points in general position must contain an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17 300 CPU hours of parallel computation. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers ideas in discrete computational geometry and SAT encoding techniques by introducing a framework that connects geometric objects to propositional assignments. We see this as a key step towards the formal verification of other SATbased results in geometry, since the abstractions we use have been successfully applied to similar problems. Overall, we hope that our work sets a new standard for the verification of geometry problems relying on extensive computation, and that it increases the trust the mathematical community places in computerassisted proofs.more » « lessFree, publiclyaccessible full text available September 2, 2025

Chakraborty, Supratik ; Jiang, JieHong Roland (Ed.)Quantum Computing (QC) is a new computational paradigm that promises significant speedup over classical computing in various domains. However, nearterm QC faces numerous challenges, including limited qubit connectivity and noisy quantum operations. To address the qubit connectivity constraint, circuit mapping is required for executing quantum circuits on quantum computers. This process involves performing initial qubit placement and using the quantum SWAP operations to relocate nonadjacent qubits for nearestneighbor interaction. Reducing the SWAP count in circuit mapping is essential for improving the success rate of quantum circuit execution as SWAPs are costly and errorprone. In this work, we introduce a novel circuit mapping method by combining incremental and parallel solving for Boolean Satisfiability (SAT). We present an innovative SAT encoding for circuit mapping problems, which significantly improves solverbased mapping methods and provides a smooth tradeoff between compilation quality and compilation time. Through comprehensive benchmarking of 78 instances covering 3 quantum algorithms on 2 distinct quantum computer topologies, we demonstrate that our method is 26× faster than stateoftheart solverbased methods, reducing the compilation time from hours to minutes for important quantum applications. Our method also surpasses the existing heuristics algorithm by 26% in SWAP count.more » « lessFree, publiclyaccessible full text available August 19, 2025

Adding blocked clauses to a CNF formula can substantially speed up SATsolving, both in theory and practice. In theory, the addition of blocked clauses can exponentially reduce the length of the shortest refutation for a formula [17, 19]. In practice, it has been recently shown that the runtime of CDCL solvers decreases significantly for certain instance families when blocked clauses are added as a preprocessing step [10,22]. This fact is in contrast to, but not in contradiction with, prior results showing that Blocked Clause Elimination (BCE) is sometimes an effective preprocessing step [14,15]. We suggest that the practical role of blocked clauses in SATsolving might be richer than expected. Concretely, we propose a theoretical study of the complexity of BlockedClause Addition (BCA) as a preprocessing step for SATsolving, and in particular, consider the problem of adding the maximum number of blocked clauses of a given arity k to an input formula F. While BCE is a confluent process, meaning that the order in which blocked clauses are eliminated is irrelevant, this is not the case for BCA: adding a blocked clause to a formula might unblock a different clause that was previously blocked. This ordersensitivity turns out to be a crucial obstacle for carrying out BCA efficiently as a preprocessing step. Our main result is that computing the maximum number of kary blocked clauses that can be added to an input formula F is NPhard for every k ≥ 2.more » « lessFree, publiclyaccessible full text available May 27, 2025

Free, publiclyaccessible full text available April 6, 2025

Nadel, Alexander ; Rozier, Kristin Yvonne (Ed.)Satisfiability (SAT) solvers are versatile tools that can solve a wide array of problems, and the models and proofs of unsatisfiability emitted by SAT solvers can be checked by verified software. In this way, the SAT toolchain is trustworthy. However, many applications are not expressed natively in SAT and must instead be encoded into SAT. These encodings are often subtle, and implementations are errorprone. Formal correctness proofs are needed to ensure that implementations are bugfree. In this paper, we present a library for formally verifying SAT encodings, written using the Lean interactive theorem prover. Our library currently contains verified encodings for the parity, atmostone, and atmostk constraints. It also contains methods of generating fresh variable names and combining subencodings to form more complex ones, such as one for encoding a valid Sudoku board. The proofs in our library are general, and so this library serves as a basis for future encoding efforts.more » « less

Nadel, Alexander ; Rozier, Kristin Yvonne (Ed.)Satisfiability (SAT) solvers are versatile tools that can solve a wide array of problems, and the models and proofs of unsatisfiability emitted by SAT solvers can be checked by verified software. In this way, the SAT toolchain is trustworthy. However, many applications are not expressed natively in SAT and must instead be encoded into SAT. These encodings are often subtle, and implementations are errorprone. Formal correctness proofs are needed to ensure that implementations are bugfree. In this paper, we present a library for formally verifying SAT encodings, written using the Lean interactive theorem prover. Our library currently contains verified encodings for the parity, atmostone, and atmostk constraints. It also contains methods of generating fresh variable names and combining subencodings to form more complex ones, such as one for encoding a valid Sudoku board. The proofs in our library are general, and so this library serves as a basis for future encoding effortsmore » « less

Sankaranarayanan, S. ; Sharygina, N. (Ed.)Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the wellknown DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for semantic proof compression that selects a subset of important clauses from a proof and stores them as a socalled proof skeleton. This proof skeleton can later be used to efficiently reconstruct a full proof by exploiting parallelism. We implemented our approach on top of the awardwinning SAT solver CaDiCaL and the proof checker DRATtrim. In an experimental evaluation, we demonstrate that we can compress proofs into skeletons that are 100 to 5,000 times smaller than the original proofs. For almost all problems, proof reconstruction using a skeleton improves the solving time on a single core, and is around five times faster when using 24 cores.more » « less