6533b7cffe1ef96bd12584e0
RESEARCH PRODUCT
Subsumption-driven clause learning with DPLL+restarts
Olivier Bailleuxsubject
FOS: Computer and information sciencesComputer Science - Logic in Computer ScienceTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESArtificial Intelligence (cs.AI)Computer Science - Artificial IntelligenceLogic in Computer Science (cs.LO)description
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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2019-06-18 |