会员体验
专利管家(专利管理)
工作空间(专利管理)
风险监控(情报监控)
数据分析(专利分析)
侵权分析(诉讼无效)
联系我们
交流群
官方交流:
QQ群: 891211   
微信请扫码    >>>
现在联系顾问~
热词
    • 7. 发明授权
    • System and method for processing graphic delay data of logic circuit to
reduce topological redundancy
    • 用于处理逻辑电路的图形延迟数据以减少拓扑冗余的系统和方法
    • US5841673A
    • 1998-11-24
    • US593569
    • 1996-01-30
    • Noriya KobayashiSharad Malik
    • Noriya KobayashiSharad Malik
    • G06F17/50G06F17/00
    • G06F17/5031
    • A delay network of logic circuit delay data composed of a first set of vertices containing first to fourth vertices, and a first set of weighted directional edges containing a first directional edge extending from the first vertex to the fourth vertex, a second directional edge extending from the second vertex to the third vertex, a third directional edge extending from the first vertex to the third vertex, and a fourth directional edge extending from the second vertex to the fourth vertex, is converted into a delay network composed of a second set of vertices containing the first to fourth vertices and an added fifth vertex, and a second set of weighted directional edges containing a fifth directional edge extending from the first vertex to the fifth vertex, a sixth directional edge extending from the second vertex to the fifth vertex, a seventh directional edge extending from the fifth vertex to the third vertex, and an eighth directional edge extending from the fifth vertex to the fourth vertex.
    • 由包含第一至第四顶点的第一组顶点组成的逻辑电路延迟数据的延迟网络以及包含从第一顶点延伸到第四顶点的第一方向边缘的第一组加权方向边缘,第二方向边缘从 第二顶点到第三顶点,从第一顶点延伸到第三顶点的第三方向边缘和从第二顶点延伸到第四顶点的第四方向边缘被转换成由第二组顶点组成的延迟网络 包含第一至第四顶点和第五顶点,以及包含从第一顶点延伸到第五顶点的第五方向边缘的第二组加权方向边缘,从第二顶点延伸到第五顶点的第六方向边缘, 从第五顶点延伸到第三顶点的第七方向边缘以及从第五顶点延伸到f的第八方向边缘 神话顶点
    • 9. 发明授权
    • Method and system for efficient implementation of boolean satisfiability
    • 有效实现布尔可满足性的方法和系统
    • US07418369B2
    • 2008-08-26
    • US10238125
    • 2002-09-09
    • Matthew MoskewiczConor MadiganSharad Malik
    • Matthew MoskewiczConor MadiganSharad Malik
    • G06F17/11
    • G06F17/504
    • Disclosed is a complete SAT solver, Chaff, which is one to two orders of magnitude faster than existing SAT solvers. Using the Davis-Putnam (DP) backtrack search strategy, Chaff employs efficient Boolean Constraint Propagation (BCP), termed two literal watching, and a low overhead decision making strategy, termed Variable State Independent Decaying Sum (VSIDS). During BCP, Chaff watches two literals not assigned to zero. The literals can be specifically ordered or randomly selected. VSIDS ranks variables, the highest-ranking literal having the highest counter value, where counter value is incremented by one for each occurrence of a literal in a clause. Periodically, the counters are divided by a constant to favor literals included in recently created conflict clauses. VSIDS can also be used to select watched literals, the literal least likely to be set (i.e., lowest VSIDS rank, or lowest VSIDS rank combined with last decision level) being selected to watch.
    • 披露了一个完整的SAT求解器,Chaff,比现有的SAT解算器快一到两个数量级。 Chaff采用戴维斯 - 普特南(DP)回溯搜索​​策略,采用高效的布尔约束传播(BCP),称为两个文字观看,以及称为可变状态独立衰减(VSIDS)的低开销决策策略。 在BCP期间,Chaff观察到两个文字未分配到零。 文字可以特别订购或随机选择。 VSIDS排列变量,最高排名的文字具有最高的计数器值,其中计数器值在子句中每次出现文字时增加1。 定期地,计数器除以常数,以支持最近创建的冲突条款中包括的文字。 VSIDS也可以用于选择观看的文字,被选择观看的文字最少可能设置(即,最低的VSIDS等级或最后的VSIDS等级与最后的决定级别相结合)。
    • 10. 发明授权
    • Implementation of boolean satisfiability with non-chronological
backtracking in reconfigurable hardware
    • 在可重配置硬件中实现具有非时序回溯的布尔可满足性
    • US6038392A
    • 2000-03-14
    • US85646
    • 1998-05-27
    • Pranav AsharSharad MalikMargaret MartonosiPeixin Zhong
    • Pranav AsharSharad MalikMargaret MartonosiPeixin Zhong
    • G06F9/44G06F17/10G06F17/50G06N5/04
    • G06F17/5054
    • A Boolean SAT solver uses reconfigurable hardware to solve a specific input problem. Each of the plurality of ordered variables has a corresponding one of a plurality of state machines. Each state machine has an implication circuit for its respective variable, and operates in parallel according to an identical state machine. One state machine implements the Davis-Putnam method in hardware and provides improved performance over software by virtue of the parallel checking of direct and transitive implications. Another state machine implements a novel non-chronological backtracking method that takes advantage of the parallel implication checking and avoids the need to maintain or to traverse a GRASP type implication graph in the event of backtracking. The novel non-chronological backtracking provides for setting a blocking variable as a leaf variable and for changing only the value of the leaf variable, but possibly changing both the value and identity of a backtracking variable.
    • 布尔SAT求解器使用可重构硬件来解决特定的输入问题。 多个有序变量中的每一个具有多个状态机中的对应的一个。 每个状态机具有用于其各自变量的含义电路,并且根据相同的状态机并行操作。 一个状态机通过硬件实现Davis-Putnam方法,并通过并行检查直接和传递的影响,提高了软件性能。 另一种状态机实现了一种新颖的非时间回溯方法,其利用并行含义检查的优点,并避免在回溯事件中维护或遍历GRASP类型含义图。 新颖的非时间回溯提供将阻塞变量设置为叶变量,并且仅改变叶变量的值,但可能改变回溯变量的值和身份。