Metalevel Algorithms for Variant Satisfiability

被引：5

作者：

Skeirik, Stephen ^{[1
]}

Meseguer, Jose ^{[1
]}

机构：

[1] Univ Illinois, Dept Comp Sci, Champaign, IL 61801 USA

来源：

REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2016 | 2016年 / 9942卷

关键词：

Finite variant property (FVP); Folding variant narrowing; Satisfiability in initial algebras; Metalevel algorithms; Reflection; Maude; ORDER-SORTED ALGEBRA; MODULO; SPECIFICATIONS; AXIOMS; TOOL;

D O I：

10.1007/978-3-319-44802-2_10

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TS/E when the theory (Sigma, E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation in Maude 2.7 of variant satisfiability using these sub-algorithms.

引用

页码：167 / 184

页数：18

共 50 条

[41] Mixed parallel execution of algorithms for satisfiability problem
Zhang, KR
Nagamatu, M
INTELLIGENT INFORMATION PROCESSING II, 2005, 163 : 273 - 277
[42] Random backtracking in backtrack search algorithms for satisfiability
Lynce, I.
Marques-Silva, J.
DISCRETE APPLIED MATHEMATICS, 2007, 155 (12) : 1604 - 1612
[43] GREEDY ALGORITHMS FOR THE MAXIMUM SATISFIABILITY PROBLEM: SIMPLE ALGORITHMS AND INAPPROXIMABILITY BOUNDS
Poloczek, Matthias
Schnitger, Georg
Williamson, David P.
Van Zuylen, Anke
SIAM JOURNAL ON COMPUTING, 2017, 46 (03) : 1029 - 1061
[44] Satisfiability models and algorithms for circuit delay computation
Silva, LGE
Marques-Silva, J
Silveira, LM
Sakallah, KA
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2002, 7 (01) : 137 - 158
[45] Algorithms for four variants of the exact satisfiability problem
Dahllöf, V
Jonsson, P
Beigel, R
THEORETICAL COMPUTER SCIENCE, 2004, 320 (2-3) : 373 - 394
[46] Metalevel relationship cardinalities
Henderson-Sellers, B.
Graham, I.M.
JOOP - Journal of Object-Oriented Programming, 1999, 12 (01): : 51 - 58
[47] A comparative runtime analysis of heuristic algorithms for satisfiability problems
Zhou, Yuren
He, Jun
Nie, Qing
ARTIFICIAL INTELLIGENCE, 2009, 173 (02) : 240 - 257
[48] Using problem symmetry in search based satisfiability algorithms
Goldberg, EI
Prasad, MR
Brayton, RK
DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS, 2002, : 134 - 141
[49] Typical case complexity of Satisfiability Algorithms and the threshold phenomenon
Franco, J
DISCRETE APPLIED MATHEMATICS, 2005, 153 (1-3) : 89 - 123
[50] Exact Algorithms for Exact Satisfiability and Number of Perfect Matchings
Andreas Björklund
Thore Husfeldt
Algorithmica, 2008, 52 : 226 - 249

← 1 2 3 4 5 →