Cover Image

How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Sidorov, Konstantin, van der Linden, Koos, Correia, Gonçalo Homem de Almeida, de Weerdt, Mathijs, Demirović, Emir
Format:	Preprint
Published:	2024
Subjects:	Artificial Intelligence I.2.8
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Necessary and Sufficient Conditions for Optimal Decision Trees using Dynamic Programming
by: van der Linden, Jacobus G. M., et al.
Published: (2023)

Optimal or Greedy Decision Trees? Revisiting their Objectives, Tuning, and Performance
by: van der Linden, Jacobus G. M., et al.
Published: (2024)

Optimal Classification Trees for Continuous Feature Data Using Dynamic Programming with Branch-and-Bound
by: Brita, Catalin E., et al.
Published: (2025)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
by: Feng, Nick, et al.
Published: (2024)

Optimal Survival Trees: A Dynamic Programming Approach
by: Huisman, Tim, et al.
Published: (2024)

T-STAR: A Context-Aware Transformer Framework for Short-Term Probabilistic Demand Forecasting in Dock-Based Shared Micro-Mobility
by: Cheng, Jingyi, et al.
Published: (2026)

Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects
by: Feng, Nick, et al.
Published: (2024)

Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds
by: Li, Jiawei, et al.
Published: (2024)

Epsilon Calculus Provides Shorter Cut-Free Proofs
by: Baaz, Matthias, et al.
Published: (2024)

Optimizing Electric Carsharing System Operations and Battery Management: Integrating V2G, B2G and Battery Swapping Strategies
by: Yang, Shuang, et al.
Published: (2024)

SORTeD Rashomon Sets of Sparse Decision Trees: Anytime Enumeration
by: Arslan, Elif, et al.
Published: (2025)

Revisiting Landmarks: Learning from Previous Plans to Generalize over Problem Instances
by: Hanou, Issa, et al.
Published: (2025)

Complexity of Scheduling Charging in the Smart Grid
by: de Weerdt, Mathijs, et al.
Published: (2017)

A Penalty-Based Guardrail Algorithm for Non-Decreasing Optimization with Inequality Constraints
by: Stepanovic, Ksenija, et al.
Published: (2024)

To the Max: Reinventing Reward in Reinforcement Learning
by: Veviurko, Grigorii, et al.
Published: (2024)

You Shall Pass: Dealing with the Zero-Gradient Problem in Predict and Optimize for Convex Optimization
by: Veviurko, Grigorii, et al.
Published: (2023)

In Search of Trees: Decision-Tree Policy Synthesis for Black-Box Systems via Search
by: Demirović, Emir, et al.
Published: (2024)

Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size
by: de Rezende, Susanna F., et al.
Published: (2026)

Enumerating Minimal Unsatisfiable Cores of LTLf formulas
by: Ielo, Antonio, et al.
Published: (2024)

Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets
by: Lymperopoulos, Panagiotis, et al.
Published: (2024)

Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
by: Cosler, Matthias, et al.
Published: (2026)

On inferring cumulative constraints
by: Sidorov, Konstantin
Published: (2026)

Edge-Colored Clustering in Hypergraphs: Beyond Minimizing Unsatisfied Edges
by: Crane, Alex, et al.
Published: (2025)

Precomputing Multi-Agent Path Replanning using Temporal Flexibility
by: Hanou, Issa, et al.
Published: (2026)

Domain-Independent Dynamic Programming with Constraint Propagation
by: Marijnissen, Imko, et al.
Published: (2026)

Lean on Vampire Proofs (Short Paper)
by: Bodingbauer, Jonas, et al.
Published: (2026)

A Short Proof of the Poincaré Conjecture
by: Dunwoody, M. J.
Published: (2025)

Proof Minimization in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

Autoritarismo global – reflexões e questões
by: Alex Demirović
Published: (2022)

Para que fim e de que forma criticar o Estado?
by: Alex Demirović
Published: (2014)

Unentanglement and Post-Measurement Branching in Quantum Interactive Proofs
by: Grewal, Sabee, et al.
Published: (2025)

EXPObench: Benchmarking Surrogate-based Optimisation Algorithms on Expensive Black-box Functions
by: Bliek, Laurens, et al.
Published: (2021)

Formulation and Proof of the Gravitational Entropy Bound
by: Averin, Artem
Published: (2024)

Security Proof for Variable-Length Quantum Key Distribution
by: Tupkary, Devashish, et al.
Published: (2023)

Interpolation in Proof Theory
by: van der Giessen, Iris, et al.
Published: (2026)

Proving Unsatisfiability with Hitting Formulas
by: Filmus, Yuval, et al.
Published: (2023)

A Short Proof of Knuth's Old Sum
by: Adegoke, Kunle
Published: (2024)

Proofs as Explanations: Short Certificates for Reliable Predictions
by: Blum, Avrim, et al.
Published: (2025)

Does Subset Sum Admit Short Proofs?
by: Włodarczyk, Michał
Published: (2024)

Using Certifying Constraint Solvers for Generating Step-wise Explanations
by: Bleukx, Ignace, et al.
Published: (2025)