专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

21. 发明申请

US20120271813A1 MULTI-LAYER SEARCH-ENGINE INDEX 有权
标题翻译：多层次搜索引擎索引
公开(公告)号：US20120271813A1
公开(公告)日：2012-10-25
申请号：US13428709
申请日：2012-03-23
申请人： HUI SHEN , Mao Yang , Lintao Zhang , Zhenyu Zhao , Xiao Wu , Ying Yan , Xiaosong Yang , Chad Walters , Choong Soon Chang
发明人： HUI SHEN , Mao Yang , Lintao Zhang , Zhenyu Zhao , Xiao Wu , Ying Yan , Xiaosong Yang , Chad Walters , Choong Soon Chang
IPC分类号： G06F17/30
CPC分类号： G06F17/30864 , G06F17/30312
摘要： Subject matter described herein includes a multi-layer search-engine index. Accordingly, the search-engine index is divided into multiple indexes, each of which includes a respective set of information used to serve (i.e., respond to) a query. One index includes a term index, which organizes a set of terms that are found among a collection of documents. Another index includes a document index, which organizes a set of documents that are searchable. A computing device is used to serve the search-engine index (i.e., to analyze the index when identifying documents relevant to a search query). For example, a solid-state device might be used to serve the multi-layer search-engine index.
摘要翻译：本文描述的主题包括多层搜索引擎索引。因此，搜索引擎索引被分成多个索引，每个索引包括用于服务（即响应）查询的相应信息集合。一个索引包括术语索引，其组织在一组文档中找到的一组术语。另一个索引包括一个文档索引，它组织一组可搜索的文档。计算设备用于服务搜索引擎索引（即，当识别与搜索查询相关的文档时分析索引）。例如，可以使用固态设备来服务多层搜索引擎索引。

22. 发明授权

US08131660B2 Reconfigurable hardware accelerator for boolean satisfiability solver 有权
标题翻译：用于布尔可满足性求解器的可重构硬件加速器
公开(公告)号：US08131660B2
公开(公告)日：2012-03-06
申请号：US12099160
申请日：2008-04-08
申请人： John Davis , Zhangxi Tan , Fang Yu , Lintao Zhang
发明人： John Davis , Zhangxi Tan , Fang Yu , Lintao Zhang
IPC分类号： G06N5/02
CPC分类号： G06N5/04
摘要： A hardware accelerator is provided for Boolean constraint propagation (BCP) using field-programmable gate arrays (FPGAs) for use in solving the Boolean satisfiability problem (SAT). An inference engine may perform implications. Block RAM (BRAM) may be used to store SAT instance information. Computation may be co-located with the BRAM memory, taking advantage of the high on-chip bandwidth and low latency of an FPGA. SAT instances may be partitioned into multiple groups that can be processed by multiple inference engines in parallel. New SAT instances can be inserted into FPGA without invoking the time-consuming FPGA re-synthesizing process.
摘要翻译：提供了用于布尔约束传播（BCP）的硬件加速器，使用现场可编程门阵列（FPGA）来解决布尔可满足性问题（SAT）。推理引擎可能会产生影响。块RAM（BRAM）可用于存储SAT实例信息。计算可以与BRAM存储器共存，利用FPGA的高片上带宽和低延迟。 SAT实例可以被划分成多个可由多个推理引擎并行处理的组。新的SAT实例可以插入到FPGA中，而无需调用耗时的FPGA重新合成过程。

23. 发明授权

US07984332B2 Distributed system checker 有权
标题翻译：分布式系统检查器
公开(公告)号：US07984332B2
公开(公告)日：2011-07-19
申请号：US12272779
申请日：2008-11-17
申请人： Junfeng Yang , Lintao Zhang , Lidong Zhou , Zhenyu Guo , Xuezheng Liu , Jian Tang , Mao Yang
发明人： Junfeng Yang , Lintao Zhang , Lidong Zhou , Zhenyu Guo , Xuezheng Liu , Jian Tang , Mao Yang
IPC分类号： G06F11/00
CPC分类号： G06F11/362
摘要： A distributed system checker may check a distributed system against events to detect bugs in the distributed system. The events may include machines crashes, network partitions, and packet losses, for example. The distributed system checker may check a distributed system that can have multiple threads and multiple processes running on multiple nodes. To obtain control over a distributed system, a distributed system checker may insert an interposition layer between a process and the operating system on each node.
摘要翻译：分布式系统检查器可以根据事件检查分布式系统以检测分布式系统中的错误。例如，事件可能包括机器崩溃，网络分区和数据包丢失。分布式系统检查器可以检查可以在多个节点上运行多个线程和多个进程的分布式系统。为了获得对分布式系统的控制，分布式系统检查器可以在进程和每个节点上的操作系统之间插入插入层。

24. 发明申请

US20100057647A1 ACCOMMODATING LEARNED CLAUSES IN RECONFIGURABLE HARDWARE ACCELERATOR FOR BOOLEAN SATISFIABILITY SOLVER 审中-公开
标题翻译：适用于可重构硬件加速器中的有针对性的条款，适用于布鲁塞尔满意度解决方案
公开(公告)号：US20100057647A1
公开(公告)日：2010-03-04
申请号：US12203948
申请日：2008-09-04
申请人： John Davis , Zhangxi Tan , Fang Yu , Lintao Zhang
发明人： John Davis , Zhangxi Tan , Fang Yu , Lintao Zhang
IPC分类号： G06F15/18 , G06N5/04
CPC分类号： G06N20/00
摘要： A hardware accelerator is provided for Boolean constraint propagation (BCP) using field-programmable gate arrays (FPGAs) for use in solving the Boolean satisfiability problem (SAT). An inference engine may perform implications. Learned clauses may be generated during conflict analysis. Operations pertaining to learned clauses may include clause insertion and clause deletion (e.g., by invalidation) from a learned clause inference engine, and “garbage collection” in which unused or invalidated clauses may be removed from an inference engine.
摘要翻译：提供了用于布尔约束传播（BCP）的硬件加速器，使用现场可编程门阵列（FPGA）来解决布尔可满足性问题（SAT）。推理引擎可能会产生影响。在冲突分析期间可能会生成学习的子句。关于学习条款的操作可以包括来自学习子句推理引擎的子句插入和子句删除（例如，通过无效），以及可以从推论引擎中去除未使用或无效的子句的“垃圾回收”。

