caa a22 4500 463182987 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070801xx s 000 0 eng 10.1007/s10817-007-9074-1 doi (NATIONALLICENCE)springer-10.1007/s10817-007-9074-1 Sinz Carsten Institute for Formal Models and Verification, Johannes Kepler University Linz, Altenbergerstr. 69, 4040, Linz, Austria aut Visualizing SAT Instances and Runs of the DPLL Algorithm [Elektronische Daten] [Carsten Sinz] SAT-solvers have turned into essential tools in many areas of applied logic like, for example, hardware verification or satisfiability checking modulo theories. However, although recent implementations are able to solve problems with hundreds of thousands of variables and millions of clauses, much smaller instances remain unsolved. What makes a particular instance hard or easy is at most partially understood - and is often attributed to the instance's internal structure. By converting SAT instances into graphs and applying established graph layout techniques, this internal structure can be visualized and thus serve as the basis of subsequent analysis. Moreover, by providing tools that animate the structure during the run of a SAT algorithm, dynamic changes of the problem instance become observable. Thus, we expect both to gain new insights into the hardness of the SAT problem and to help in teaching SAT algorithms. Springer Science+Business Media B.V., 2007 SAT instance nationallicence DPLL procedure nationallicence Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 219-243 0168-7433 39:2<219 2007 39 10817 https://doi.org/10.1007/s10817-007-9074-1 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-007-9074-1 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Sinz Carsten Institute for Formal Models and Verification, Johannes Kepler University Linz, Altenbergerstr. 69, 4040, Linz, Austria aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 219-243 0168-7433 39:2<219 2007 39 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer