Efficient all-UIP learned clause minimization

DOI10.1007/978-3-030-80223-3_12OpenAlexW3185633566MaRDI QIDQ2118297

Mathias Fleury, Armin Biere

Publication date: 22 March 2022

Full work available at URL: https://resolver.obvsg.at/urn:nbn:at:at-ubl:3-6935

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Uses Software

• MiniSat
• Plingeling
• PrecoSAT
• Treengeling
• GitHub
• Lingeling
• YalSAT
• CaDiCaL
• Paracooba
• Kissat

Cites Work

• Unnamed Item
• Chronological backtracking
• Backing backtracking
• Clause size reduction with all-UIP learning
• Generalized Conflict-Clause Strengthening for Satisfiability Solvers
• Evaluating CDCL Variable Scoring Schemes
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Buckets, Heaps, Lists, and Monotone Priority Queues
• Theory and Applications of Satisfiability Testing

This page was built for publication: Efficient all-UIP learned clause minimization