Subsumption-driven clause learning with DPLL+ restarts
O Bailleux - arXiv preprint arXiv:1906.07508, 2019 - arxiv.org
arXiv preprint arXiv:1906.07508, 2019•arxiv.org
We propose to use a DPLL+ restart to solve SAT instances by successive simplifications
based on the production of clauses that subsume the initial clauses. We show that this
approach allows the refutation of pebbling formulae in polynomial time and linear space, as
effectively as with a CDCL solver.
based on the production of clauses that subsume the initial clauses. We show that this
approach allows the refutation of pebbling formulae in polynomial time and linear space, as
effectively as with a CDCL solver.
We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approach allows the refutation of pebbling formulae in polynomial time and linear space, as effectively as with a CDCL solver.
arxiv.org