25. 发明申请

US20090254505A1 RECONFIGURABLE HARDWARE ACCELERATOR FOR BOOLEAN SATISFIABILITY SOLVER 有权
标题翻译：可重构硬件加速器，适用于布鲁塞尔满意度解决方案
公开(公告)号：US20090254505A1
公开(公告)日：2009-10-08
申请号：US12099160
申请日：2008-04-08
申请人： John Davis , Zhangxi Tan , Fang Yu , Lintao Zhang
发明人： John Davis , Zhangxi Tan , Fang Yu , Lintao Zhang
IPC分类号： G06N5/04
CPC分类号： G06N5/04
摘要： A hardware accelerator is provided for Boolean constraint propagation (BCP) using field-programmable gate arrays (FPGAs) for use in solving the Boolean satisfiability problem (SAT). An inference engine may perform implications. Block RAM (BRAM) may be used to store SAT instance information. Computation may be co-located with the BRAM memory, taking advantage of the high on-chip bandwidth and low latency of an FPGA. SAT instances may be partitioned into multiple groups that can be processed by multiple inference engines in parallel. New SAT instances can be inserted into FPGA without invoking the time-consuming FPGA re-synthesizing process.
摘要翻译：提供了用于布尔约束传播（BCP）的硬件加速器，使用现场可编程门阵列（FPGA）来解决布尔可满足性问题（SAT）。推理引擎可能会产生影响。块RAM（BRAM）可用于存储SAT实例信息。计算可能与BRAM存储器共存，利用FPGA的高片上带宽和低延迟。 SAT实例可以被划分成多个可由多个推理引擎并行处理的组。新的SAT实例可以插入到FPGA中，而无需调用耗时的FPGA重新合成过程。

26. 发明授权

US07577625B2 Handling of satisfaction and conflicts in a quantified Boolean formula solver 失效
标题翻译：在量化布尔公式求解器中处理满意度和冲突
公开(公告)号：US07577625B2
公开(公告)日：2009-08-18
申请号：US11328009
申请日：2006-01-09
申请人： Lintao Zhang
发明人： Lintao Zhang
IPC分类号： G06N5/02 , G06N5/04
CPC分类号： G06N5/003
摘要： In order to provide for more efficient QBF satisfiability determination, the formula to be checked is transformed into one formula which is equi-satisfiable, and one which is equi-tautological. The conjunction or disjunction of these two formulas, then, is used to determine satisfiability, with the result being that a determination of satisfiability is more easily achieved. A conjunctive normal form transformation of the initial formula yields a group of clauses, only one of which must be unsatisfiable for the formula to be unsatisfiable. A disjunctive normal form transformation of the initial formula yields a group of cubes, only one of which must be satisfiable in order for the formula to be determined to be satisfiable.
摘要翻译：为了提供更有效的QBF可满足度确定，要检查的公式被转换为一个等价可比的公式，其中一个是等价的。然后，这两个公式的连接或分离用于确定可满足性，结果是更容易实现可满足性的确定。初始公式的联合正态形式转换产生一组条款，其中只有一个条款必须不能令人满意，因为该公式不能令人满意。初始公式的分离正态形式转换产生一组立方体，其中只有一个立方体必须是可满足的，以便确定公式是可满足的。

27. 发明申请

US20060190865A1 Quantified boolean formula (QBF) solver 有权
标题翻译：量化布尔公式（QBF）求解器
公开(公告)号：US20060190865A1
公开(公告)日：2006-08-24
申请号：US11038958
申请日：2005-01-18
申请人： Yuan Yu , Lintao Zhang
发明人： Yuan Yu , Lintao Zhang
IPC分类号： G06F17/50
CPC分类号： G06F17/504 , G06F17/11
摘要： Quantified Boolean formula (QBF) techniques are used in determining QBF satisfiability. A QBF is broken into component parts that are analyzable by a satisfiability (SAT) solver. Each component is then independently, and perhaps in parallel, analyzed for satisfiability. If a component is unsatisfiable, then it is determined that the QBF is unsatisfiable, and the analysis is stopped. If a component is satisfiable, then an assignment corresponding to the satisfiable component is noted. If a component is satisfiable, then it is appended to another untested component to provide a combination component, and the satisfiability of the combination component is analyzed. Such appending and analysis is repeated until the QBF is completed and determined to be satisfiable or determined to be unsatisfiable.
摘要翻译：量化布尔公式（QBF）技术用于确定QBF可满足性。 QBF被分解成可满足性（SAT）求解器可分析的组件。然后分析每个组件的可靠性，并且可能并行地进行分析。如果组件不能令人满意，则确定QBF不可满足，并且分析停止。如果组件是可满足的，则记录对应于可满足组件的分配。如果组件可满足，则将其附加到另一未测试组件以提供组合组件，并分析组合组件的可满足性。重复这种附加和分析直到QBF完成并确定为满足或确定为不满意。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式