检索结果-内蒙古大学图书馆

Computerized Adaptive Testing to Balance Exposure Bias and Measurement Accuracy Using Zero-Suppressed binary decision diagrams

引用

IEEE ACCESS 2025年 13卷 33883-33903页

作者： Ueno, Maomi Fuchimoto, Kazuma Kishida, Wakaba Miyazawa, Yoshimitsu Univ Electrocommun Grad Sch Informat & Engn Tokyo 1828585 Japan Natl Ctr Univ Entrance Examinat Res & Dev Tokyo 1530041 Japan

Computerized adaptive testing (CAT) presents a tradeoff dilemma involving item exposure bias and measurement accuracy. To resolve this dilemma, we propose a new two-step CAT mechanism to balance exposure bias and measurement accuracy. Using zero-suppressed binary decision diagram (ZDD), the proposed method first selects and presents an optimal item from an equivalent item pool, which uniformly divides the whole item pool. The first step rapidly provides a roughly approximated ability estimate of an examinee. The second step produces a more accurate ability estimate of the examinee. Specifically, the second step selects an optimal item from the whole item pool and presents an item with a difficulty parameter value that is approximately equal to the examinee ability estimate. Numerical experiment results underscore the effectiveness of the proposed method.

关键词： Accuracy Testing Probabilistic logic IP networks History binary decision diagrams Standards Upper bound Gaussian distribution Current measurement Computerized adaptive testing item response theory parallel test assembly zero-suppressed binary decision diagrams

来源：评论

学校读者我要写书评

暂无评论

Optimizing binary decision diagrams for Interpretable Machine Learning Classification

引用

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS 2024年第10期43卷 3083-3087页

作者： Cabodi, Gianpiero Camurati, Paolo E. Marques-Silva, Joao Palena, Marco Pasini, Paolo Politecn Torino DAUIN I-10129 Turin Italy Univ Toulouse ANITI F-31013 Toulouse France

Machine learning (ML) is ever more frequently used as a tool to aid decision making. The need to understand the decisions made by ML algorithms has sparked a renewed interest in explainable ML models. A number of known models are often regarded as interpretable by human decision makers with varying degrees of difficulty. The size of such models plays a crucial role in determining how easily they can be understood by a human. In this article we propose the use of binary decision diagrams (BDDs) as an interpretable ML model. BDDs can be deemed as interpretable as decision trees (DTs) while offering a often more compact representation due to node sharing. Fixed variable ordering also allows for more concise explanations. We propose a SAT-based approach for learning optimal BDDs that exhibit perfect accuracy on training data. We also explore heuristic methods for computing suboptimal BDDs, in order to improve scalability. We also investigate procedures to transform instances of known ML models into BDDs in order to provide more concise explanations.

关键词： Boolean functions Training Training data decision trees Channel coding Scalability Integrated circuits binary decision diagrams boolean functions classification algorithms machine learning

来源：评论

学校读者我要写书评

暂无评论

A Recursive Framework for Evaluating Moments Using Zero-Suppressed binary decision diagrams

引用

IEEE ACCESS 2024年 12卷 91886-91895页

作者： Godwin Lim, Brian Tan, Renzo Roel Kawahara, Jun Minato, Shin-Ichi Ikeda, Kazushi Nara Inst Sci & Technol Div Informat Sci Nara 6300192 Japan Kyoto Univ Grad Sch Informat Kyoto 6068501 Japan Ateneo Manila Univ John Gokongwei Sch Management Manila 1108 Philippines

The zero-suppressed binary decision diagram (ZDD) is a compact data structure widely used for the efficient representation of families of sparse subsets. Its inherent recursive structure also facilitates easy diagram manipulation and family operations. Practical applications generally fall under discrete optimization, such as combinatorial problems and graph theory. Given its utility, summarizing the subsets represented in the diagram using key metrics is of great value as this provides valuable insights into the characteristics of the family. The paper proposes a recursive algorithm to extract information on moments from families represented as a ZDD. Given a value for every element in the universe, the value of a subset is first formulated as the sum of the values of its elements. The moments of a family are then calculated as the mean of the exponentiated subset values, akin to the method of moments. Leveraging the structure of the ZDD, the proposed algorithm recursively traverses a given diagram for efficient moments evaluation via multinomial expansion. Its utility is then demonstrated with three classical problems-power sets, the knapsack problem, and paths in graphs-offering orders of magnitude increase in computational efficiency relative to conventional method. Overall, the proposed algorithm enhances the functionality of the ZDD by introducing an efficient family operation to uncover the distribution of subset values in a represented family.

关键词： binary decision diagrams Method of moments Finite element analysis Time complexity Programming Memory management Optimization methods Discrete optimization family operation method of moments zero-suppressed binary decision diagram

来源：评论

学校读者我要写书评

暂无评论

Correct and Verify-CAV: Exploiting binary decision diagrams to Enable Formal Verification of Approximate Adders With Correct Carry Bits

引用

IEEE TRANSACTIONS ON CIRCUITS AND SYSTEMS I-REGULAR PAPERS 2025年第4期72卷 1718-1730页

作者： Jha, Chandan Kumar Qayyum, Khushboo Hassan, Muhammad Drechsler, Rolf Univ Bremen Inst Comp Sci D-28359 Bremen Germany German Res Ctr Artificial Intelligence DFKI D-28359 Bremen Germany

Approximate adders have received significant attention as they give benefits in power, performance, and area for error-resilient applications. Due to their ubiquitous use, formal verification of approximate adders has also gained traction. However, prior works on formal verification of approximate adders are limited to relaxed equivalence checking, i.e., checking whether the approximate adder designs have an error less than a specified threshold. This method has limitations, as multiple approximate adder designs can satisfy the relaxed equivalence checking criterion, which can cause more than expected deterioration in the output quality. The deterioration in output quality is larger in approximate adder designs that produce exact results for some regions of the input space but have the freedom to produce approximate results in other regions of the input space. In this paper, we propose a methodology called Correct and Verify (CAV), which exploits binary decision diagrams (BDDs) to guarantee that the approximate adder with correct carry bits exactly matches its functional specification. Our idea takes advantage of the BDD structure in extracting the internal signals, particularly the carry signal from the golden reference exact adder. Afterward, a corrector circuit is generated from the functional specification and the extracted carry signal is used as input in the corrector circuit. The corrector circuit is used to generate the corrected adder from the approximate adder. The generated corrected adder can be compared against a formally verified golden reference exact adder. We show the efficacy of CAV over approximate Ripple Carry Adders (RCA) as well as approximate Parallel Prefix Adders (PPA). Lastly, we perform a qualitative analysis by introducing mutations in the designs to show the fault detection quality of the CAV methodology.

关键词： Adders Circuits Boolean functions Formal verification binary decision diagrams Integrated circuit modeling Program processors Measurement Logic gates Inverters combinational equivalence checking binary decision diagrams and-inverter graphs approximate adders

来源：评论

学校读者我要写书评

暂无评论

binary decision diagrams on Modern Hardware 23

Binary Decision Diagrams on Modern Hardware

引用

23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023

作者： Pastva, Samuel Henzinger, Thomas Institute of Science and Technology Austria Klosterneuburg3400 Austria

ISBN: (纸本)9783854480600

binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores. © 2023 FMCAD Association and individual authors.

关键词： binary decision diagrams

来源：评论

学校读者我要写书评

暂无评论

Formal Verification of Integer Multiplier Circuits Using binary decision diagrams

引用

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS 2023年第4期42卷 1365-1378页

作者： Kumar, Jitendra Miyasaka, Yukio Srivastava, Asutosh Fujita, Masahiro Jawaharlal Nehru Univ Dept Comp & Syst Sci New Delhi 110067 India Univ Calif Berkeley Dept Elect Engn & Comp Sci Berkeley CA 94720 USA Univ Tokyo VLSI Design & Educ Ctr Tokyo 1130032 Japan

Multiplier circuit covers a more extensive area of embedded system application in digital signal processing, cryptography, and multimedia. Nonstandard implementations and custom optimization are being done to reduce the size of multipliers. The circuit became prone to a buggy, and hence the demand for verification increased. Formal verification methods, such as satisfiability (SAT), symbolic computer algebra (SCA), and binary decision diagrams (BDDs) have made massive progress over the last few decades. However, these methods are insufficient to verify the optimized multipliers. SAT-based equivalence checking is computationally expensive. SCA-based backward rewriting is limited to algebraic-friendly multipliers. The complexity of BDDs is exponential with the input size. Although, by allowing an additional variable method, the size of the BDD is limited to 4th degree polynomial of the number of the inputs, this method is not explored to verify optimized multipliers. This article focus on verifying integer multipliers with diverse architectures. We propose an algorithm for the direct construction of BDDs without traversing circuits and generate BDDs up to 1024 bits. We utilize the additional variable method and constructing BDDs using high-to-low variable ordering. We reduce the complexity of BDD size to a 3rd degree polynomial. We generate BDDs and verify the multipliers with various architectures up to 64 bits. We propose a method to verify optimized multipliers by checking equivalence and verifying up to 32-bits optimized multipliers. We do the error tolerance analysis of our approach by inserting bugs in a circuit at various locations.

