Blocked clause decomposition

DOI10.1007/978-3-642-45221-5_29MaRDI QIDQ2870145zbMATH OpenOpenAlexFDO

Authors Marijn J. H. Heule, Armin Biere

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-45221-5_29

Mathematics Subject Classification ID

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

Recommendations

• Everything you always wanted to know about blocked sets (but were afraid to ask)
• Super-blocked clauses
• Blocked clause elimination
• Local redundancy in SAT: generalizations of blocked clauses
• Decomposing SAT Instances with Pseudo Backbones

Cited in

(9)

• Set-blocked clause and extended set-blocked clause in first-order logic
• Super-blocked clauses
• Everything you always wanted to know about blocked sets (but were afraid to ask)
• SAT race 2015
• Recognition of Nested Gates in CNF Formulas
• Local redundancy in SAT: generalizations of blocked clauses
• Mining definitions in Kissat with Kittens
• Clausal congruence closure
• Sometimes hoarding is harder than cleaning: NP-hardness of maximum blocked-clause addition

Describes a project that uses

Uses Software

• MiniSat
• Plingeling
• Lingeling

This page was built for publication: Blocked clause decomposition

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