Subsumption-driven clause learning with DPLL+restarts
arXiv:1906.07508v1
Originality Synthesis-oriented
AI Analysis
This is an incremental improvement for SAT solving, offering an alternative method with similar performance to existing approaches.
The paper tackles solving SAT instances by using DPLL+restart with clause subsumption, showing it can refute pebbling formulae in polynomial time and linear space, matching CDCL solver effectiveness.
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.