Cost-effective hyper-resolution for preprocessing CNF formulas

DOI10.1007/11499107_34MaRDI QIDQ5713736zbMATH OpenOpenAlexFDO

Authors Roman Gershman, Ofer Strichman

Publication date 15 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b137280

Mathematics Subject Classification ID

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

Recommendations

• Theory and Applications of Satisfiability Testing
• Effective preprocessing in SAT through variable and clause elimination
• Partitioning methods for satisfiability testing on large formulas
• Preprocessing in incremental SAT
• A Preprocessor for Max-SAT Solvers

Cited in

(8)

• Visualizing SAT instances and runs of the DPLL algorithm
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Efficient CNF simplification based on binary implication graphs
• Preprocessing for DQBF
• Simulating circuit-level simplifications on CNF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Theory and Applications of Satisfiability Testing
• Clausal congruence closure

Describes a project that uses

Uses Software

• Chaff
• Siege
• BerkMin

This page was built for publication: Cost-effective hyper-resolution for preprocessing CNF formulas

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