关键词： Formal verification Computer bugs Optimization binary decision diagrams Adders Signal processing algorithms Tolerance analysis Adder trees algebraic backward rewriting binary decision diagrams (BDDs) error tolerance analysis multiplier verification

来源：评论

学校读者我要写书评

暂无评论

On Aligning Non-Order-Associated binary decision diagrams

引用

INFORMS JOURNAL ON COMPUTING 2023年第5期35卷 910-928页

作者： Bochkarev, Alexey A. Smith, J. Cole Rheinland Pfalz Tech Univ Kaiserslautern Landau Dept Math D-67663 Kaiserslautern Germany Syracuse Univ Dept Elect Engn & Comp Sci Syracuse NY 13244 USA

Recent studies employ collections of binary decision diagrams (BDDs) to solve combinatorial optimization problems. This paper focuses on the problem of optimally aligning two BDDs, that is, transforming them to enforce a common order of variables while keeping the total size of the diagrams as small as possible. We address this problem, which is known to be NP-hard, by introducing and studying a simplified problem instead of working with the more complex original diagrams. We discuss some basic properties of the simplified problem, design a corresponding heuristic for the original problem, and show empirically that this approach yields good quality alignments while significantly reducing the complexity of intermediate diagram transformations. We highlight the practicality of this approach in the context of a variation of the uncapacitated facility location problem.

关键词： analysis of algorithms data structures binary decision diagrams combinatorial optimization problems

来源：评论

学校读者我要写书评

暂无评论

Comprehensive and Instantly Responsive Player Assistance using binary decision diagrams 19

Comprehensive and Instantly Responsive Player Assistance usi...

引用

19th International Conference on the Foundations of Digital Games (FDG)

作者： Mawhorter, Ross Smith, Adam Univ Calif Santa Cruz Santa Cruz CA 95064 USA

ISBN: (纸本)9798400709555

In large game worlds, players can get lost and feel overwhelmed as they try to figure out which immediate choices will make progress towards their own long-range goals in the game. This is a planning problem, but these games often have large state spaces. In this paper, we show that binary decision diagrams (BDDs) can directly manipulate very large game state spaces, and this power can be leveraged to construct instantly responsive player assistance systems. We use BDDs to build a compressed representation of a game's state-transition function, and use it to derive an action policy that makes shortest-path recommendations for any feasible state towards any achievable goal in milliseconds. We introduce the intuition behind planning with BDDs using a tiny grid world, and eventually scale to an integrated system for start-to-finish gameplay assistance in Super Metroid.

关键词： binary decision diagrams Graph Search Player Assistance

来源：评论

学校读者我要写书评

暂无评论

PfComp: A Verified Compiler for Packet Filtering Leveraging binary decision diagrams 2024

PfComp: A Verified Compiler for Packet Filtering Leveraging ...

引用

13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)

作者： Chavanon, Clement Besson, Frederic Ninet, Tristan Univ Rennes INRIA Rennes France Thales Grp Gennevilliers France

ISBN: (纸本)9798400704888

We present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a Clight program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code out-performs a sequential evaluation of the policy rules.

关键词： packet filtering verified compilation binary decision diagrams

来源：评论

学校读者我要写书评

暂无评论

Towards Deterministic Compilation of binary decision diagrams From Feature Models 24

Towards Deterministic Compilation of Binary Decision Diagram...

引用

28th International Systems and Software Product Line Conference (SPLC)

作者： Hess, Tobias Semmler, Sean Niklas Sundermann, Chico Toran, Jacobo Thuem, Thomas Univ Ulm Ulm Germany Paderborn Univ Paderborn Germany

ISBN: (纸本)9798400705939

Compiling binary decision diagrams (BDD) from feature models is a challenging task whose outcome and performance depends on many interconnected factors. As almost all of these factors trace back to the BDD's variable order, finding suitable orders is paramount for compilation success. In addition to cross-tree constraints, Alternative groups in feature models pose a challenge for variable ordering as separating group variables in the order can lead to duplication of large parts of the BDD. Previous approaches only scale to under-constrained models and require knowledge of the feature hierarchy. We address both shortcomings with a novel deterministic variable-ordering heuristic that detects Alternative groups in Boolean formulas and exploits them for variable ordering using the well-known FORCE heuristic in a divide-and-conquer approach. Our evaluation shows that this heuristic, together with our compilation strategy, scales to many models for which BDDs could not be compiled previously. Thereby, this work resolves SPLC's knowledge compilation challenge for an important subset of real-world models.

关键词： binary decision diagrams Variable Ordering Feature-Model Analysis

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：