Towards a Semantics of Unsatisfiability Proofs with Inprocessing

DOI10.29007/7jgqzbMath1403.68244OpenAlexW2741154258MaRDI QIDQ4645727

Tobias Philipp, Adrián Rebola-Pardo

Publication date: 10 January 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.29007/7jgq

zbMATH Keywords

SAT solvingblocked clausesDRAT proofs

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (3)

Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Simulating strong practical proof systems with extended resolution ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem

This page was built for publication: Towards a Semantics of Unsatisfiability Proofs with Inprocessing