Pre-processing in Boolean Satisfiability Using Bounded (2,k)-Consistency on Regions with Locally Difficult Constraint Setup
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10190142" target="_blank" >RIV/00216208:11320/14:10190142 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1142/S0218213013500292" target="_blank" >http://dx.doi.org/10.1142/S0218213013500292</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1142/S0218213013500292" target="_blank" >10.1142/S0218213013500292</a>
Alternative languages
Result language
angličtina
Original language name
Pre-processing in Boolean Satisfiability Using Bounded (2,k)-Consistency on Regions with Locally Difficult Constraint Setup
Original language description
A new type of partially global consistency derived from 2, -consistency called bounded 2, - consistency (B2C-consistency) is presented in this paper. It is designed for application in propositional satisfiability (SAT) as a building block for a preprocessing tool. Together with the new B2C-consistency a special mechanism for selecting regions of the input SAT instance with difficult constraint setup was also proposed. This mechanism is used to select suitable difficult sub-problems whose simplificationthrough consistency can lead to a significant reduction in the effort needed to solve the instance. A new prototype preprocessing tool preprocessSIGMA which is based on the proposed techniques was implemented. As a proof of new concepts a competitive experimental evaluation on a set of relatively difficult SAT instances was conducted. It showed that our prototype preprocessor is competitive with respect to the existent preprocessing tools LiVer, NiVer, HyPre, blocked clause elimination (
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JD - Use of computers, robotics and its application
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP103%2F10%2F1287" target="_blank" >GAP103/10/1287: PlanEx: Bridging Planning and Execution</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
International Journal on Artificial Intelligence Tools
ISSN
0218-2130
e-ISSN
—
Volume of the periodical
23
Issue of the periodical within the volume
1
Country of publishing house
US - UNITED STATES
Number of pages
29
Pages from-to
1-29
UT code for WoS article
—
EID of the result in the Scopus database
—