DAVIDE BRESOLIN, Department of Computer Science, University of Verona,
Verona, Italy
E-mail: bresolin@sci.univr.it
VALENTIN GORANKO, School of Mathematics, University of the
Witwatersrand, Johannesburg, South Africa
E-mail: goranko@maths.wits.ac.za
ANGELO MONTANARI and PIETRO SALA, Department of Mathematics and
Computer Science, University of Udine, Udine, Italy
E-mail: angelo.montanari@dimi.uniud.it; pietro.sala@dimi.uniud.it
Abstract
In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.
1 Introduction
Interval-based temporal logics provide a natural framework for temporal representation and
reasoning. Unfortunately, in the interval temporal logic setting undecidability is the rule (see, for
instance [16, 17]). The quest for decidable fragments and systems of temporal logics with intervalbased
semantics is one of the main research problems in the area of interval logics. Several
decidability results have been established previously by reduction to point-based logics, either
by selection of an appropriate subset of temporal operators or by restriction of the semantics,
e.g. imposing locality, homogeneity or other principles that essentially reduce it to point-based
semantics [1–3, 12–14, 18, 22]. Only recently some decidability results for genuinely interval-based
logics have been established [4–10].
(...)
In this article, we develop a sound, complete and terminating tableau system for D(symbol) .
(...)
The decision problem for D(symbol) is in PSPACE.
(...)
5 Implementation
In this section we briefly describe an implementation of the proposed tableau methods in Lotrec,
a generic theorem prover for modal and description logics [11, 15].
(...)
5.1 A short overview of Lotrec
Lotrec is a generic prover that can be used for most modal logics studied in the literature. It can be
used to prove validity and satisfiability of formulas. Whenever a formula is satisfiable, it returns a
model for it; whenever a formula is not valid, it returns a counter model for it. In Lotrec, a tableau is
a special kind of labelled graph that is built, and possibly revised, according to a set of user-specified
rules. Every node of the graph is labelled with a set of formulae and can be enriched by auxiliary
markings, if needed.
(...)
6 Conclusions
In this article, we investigated the decidability problem for logics of subinterval structures over
dense linear orderings. First, we systematically studied the logic D· of the strict subinterval relation.
We provided an alternative proof of its decidability by a non-standard small-model theorem and
we developed an optimal tableau-based decision procedure for it. Then, we showed how to refine
structures and techniques for D· to cope with the logic D of the proper subinterval relation. We
proved that it is decidable as well, and we devise an optimal tableau-based decision procedure for
it. Finally, we implemented both tableau methods in Lotrec, a generic theorem prover for modal and
description logics.
http://logcom.oxfordjournals.org/cgi/reprint/exn063
sexta-feira, 13 de fevereiro de 2009
quarta-feira, 11 de fevereiro de 2009
Parallel SAT Solving in Bounded Model Checking
ERIKA ÁBRAHÁM
TOBIAS SCHUBERT and BERND BECKER
MARTIN FRÄNZLE and CHRISTIAN HERDE
Abstract
Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths.We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting.We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.
Keywords: Parallel programs, bounded model checking, SAT solving, linear programming, hybrid systems.
Journal of Logic and Computation
http://logcom.oxfordjournals.org/cgi/reprint/exp002v1.pdf
(...)
For discrete systems a SAT solver is used, while the analysis of linear hybrid automata, for example, requires the application of a combined SAT-LP solver. Some popular solvers are, e.g. zChaff [21], BerkMin [14], MiniSAT [12],
HySat [13], MathSAT [4], CVCLite [5] and ICS [9].
(...)
2 Bounded model checking
We first give a short review of BMC [7, 15] and briefly describe how state-of-the-art SAT solvers
check satisfiability of propositional formulae. In this article we restrict ourselves to safety properties;
for lifeness properties see e.g. [7].
(...)
2.2 Satisfiability checking
The formulae ϕk describing counterexamples of length k are checked for satisfiability by a traditional
SAT solver.
First, the Boolean formula is transformed into a conjunctive normal form (CNF). In order to
keep the formula as small as possible, auxiliary Boolean variables are used to build the CNF
[26]. A formula in CNF form is a conjunction of clauses, while each clause is the disjunction of
literals.We distinguish between positive literals being Boolean variables, and negative literals being
negated ones.
In order to satisfy the formula, each of the clauses must be satisfied, i.e. at least one literal in each
clause must be true. The SAT solver assigns values to the variables in an iterative manner. After each
decision, i.e. free choice of an assignment, the solver propagates the assignment by searching for
unit clauses, i.e. clauses in that all literals but one are already false; the remaining literal is implied
to be true, since otherwise the clause would not be satisfied.
If two unit clauses imply different values for the same variable, a conflict occurs. In this case
a conflict analysis can take place which results in non-chronological backtracking and conflict
learning [20, 28]. Intuitively, the solver applies resolution to some unit clauses, using the implication
tree, and inserts a new conflict clause thereby strengthening the problem constraints and restricting
the state space for further search.
(...)
3 Parallel BMC
(...)
4 Experimental results
We implemented a prototype SAT solver that works mainly as described in Section 2.2. For
communication we use MPICH2 [16], an implementation of the message passing interface (MPI)
standard.
(...)
5 Conclusions
In this article we introduced a parallel SAT-solving technique for BMC.The parallelization is different
from existing approaches: instead of solving a single problem instance using parallel solvers, we let
different solvers solve different BMC instances. In order to speed up the search, we apply CSR and
let the solvers communicate the conflict clauses found during their SAT-checks. The experiments
performed show that the positive effect of CSR can only be preserved under parallelization if the
solvers communicate the conflict clauses among themselves.With communication, the full advantage
of sequential CSR can be maintained in the concurrent setting, yielding nearly linear speedup from
parallelization.
(...)
[26] G. Tseitin. On the complexity of derivations in propositional calculus. In Studies in Constructive
Mathematics and Mathematical Logics, Slisenko ed., pp. 115–125. Springer, Berlin, 1970.
(...)
TOBIAS SCHUBERT and BERND BECKER
MARTIN FRÄNZLE and CHRISTIAN HERDE
Abstract
Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths.We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting.We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.
Keywords: Parallel programs, bounded model checking, SAT solving, linear programming, hybrid systems.
Journal of Logic and Computation
http://logcom.oxfordjournals.org/cgi/reprint/exp002v1.pdf
(...)
For discrete systems a SAT solver is used, while the analysis of linear hybrid automata, for example, requires the application of a combined SAT-LP solver. Some popular solvers are, e.g. zChaff [21], BerkMin [14], MiniSAT [12],
HySat [13], MathSAT [4], CVCLite [5] and ICS [9].
(...)
2 Bounded model checking
We first give a short review of BMC [7, 15] and briefly describe how state-of-the-art SAT solvers
check satisfiability of propositional formulae. In this article we restrict ourselves to safety properties;
for lifeness properties see e.g. [7].
(...)
2.2 Satisfiability checking
The formulae ϕk describing counterexamples of length k are checked for satisfiability by a traditional
SAT solver.
First, the Boolean formula is transformed into a conjunctive normal form (CNF). In order to
keep the formula as small as possible, auxiliary Boolean variables are used to build the CNF
[26]. A formula in CNF form is a conjunction of clauses, while each clause is the disjunction of
literals.We distinguish between positive literals being Boolean variables, and negative literals being
negated ones.
In order to satisfy the formula, each of the clauses must be satisfied, i.e. at least one literal in each
clause must be true. The SAT solver assigns values to the variables in an iterative manner. After each
decision, i.e. free choice of an assignment, the solver propagates the assignment by searching for
unit clauses, i.e. clauses in that all literals but one are already false; the remaining literal is implied
to be true, since otherwise the clause would not be satisfied.
If two unit clauses imply different values for the same variable, a conflict occurs. In this case
a conflict analysis can take place which results in non-chronological backtracking and conflict
learning [20, 28]. Intuitively, the solver applies resolution to some unit clauses, using the implication
tree, and inserts a new conflict clause thereby strengthening the problem constraints and restricting
the state space for further search.
(...)
3 Parallel BMC
(...)
4 Experimental results
We implemented a prototype SAT solver that works mainly as described in Section 2.2. For
communication we use MPICH2 [16], an implementation of the message passing interface (MPI)
standard.
(...)
5 Conclusions
In this article we introduced a parallel SAT-solving technique for BMC.The parallelization is different
from existing approaches: instead of solving a single problem instance using parallel solvers, we let
different solvers solve different BMC instances. In order to speed up the search, we apply CSR and
let the solvers communicate the conflict clauses found during their SAT-checks. The experiments
performed show that the positive effect of CSR can only be preserved under parallelization if the
solvers communicate the conflict clauses among themselves.With communication, the full advantage
of sequential CSR can be maintained in the concurrent setting, yielding nearly linear speedup from
parallelization.
(...)
[26] G. Tseitin. On the complexity of derivations in propositional calculus. In Studies in Constructive
Mathematics and Mathematical Logics, Slisenko ed., pp. 115–125. Springer, Berlin, 1970.
(...)
Assinar:
Comentários (Atom)