1,720,998 research outputs found
Verification Of Data-Intensive Embedded Systems
No full textVerification of embedded software relying on black-box hardware is challenging whenever precise specifications of the underlying systems are incomplete or not available. Learning structured hardware models is a powerful enabler of verification in these cases, but it
can be inefficient when the system to be learned is data-intensive rather than control-intensive. We contribute a methodology to attack this problem based on a specific class of automata which are well suited to model systems wherein data paths are known to be decoupled from control paths. We show the effectiveness of our approach by combining learning and verification to assess the correctness of embedded programs relying on FIFO register circuitry to control an elevator system
Ranking and reputation systems in the QBF competition
No full textSystems competitions play a fundamental role in the advancement of the state of the art in several automated reasoning fields. The goal of such events is to answer the question: "Which system should I buy?". In this paper, we consider voting systems as an alternative to other procedures which are well established in automated reasoning contests. Our research is aimed to compare methods that are customary in the context of social choice, with methods that are targeted to artificial settings, including a new hybrid method that we introduce
Backjumping for Quantified Boolean Logic satisfiability
No full textAbstractThe implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of them based on the Davis, Logemann, Loveland procedure (DLL) for propositional satisfiability (SAT). In this paper we show how it is possible to extend the conflict-directed backjumping schema for SAT to the satisfiability of QBFs: When applicable, conflict-directed backjumping allows search to skip over existentially quantified literals while backtracking. We introduce solution-directed backjumping, which allows the same behavior for universally quantified literals. We show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based decision procedure for satisfiability of QBFs. We also implement and test the procedure: The experimental analysis shows that, because of backjumping, significant speed-ups can be obtained.Summing up: We present the first algorithm that applies conflict and solution directed backjumping to QBF, and demonstrate the performance of this algorithm via an empirical study
Learning for Quantified Boolean Logic Satisfiability
No full textLearning, i.e., the ability to record and exploit some informa-
tion which is unveiled during the search, proved to be a very
effective AI technique for problem solving and, in particular,
for constraint satisfaction. We introduce learning as a general
purpose technique to improve the performances of decision
procedures for Quantified Boolean Formulas (QBFs). Since
many of the recently proposed decision procedures for QBFs
solve the formula using search methods, the addition of learn-
ing to such procedures has the potential of reducing useless
explorations of the search space. To show the applicability
of learning for QBF satisfiability we have implemented it in
Q U BE, a state-of-the-art QBF solver. While the backjump-
ing engine embedded in Q U BE provides a good starting point
for our task, the addition of learning required us to devise new
data structures and led to the definition and implementation of
new pruning strategies. We report some experimental results
that witness the effectiveness of learning. Noticeably, Q U BE
augmented with learning is able to solve instances that were
previously out if its reach. To the extent of our knowledge,
this is the first time that learning is proposed, implemented
and tested for QBFs satisfiability
Backjumping for Quantified Boolean Logic Satisfiability
No full textThe implementation of effective reasoning tools for
deciding the satisfiability of Quantified Boolean
Formulas (QBFs) is an important research issue
in Artificial Intelligence. Many decision proce-
dures have been proposed in the last few years,
most of them based on the Davis, Logemann, Love-
land procedure (DLL) for propositional satisfiabil-
ity (SAT). In this paper we show how it is pos-
sible to extend the conflict-directed backjumping
schema for SAT to QBF: when applicable, it al-
lows to jump over existentially quantified literals
while backtracking. We introduce solution-directed
backjumping, which allows the same for univer-
sally quantified literals. Then, we show how it is
possible to incorporate both conflict-directed and
solution-directed backjumping in a DLL-based de-
cision procedure for QBF satisfiability. We also im-
plement and test the procedure: The experimental
analysis shows that, because of backjumping, sig-
nificant speed-ups can be obtained. While there
have been several proposals for backjumping in
SAT, this is the first time –as far as we know– this
idea has been proposed, implemented and experi-
mented for QBFs
Metodo per il supporto alla pianificazione di traiettorie stereotassiche lineari per l'mpianto di dispositivi intracerebrali quali elettrodi multicontatto registranti e/o stimolanti, sonde bioptiche, applicatori di luce laser
No full textMetodo per il supporto alla pianificazione di traiettorie stereotassiche lineari per l’impianto di dispositivi intracerebrali, quali elettrodi multicontatto, sonde bioptiche, applicatori di luce laser o simili comprendente i seguenti passi:
a) realizzazione di un database all’interno del quale database sono presenti informazioni relative alle traiettorie di inserimento di elettrodi di uno o più pazienti,
b) selezione di almeno una struttura bersaglio nell’encefalo del paziente,
c) estrazione delle traiettorie di interesse dal database sulla base dell’individuazione della detta struttura bersaglio,
d)scelta delle traiettorie di interesse che presentano valori all’interno di un intervallo definito da valori soglia di predeterminati parametri
Quantifier structure in search based procedures for QBFs
Full text linkThe best currently available solvers for quantified Boolean
formulas (QBFs) process their input in prenex form, i.e., all the quan-
tifiers have to appear in the prefix of the formula separated from the
purely propositional part representing the matrix. However, in many QBFs
derived from applications, the propositional part is intertwined with the
quantifier structure. To tackle this problem, the standard approach is to
convert such QBFs in prenex form, thereby losing structural information
about the prefix. In the case of search-based solvers, the prenex-form
conversion introduces additional constraints on the branching heuristic
and reduces the benefits of the learning mechanisms. In this paper, we
show that conversion to prenex form is not necessary: current search-based
solvers can be naturally extended in order to handle nonprenex QBFs
and to exploit the original quantifier structure. We highlight the two
mentioned drawbacks of the conversion in prenex form with a simple
example, and we show that our ideas can also be useful for solving QBFs
in prenex form. To validate our claims, we implemented our ideas in the
state-of-the-art search-based solver QUBE and conducted an extensive
experimental analysis. The results show that very substantial speedups can
be obtained
- …
