<?xml version="1.0" encoding="utf-8"?>
<export-example>
  <doc>
    <id>872</id>
    <completedYear/>
    <publishedYear/>
    <thesisYearAccepted/>
    <language>eng</language>
    <pageFirst/>
    <pageLast/>
    <pageNumber/>
    <edition/>
    <issue/>
    <volume/>
    <type>reportzib</type>
    <publisherName/>
    <publisherPlace/>
    <creatingCorporation/>
    <contributingCorporation/>
    <belongsToBibliography>0</belongsToBibliography>
    <completedDate>2005-08-03</completedDate>
    <publishedDate>2005-08-03</publishedDate>
    <thesisDateAccepted>--</thesisDateAccepted>
    <title language="eng">Foundations of Hierarchical SAT-Solving</title>
    <abstract language="eng">The theory of hierarchical Boolean satisfiability (SAT) solving proposed in this paper is based on a strict axiomatic system and introduces a new important notion of implicativity. The theory makes evident that increasing implicativity is the core of SAT-solving. We provide a theoretical basis for increasing the implicativity of a given SAT instance and for organizing SAT-solving in a hierarchical way. The theory opens a new domain of research: SAT-model construction. Now quite different mathematical models can be used within practical SAT-solvers. The theory covers many advanced techniques such as circuit-oriented SAT-solving, mixed BDD/CNF SAT-solving, merging gates, using pseudo-Boolean constraints, using state machines for representation of Boolean functions, arithmetic reasoning, and managing don t cares. We believe that hierarchical SAT-solving is a cardinal direction of research in practical SAT-solving.</abstract>
    <identifier type="serial">05-38</identifier>
    <identifier type="opus3-id">872</identifier>
    <identifier type="urn">urn:nbn:de:0297-zib-8728</identifier>
    <author>Yakov Novikov</author>
    <author>Raik Brinkmann</author>
    <series>
      <title>ZIB-Report</title>
      <number>05-38</number>
    </series>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>SAT</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>implicativity</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>verification</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>Boolean vector function</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>satisfiability</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>Bounded-Model-Checking</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>BMC</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>model</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>block</value>
    </subject>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>hierarchy</value>
    </subject>
    <collection role="ddc" number="000">Informatik, Informationswissenschaft, allgemeine Werke</collection>
    <collection role="msc" number="06E30">Boolean functions [See also 94C10]</collection>
    <collection role="msc" number="94C10">Switching theory, application of Boolean algebra; Boolean functions [See also 06E30]</collection>
    <collection role="institutes" number="">ZIB Allgemein</collection>
    <file>https://opus4.kobv.de/opus4-zib/files/872/ZR-05-38.pdf</file>
  </doc>
</export-example>
