Short proofs for some symmetric quantified Boolean formulas

DOI10.1016/J.IPL.2018.07.009MaRDI QIDQ1799597zbMATH OpenOpenAlexWikidataFDO

Authors M. Kauers, Martina Seidl

Publication date 19 October 2018

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.01437

zbMATH Keywords

QBFproof complexityautomatic theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Abstract: We exploit symmetries to give short proofs for two prominent formula families of QBF proof complexity. On the one hand, we employ symmetry breakers. On the other hand, we enrich the (relatively weak) QBF resolution calculus Q-Res with the symmetry rule and obtain separations to powerful QBF calculi.

Recommendations

• Symmetries of quantified Boolean formulas
• Proof complexity of QBF symmetry recomputation
• Proof complexity of resolution-based QBF calculi
• Short proofs in QBF expansion
• Shortening QBF proofs with dependency schemes

Cites work

• scientific article; zbMATH DE number 702472 (Why is no real title available?)
• Proof complexity of resolution-based QBF calculi
• QBF Resolution Systems and Their Proof Complexities
• Resolution for quantified Boolean formulas
• Short proofs for tricky formulas
• Size, cost and capacity: a semantic technique for hard random QBFs
• Symmetries of quantified Boolean formulas
• The symmetry rule in propositional logic

Cited in

(6)

• Proof complexity of QBF symmetry recomputation
• Symmetries of quantified Boolean formulas
• A simple proof of QBF hardness
• Short proofs in QBF expansion
• QBFFam: a tool for generating QBF families from proof complexity
• Never trust your solver: certification for SAT and QBF

This page was built for publication: Short proofs for some symmetric quantified Boolean formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799597)