The paper is concerned with the relevant practical problem of selectinga small unsatisfiable subset of clauses inside an unsatisfiable CNF formula. Moreover, it deals with the algorithmic problem of improvingan enumerative (DPLL-style) approach to SAT, in order to overcome some structural defects of such an approach. Within a complete solution framework, we are able to evaluate the difficulty of each clause by analyzing the history of the search. Such clause hardness evaluation is used in order to rapidly select an unsatisfiable subformula (of the given CNF) which is a good approximation of a minimal unsatisfiable subformula (MUS). Unsatisfiability is proved by solving only such subformula. Very small unsatisfiable subformulae are detected inside famous Dimacs unsatisfiable problems and in real-world problems. Comparison with the very efficient solver SATO 3.2 used as a state-of-the-art DPLL procedure (disabling learning of new clauses) shows the effectiveness of such enumeration guide.
Approximating minimal unsatisfiable subformulae by means of adaptive core search / Bruni, Renato. - In: DISCRETE APPLIED MATHEMATICS. - ISSN 0166-218X. - STAMPA. - 130:2(2003), pp. 85-100. (Intervento presentato al convegno CMMSE 2002 tenutosi a Alicante nel 20 September 2002 through 25 September 2002) [10.1016/s0166-218x(02)00399-2].
Approximating minimal unsatisfiable subformulae by means of adaptive core search
BRUNI, Renato
2003
Abstract
The paper is concerned with the relevant practical problem of selectinga small unsatisfiable subset of clauses inside an unsatisfiable CNF formula. Moreover, it deals with the algorithmic problem of improvingan enumerative (DPLL-style) approach to SAT, in order to overcome some structural defects of such an approach. Within a complete solution framework, we are able to evaluate the difficulty of each clause by analyzing the history of the search. Such clause hardness evaluation is used in order to rapidly select an unsatisfiable subformula (of the given CNF) which is a good approximation of a minimal unsatisfiable subformula (MUS). Unsatisfiability is proved by solving only such subformula. Very small unsatisfiable subformulae are detected inside famous Dimacs unsatisfiable problems and in real-world problems. Comparison with the very efficient solver SATO 3.2 used as a state-of-the-art DPLL procedure (disabling learning of new clauses) shows the effectiveness of such enumeration guide.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
