Classes of Boolean Formulae with Effectively Solvable SAT

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F10%3A10051502" target="_blank" >RIV/00216208:11320/10:10051502 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Classes of Boolean Formulae with Effectively Solvable SAT

Original language description

We present an overview of known classes of Boolean formulae for which polynomial time algorithms for satisfiability testing (SAT) are known. We will summarize basic properties of these classes and their mutual relations with respect to inclusion. One ofthese classes on which we focus our attention in particular is the class of Single Lookahead Unit Resolution formulae (SLUR). We will define a hierarchy of classes which constitutes a generalization of the SLUR class, and prove its properties.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

—

Continuities

S - Specificky vyzkum na vysokych skolach

Publication year

2010

Confidentiality

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

Article name in the collection

WDS 2010 - Proceedings of Contributed Papers

ISBN

978-80-7378-139-2

ISSN

—

e-ISSN

—

Number of pages

6

Pages from-to

—

Publisher name

MATFYZPRESS

Place of publication

Praha

Event location

Praha

Event date

Jun 1, 2010

Type of event by nationality

EUR - Evropská akce

UT code for WoS article

—