A faster implementation of EQ and SE queries for switch-list representations

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F24%3A10493959" target="_blank" >RIV/00216208:11320/24:10493959 - isvavai.cz</a>

Result on the web

<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=haUKl4Exof" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=haUKl4Exof</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10472-023-09915-5" target="_blank" >10.1007/s10472-023-09915-5</a>

Result language

angličtina

Original language name

A faster implementation of EQ and SE queries for switch-list representations

Original language description

A switch-list representation (SLR) of a Boolean function is a compressed truth table representation of a Boolean function in which only (i) the function value of the first row in the truth table and (ii) a list of switches are stored. A switch is a Boolean vector whose function value differs from the value of the preceding Boolean vector in the truth table. The paper Cepek and ChromATIN SMALL LETTER Y WITH ACUTE (JAIR 2020) systematically studies the properties of SLRs and among other results gives polynomial-time algorithms for all standard queries investigated in the Knowledge Compilation Map introduced in Darwiche and Marquis (JAIR 2002). These queries include consistency check, validity check, clausal entailment check, implicant check, equivalence check, sentential entailment check, model counting, and model enumeration. The most difficult query supported in polynomial time by the smallest number of representation languages considered in the Knowledge Compilation Map is the sentential entailment check (of which the equivalence check is a special case). This query can be answered in polynomial time for SLRs, as shown in Cepek and ChromATIN SMALL LETTER Y WITH ACUTE (JAIR 2020). However, the query-answering algorithm is an indirect one: it first compiles both input SLRs into OBDDs (changing the order of variables for one of them if necessary) and then runs the sentential entailment check on the constructed OBDDs (both respecting the same order of variables) using an algorithm from the monograph by Wegener (2000). In this paper we present algorithms that answer both the equivalence and the sentential entailment query directly by manipulating the input SLRs (hence eliminating the compilation step into OBDD), which in both cases improves the time complexity of answering the query by a factor of n for input SLRs on n variables.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Annals of Mathematics and Artificial Intelligence

ISSN

1012-2443

e-ISSN

1573-7470

Volume of the periodical

92

Issue of the periodical within the volume

5

Country of publishing house

NL - THE KINGDOM OF THE NETHERLANDS

Number of pages

16

Pages from-to

1097-1112

UT code for WoS article

001129223400001

EID of the result in the Scopus database

2-s2.0-85179959830