Search
Search Results
-
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper...
-
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information...
-
Propositional Proof Skeletons
Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the...
-
CHC Model Validation with Proof Guarantees
Formal verification tooling increasingly relies on logic solvers as automated reasoning engines. A point of commonality among these solvers is the...
-
Unsatisfiability of Comparison-Based Non-malleability for Commitments
There are two distinct formulations of non-malleability of commitments found in the literature: the comparison-based definition and the...
-
A Resolution-Based Interactive Proof System for UNSAT
Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless...
-
Towards a Certified Proof Checker for Deep Neural Network Verification
Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for...
-
Proof-Guided Underapproximation Widening for Bounded Model Checking
Bounded Model Checking (BMC) is a popularly used strategy for program verification and it has been explored extensively over the past decade. Despite...
-
Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format
Proofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical...
-
Preprocessing of Propagation Redundant Clauses
The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven...
-
Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using...
-
In the Head of the Beholder: Comparing Different Proof Representations
Ontologies provide the logical underpinning for the Semantic Web, but their consequences can sometimes be surprising and must be explained to users....
-
The Packing Chromatic Number of the Infinite Square Grid is 15
A packing k-coloring is a natural variation on the standard notion of graph k-coloring, where vertices are assigned numbers from...
-
Flexible Proof Production in an Industrial-Strength SMT Solver
Proof production for SMT solvers is paramount to ensure their correctness independently from implementations, which are often prohibitively difficult...
-
Proof Complexity of Modal Resolution
We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al....
-
On the lengths of tree-like and Dag-like cutting plane refutations of Horn constraint systems
In this paper, we investigate the properties of cutting plane based refutations for a class of integer programs called Horn constraint systems (HCSs). ...
-
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for...
-
Clausal Proofs for Pseudo-Boolean Reasoning
When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when...
-
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
In the last decade, numerous algorithms for single-objective Boolean optimization have been proposed that rely on the iterative usage of a highly...