Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Practical Aspects of Automated Reasoning
Article type: Research Article
Authors: Asín Achá, Roberto; | Nieuwenhuis, Robert | Oliveras, Albert | Rodríguez-Carbonell, Enric
Affiliations: Technical University of Catalonia, Barcelona, Spain | www.lsi.upc.edu/~rasin | www.lsi.upc.edu/~roberto | www.lsi.upc.edu/~oliveras | www.lsi.upc.edu/~erodri
Note: [] Corresponding author. E-mail: rasin@lsi.upc.edu.
Abstract: Since Zhang and Malik's work in 2003 [19], it is well-known that modern DPLL-based SAT solvers with learning can be instrumented to write a trace on disk from which, if the input is unsatisfiable, a resolution proof can be extracted (and checked), and hence also an unsatisfiable core: a (frequently small) unsatisfiable subset of the input clauses. In this article we first give a new algorithmic approach for processing these (frequently huge) traces. It achieves the efficiency of a depth-first traversal, while preserving the property that memory usage remains upper bounded by that of the SAT solver that generated the trace. The second part of this article is about in-memory algorithms for generating SAT proofs and cores, without writing traces to disk. We discuss advantages and disadvantages of this approach and investigate why the current SAT solvers with this feature still run out of memory on long SAT runs. We analyze several of these in-memory algorithms, based on carefully designed experiments with our implementation of each one of them, as well as with (our implementation of) a trace-based one. Then we describe a new in-memory algorithm which saves space by doing more bookkeeping to discard unnecessary information, and show that it can handle significantly more instances than the previously existing algorithms, at a negligible expense in time.
Keywords: SAT, SAT proofs, unsatisfiable cores, DPLL, SAT solvers
DOI: 10.3233/AIC-2010-0462
Journal: AI Communications, vol. 23, no. 2-3, pp. 145-157, 2010
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl