On the complexity of choosing the branching literal in DPLL

DOI10.1016/S0004-3702(99)00097-1MaRDI QIDQ1978252zbMATH OpenOpenAlexFDO

Authors Paolo Liberatore

Publication date 4 June 2000

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0004-3702(99)00097-1

zbMATH Keywords

complexitypropositional satisfiabilityDavis-Putnam

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Recommendations

• Complexity results on DPLL and resolution
• How good are branching rules in DPLL?
• Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas
• Learning to select branching rules in the DPLL procedure for satisfiability
• Advances in Artificial Intelligence

Cites work

• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• scientific article; zbMATH DE number 956858 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Branching rules for satisfiability
• How good are branching rules in DPLL?
• Solving propositional satisfiability problems

Cited in

(11)

• Scaling up DPLL(T) string solvers using context-dependent simplification
• Learning to select branching rules in the DPLL procedure for satisfiability
• On the limit of branching rules for hard random unsatisfiable 3-SAT
• Argumentation in artificial intelligence
• Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
• On the relation among answer set solvers
• How important are branching decisions: fooling MIP solvers
• How good are branching rules in DPLL?
• New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability
• Complexity results on DPLL and resolution
• Advances in Artificial Intelligence

This page was built for publication: On the complexity of choosing the branching literal in DPLL

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