Subsumption-driven clause learning with DPLL+restarts
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a concrete algorithm which we claim is faith…
2kA DPLL(T) Framework for Verifying Deep Neural Networks
Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs can have bugs and can be attacked. To address this, research has explored a wi…
Clause Vivification by Unit Propagation in CDCL SAT Solvers
Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effec…
Recursive Decomposition for Nonconvex Optimization
Continuous optimization is an important problem in many areas of AI, including vision, robotics, probabilistic inference, and machine learning. Unfortunately, most real-world optimization problems are nonconvex, causing …
Combinatorial Optimizationgraph partitioningProblem DecompositionProtein FoldingLLMs for Legal Subsumption in German Employment Contracts
Legal work, characterized by its text-heavy and resource-intensive nature, presents unique challenges and opportunities for NLP research. While data-driven approaches have advanced the field, their lack of interpretabili…