[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

WO2015148599A1 - Résolution de problèmes non déterministes polynomiaux complets sans coût hyper polynomial - Google Patents

Résolution de problèmes non déterministes polynomiaux complets sans coût hyper polynomial Download PDF

Info

Publication number
WO2015148599A1
WO2015148599A1 PCT/US2015/022377 US2015022377W WO2015148599A1 WO 2015148599 A1 WO2015148599 A1 WO 2015148599A1 US 2015022377 W US2015022377 W US 2015022377W WO 2015148599 A1 WO2015148599 A1 WO 2015148599A1
Authority
WO
WIPO (PCT)
Prior art keywords
assertions
assertion
counter
prevailing
constraint
Prior art date
Application number
PCT/US2015/022377
Other languages
English (en)
Inventor
Clayton Gillespie
Original Assignee
Clayton Gillespie
Priority date (The priority date is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the date listed.)
Filing date
Publication date
Application filed by Clayton Gillespie filed Critical Clayton Gillespie
Priority to KR1020167011170A priority Critical patent/KR102341689B1/ko
Priority to CA2943044A priority patent/CA2943044C/fr
Priority to CN201580002451.1A priority patent/CN105745618A/zh
Priority to SG11201606976PA priority patent/SG11201606976PA/en
Priority to JP2016526262A priority patent/JP6550384B2/ja
Priority to EP15768263.4A priority patent/EP3123302A4/fr
Priority to US15/126,227 priority patent/US10528868B2/en
Priority to AU2015236144A priority patent/AU2015236144B2/en
Priority to MYPI2016703394A priority patent/MY184777A/en
Publication of WO2015148599A1 publication Critical patent/WO2015148599A1/fr
Priority to IL247866A priority patent/IL247866B/en

Links

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING OR COUNTING
    • G06N—COMPUTING ARRANGEMENTS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computing arrangements using knowledge-based models
    • G06N5/04—Inference or reasoning models
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING OR COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/10—Complex mathematical operations
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING OR COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/10—Complex mathematical operations
    • G06F17/11—Complex mathematical operations for solving equations, e.g. nonlinear equations, general mathematical optimization problems
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING OR COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F2111/00—Details relating to CAD techniques
    • G06F2111/06—Multi-objective optimisation, e.g. Pareto optimisation using simulated annealing [SA], ant colony algorithms or genetic algorithms [GA]
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING OR COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design
    • G06F30/39—Circuit design at the physical level
    • G06F30/392—Floor-planning or layout, e.g. partitioning or placement

Definitions

  • Computational complexity theory is a branch of computer science that focuses on classifying computational problems according to their inherent difficulty.
  • One such classification is "NP", which is the class of problems that can be solved in polynomial time by an algorithm running on a non-deterministic Turing machine.
  • An algorithm is said to run in polynomial time if its running time is upper-bounded by a polynomial function of the size of the input for the algorithm, i.e., T(n) e 0(n k ) for some constant k.
  • the present invention might be compared to the Newton Method, the Davis-Putnam-Logemann- Loveland (DPLL) algorithm, and the Conflict-Driven Clause Learning (CDCL) algorithm.
  • Embodiments of the present invention address problems associated with automated solution of NP, NP-complete, and NP-hard problems in polynomial time without the need for tuning.
  • Embodiments of the present invention may be implemented using any of a variety of techniques, such as computer- implemented methods and/or systems. Any reference herein to embodiments of the present invention which are implemented using a "method” or “methods” should be understood to include embodiments implemented using methods and/or systems. Similarly, any reference herein to embodiments of the present invention which are implemented using a "system” or “systems” should be understood to include embodiments implemented using methods and/or systems.
  • Embodiments of the present invention provide a method for solving NP, NP-complete, or NP- hard problems in polynomial time without the need for tuning.
  • Certain embodiments of the present invention include a method which includes converting a given problem definition into an expression composed of one or more constraints; selecting assumed value predicates for the variables of the expression; propagating the implications of the assumptions; identifying any contradictions caused by the implications of the assumptions; determining, for each identified contradiction, whether that contradiction can be moved towards a corresponding location where it will resolve as an implication; for each contradiction which can be so moved, moving that contradiction towards its corresponding location; and, for any contradiction which cannot be so moved, reporting that the expression is unsatisfiable.
  • Embodiments of the present invention provide a method for improving the time requirement of solving of a logical or numerical problem by resolving conditional contradictions arising during the solving of the problem, without the need for tuning.
  • the problem is formed of constraints, each of which includes one or more variables. Solving the problem includes determining whether the problem is satisfiable by a set of variable values or unsatisfiable when there are no sets of variable values that satisfy the expression.
  • the problem may be a logical expression in conjunct normal form (CNF) such that it is a conjunction of a set of constraints, where each of the constraints is a disjunction of several variables.
  • CNF conjunct normal form
  • the method includes receiving, as part of the problem being input to a computer, unconditional assertions regarding values of zero or more of the variables; making assumptions regarding values of one or more of the variables that are not subject of the unconditional assertions; and using the assumptions or the unconditional assertions to make assertions of terms regarding values for other variables of the problem.
  • a constraint is forced to assert a term when, as a result of existing assumptions or assertions, the values of all but one of the terms are restricted. Then, for the constraint to be satisfied, the one remaining term becomes asserted and cannot be negated without creating a contradiction. If the value of the asserted term is not already determined, it becomes determined.
  • the constraint is asserting, and if it caused the value of the asserted term to become determined, then the assertion and the constraint that asserts it becomes prevailing.
  • the method continues with setting values for the variables as determined values responsive to the unconditional assertions, the assumptions, or the generated conditional assertions.
  • the variables not having a determined value are called free variables.
  • the iteration of the making of assumptions, the making of assertions, and the setting of values for the variables as determined forms the process of implication.
  • a contradiction may be conditioned on the assumptions and arises when all terms of some constraint are restricted.
  • the method moves a contradiction by forcing the assertion of a value of a term of a first contradicted constraint which in turn restricts terms of the same variable in other constraints that are not already restricted or negates disagreeing asserted values or assumptions of the same variable, possibly producing a contradiction in a contiguous second constraint and always resolving the contradiction in the first constraint.
  • the method directs this motion of the contradiction in order to expel the contradiction from the problem. It is advantageous for the method not to force the assertion of a value of any term that is unconditionally negated. It is also advantageous for the direction of motion of a contradiction to be chosen in such a way that all possible paths of escape will be explored if the contradiction cannot be expelled.
  • the method detects when the term being counter-asserted has no assumptions in the path behind the direction of motion and marks that assertion as being unconditional. The method continues by reporting that the problem is satisfied if the count of the free variables is zero and all contradictions have been expelled, or by reporting that the problem is unsatisfiable if a contradiction is encountered where all the terms are unconditionally negated.
  • RAM random access memory
  • Figure 1 shows a Variable and Constraint diagram that demonstrates by example that a process that parameterizes teardrops as summarizing constraints, as DPLL and CDCL do, is insufficient to avoid hyper-polynomial computational costs without some form of tuning.
  • Figure 2 shows a flowchart of a method performed by a computer system implemented according to one embodiment of the present invention.
  • the white circles represent variables and the lines represent constraints.
  • a term is represented by a constraint line traversing a variable circle. Lines that traverse a variable circle in a vertical way represent terms that have the ⁇ ' value predicate for that variable. Lines that traverse a variable circle in a horizontal way represent terms that have the 'X' value predicate for that variable.
  • the variable circles are labeled with a letter of the Latin alphabet.
  • the expression represented in Figure 1 is identical to the expression represented in the following table:
  • the contradiction in constraint 23 has three assumptions in its reason, xB, xC, and xG. Because stratified reasons are being used, the precipitant of this teardrop must be in a path that contains xG. The identified precipitant in this case is xG itself.
  • the summarizing constraint produced is a disjunct phrase containing the following terms: oB, oC, oG.
  • variables C, D, E, and F have identical connections to other variables, and the same can be said for the variables G, H, J, and K.
  • These blocks are connected in series with an initial segment consisting of the constraints that contain terms of B, and a terminal segment consisting of constraints that contain terms of Z.
  • the number of summarizing constraints produced by this example is equal to the product of the sizes of the blocks. If the number of variables in the identically connected sets is varied, then the number of summarizing constraints produced continues to be the product of the sizes, as long as the block adjacent to the initial segment does not have its size reduced to 1. If additional blocks are inserted into the series, the number of summarizing constraints produced will be the product of the sizes of all the blocks, as long as B remains the variable of the first assumption, and as long as the block adjacent to the initial segment is always the last block in which assumptions are made.
  • a product of block sizes is a hyper- polynomial number, and therefore the method used in the description above does not provide a solution without hyper-polynomial cost.
  • embodiments of the present invention move contradictions contiguously through the same proximal space, they are able to detect relationships that the example algorithm misses or detects only after great effort, and this detection occurs specifically when the contradiction reverses through a point of former divergence which is not a precipitant such that the latest assumption is removed from the reason of the counter-assertion, or when a contradiction causes an assumption to be negated and counter-assertion or implication continues outside a single stratum.
  • Embodiments of the present invention provide systems, methods, and/or devices for improving the performance of machines that solve problems in the complexity classes called "NP,” “NP-complete,” and “NP-hard”.
  • P is a class of problems that can be solved by a deterministic Turing machine in polynomial time. A deterministic Turing machine engages in serial or limited parallel-processing.
  • NP is a class of problems that can be solved by a non-deterministic Turing machine in polynomial time. A non- deterministic Turing machine is capable of unlimited parallel-processing.
  • NP-complete is a subset of hard problems in NP whose membership in P is doubted. Examples of NP-complete problems are the Traveling Salesman Problem and the Satisfiability or satisfaction (SAT) Problem.
  • NP-complete problems pertain to a number of technical fields.
  • NP-hard are those problems which have a component that is known to be NP-complete but which have other components and those other components are tractable but otherwise are unclassified.
  • the conjunct normal form represents an expression as a list of conjunct ("ANDed") constraints where each constraint is composed of one or more disjunct ("ORed") logical terms.
  • a "term” is a particular instance of a value assignment (usually “true” or “false") for a particular variable where the particular value assignment occurs in the context of a particular constraint. Therefore, a term is a value of a variable in the context of a particular constraint. The same value of the same variable in a different constraint represents a different term. It is known that the representation of any problem which is in NP has a conversion to a logical expression in conjunct normal form which does not incur a hyper-polynomial cost.
  • solutions to NP-complete problems, as well as many other problems in NP have either required an exhaustive search of possible value assignments for the variables represented in the problem, or otherwise required hyper-polynomial costs, such as N! or 3 N , rather than polynomial costs such as N 3 , where N is the size of the input to the problem.
  • Embodiments of the present invention may find solutions to NP-complete problems, and other problems in NP, without requiring an exhaustive search of possible value assignments for the variables represented in the problem, and without otherwise requiring hyper-polynomial costs.
  • embodiments of the present invention permit a computer, whether conventional or purpose-built, to solve NP-complete problems or other problems in NP in a number of elementary steps that is less than a number that is proportional to the fifth exponent of the number of variables in the problem rather than a number that is hyper-polynomial. Embodiments of the present invention thereby enable a reduction in computational cost that is comparable to the reduction from linear to logarithmic cost.
  • Embodiments of the present invention which may be implemented as computer processors and/or computers, provide a very significant improvement to automatic computing devices as well as to other machines that use computers to control their behavior. This improvement greatly reduces the amount of power, cooling, rent, and other costs that are required in order to establish and operate a computer while decisions are being computed, as well as reducing the time that operators of the computer must wait for a result.
  • An automatic computing device that is augmented with embodiments of the present invention may no longer require to be programmed in a conventional way; instead, such a device or system accepts the set of constraints as the requirements to be met, whether those are structural or behavioral requirements, and the machine outputs a result or operates in a manner that satisfies those constraints.
  • One means by which embodiments of the present invention may deliver their improvements to the performance of computers and other devices that perform automated processes is by imposing a specific arrangement of switches within the computer and these switches rely on the physical property of exclusion.
  • Exclusion among fermions is inherent in that no two fermions, or particles, of the same type can occupy the same space at the same time; so forcing one particle into position may force another particle out of position, as when the teeth of one gear push against the teeth of another gear that is meshed with the first, thus switching the positions of both gears while only applying external force to one.
  • Exclusion among bosons is inherent in the potentials we can engineer across carriers - we arrange that the potential is always either high or low, as in a transistor.
  • One embodiment of the present invention is a data processing system which solves given NP, NP-complete, or NP-hard problems using a deterministic machine in polynomial time.
  • the given problem definition is converted into an expression composed of logical or otherwise deterministic constraints.
  • Embodiments of the present invention may be implemented as one or more devices and/or automated processes that process information in order to render decisions efficiently.
  • the behavior of such embodiments may be explained using a system of objects, necessary relationships that contribute to the definition of what those objects are, and transformations that alter the states of those objects in ways that are consistent with the necessary relationships. Certain vocabulary used to describe embodiments of the present invention are described below.
  • Each "variable" is a locale of variability, which can be characterized as a set of values.
  • each variable is the name of a logical predicate which appears in the given expression.
  • a variable could be the set of valid voltages supplied to a pin on a computer chip, a numeric register, an alphanumeric string in some programming language, or any data structure that has the property of representing one (or no) value at a time and can represent more than one value over time.
  • a variable here is similar to a variable in the domain of software engineering.
  • a variable could be defined as a logical predicate on a numeric variable that does not otherwise appear in the expression.
  • the expression variable is Boolean not numeric, and the atomic values of the expression variable are "true” and "false”, not numbers.
  • Value predicates are statements that define a specific subset of atomic values of a variable. A set containing all atomic values of a variable is not a valid value predicate. A set containing no atomic values is not a valid value predicate. In other words, "null” and “inherent contradiction” are not valid values in the way of speaking used herein.
  • a "term” is primarily composed of a reference to, or a reproduction of, a variable within the context of a constraint. An explanation of "constraint” is provided farther below. [0050] Certain embodiments of the present invention may be embedded in a system that is interpreted as using two-valued logic. In two-valued logic, a term is typically interpreted as representing a Boolean value of the variable.
  • Certain embodiments of the present invention may be embedded in a system that is interpreted as using many-valued logic.
  • An example of a many-valued logic is first-order logic, which includes representations of numbers.
  • a term may represent a Boolean value as in two- valued logic, but it may instead represent a value of some variable that is not the subject of an explicit predicate.
  • a non-Boolean value When representing a value of such a variable, we call such a term a non-Boolean value.
  • phrase contains an addressable set of terms representing value predicates.
  • a phrase contains any number of terms, but for each term in the phrase, there may be no other term that represents a value predicate of the same variable.
  • Each phrase also represents either a conjunction or disjunction of the value predicates it contains.
  • a numerically represented vector is an example of a conjunct phrase, and a CNF constraint is an example of a disjunct phrase.
  • a "constraint" is represented by a non-empty disjunct phrase of Boolean terms.
  • a constraint may be represented by either a disjunct phrase or a satisfiable- or-mutually-mapped expression (SOMME).
  • One set of value predicates is "complementary" to another set of value predicates for the same variable if no predicate in either set disagrees with the other predicates in the same set, the intersection of the first set disagrees with the intersection of the second set, and every atomic value of the variable is in either one set or the other exclusively.
  • each variable value is complementary to the only other possible value for that variable and disagrees with it.
  • the SOMME implies a non-tautological value predicate for a variable other than the variable represented by this term;
  • a value predicate is "asserted" for the variable of the one unrestricted term. If all the restricted terms of a constraint are unconditionally restricted, then an assertion of that constraint imposed by those restrictions is trivially unconditional. Also, if a constraint contains only one term, the value predicate represented for that term is trivially unconditionally asserted. Otherwise, if any of the terms of a constraint is not unconditionally restricted, but the constraint asserts a value predicate, that assertion is conditional.
  • constraints contain terms that represent value predicates that represent sets of atomic values with more than one member, it is possible for a constraint to unconditionally assert a first value predicate and to conditionally assert a second value predicate that is a proper subset of its unconditional assertion.
  • a constraint may continue to have a conditional assertion even after one or more of its conditional restrictions are removed. Unconditional restrictions cannot be removed.
  • any unconditional assertion for that variable is the one that prevails.
  • the choice of which assertion to designate as prevailing is arbitrary and is most easily rendered by taking the first such assertion that presents itself. (See farther below for a discussion of conditional assertions that cannot become prevailing regardless of what other assertions exist.)
  • a subsequently presented unconditional assertion represents a value predicate that is a subset of the value predicate for a previously presented prevailing conditional assertion for the same variable
  • the previously presented conditional assertion may (but need not) become non-prevailing.
  • unconditional assertions usually become non-prevailing but in fact remain prevailing
  • the efficiency of the present invention is reduced but not to the point that it becomes hyper- polynomial.
  • the discussions below presume that such assertions become non-prevailing.
  • conditional assertions that are valid candidates for being designated as prevailing when no unconditional assertions for the same variable exist the first such assertion that presents itself should be made prevailing.
  • intersection of the set of value predicates represented by a subsequently presented valid candidate conditional assertion and the intersection of the previously presented prevailing unconditional and conditional assertions for the same variable is a proper subset of the intersection of the previously presented prevailing unconditional and conditional assertions, then the subsequently presented assertion becomes prevailing. In all other cases, a subsequently presented conditional assertion does not become prevailing. (Invalid candidates for being designated as prevailing are discussed farther below.) [0087] As each assertion becomes prevailing, it may be associated with the next number in a sequence. This number is called the "prevalence" number of the assertion.
  • assertions that are not produced by constraints and which are for a variable that previously had no determinant, or has a determinant but the determinant represents a set containing more than one atomic value.
  • Such an assertion is called an "assumption” or an “assumptive assertion” and its value predicate is “assumptive”.
  • assertions that are forced from constraints are called “implicated assertions”. Assumptions are always conditional, and each value predicate must contribute to the determinant for the variable the assumptive value predicate represents.
  • Any constraint is "satisfied" when one or more of its terms is not restricted and the variable of that term has a determinant.
  • An expression is satisfied when none of its constraints are contradicted and all variables have determinants that represent a set containing a single atomic value.
  • a “pool” is an addressable set to which elements can be added and removed. As a pool perse, elements may be added to or removed from the pool in any order. Pools may also incorporate specific rules for the order in which added elements are removed. For example, non-prioritized queues incorporate a "first-in-first-out” (FIFO) rule, and stacks incorporate a “first-in-last-out” (FILO) rule.
  • FIFO first-in-first-out
  • FILO first-in-last-out
  • Implication is a process that is triggered when a new determinant is introduced. In this process, the terms that are restricted by the new determinant are identified, and then the constraints of those terms are checked to see if all or all but one of the terms in each constraint is restricted.
  • Implication may halt as soon as a constraint becomes contradicted and always halts when no new prevailing assertions were produced in the most recent iteration of the implication process.
  • Behavior #1 One behavior that may be exhibited by an algorithm to solve problems in NP, NP-complete, or NP-hard without incurring hyper-polynomial costs and without the need for the algorithm to be tuned is such that, when contradictions are found in the rhizomatic networks that are made apparent by the implication of assumptions, these contradictions are moved through the networks in an attempt to assert a value predicate for a term where there is no disagreeing value predicate that is asserted, in order to satisfy all the constraints in the prevailing paths that lead to the contradiction.
  • Algorithms that rely on random variations of a putative solution such as Genetic Algorithms, do not identify the case when there is no solution set at all and are susceptible to performing meandering variations indefinitely when the solution set is small.
  • Behavior #1 avoiding the pathological orderings in algorithms that create summarizing constraints is what tuning should provide; so to provide non-hyper-polynomial cost solutions without tuning, Behavior #1 resolves contradictions while avoiding the creation of new summarizing constraints with an indeterminate number of terms and without relying on random variations.
  • assumptions are non-prevailing but do contribute to the determinant for the variable that the assumption represents.
  • a term that was restricted, but for which there are no extant prevailing assertions that conjunctively converge to produce a determinant that represents the restriction is either restricted by an assumption or was restricted by a prevailing assertion but that assertion has been subsequently removed, or is restricted in part by an implicated assertion that is not prevailing.
  • Each contradiction must be moved toward a term that is restricted by an assumption or toward some other term for which the recorded restriction is not fully supported by prevailing assertions that are part of a prevailing path that leads to and produces the contradiction.
  • Terms for which the recorded restriction is not fully supported by prevailing assertions are called “destinations”, and destinations that are not fully supported by the conjunctive convergence of extant prevailing assertions and assumptions are called "pseudo-assumptions”.
  • Counter-asserting resolves the contradiction in one constraint and may "negate" some assertions that contributed to the determinant for the variable represented by the counter-assertion. Negation of an assumptive assertion eliminates the assumption. Negation of an implicated assertion or counter-asserted assertion removes the assertion itself and creates a contradiction in its constraint.
  • a counter-assertion may also provide a restriction in a constraint that was not asserting and produce an implicated assertion from that constraint.
  • Another behavior (“Behavior #3") that may be exhibited by an algorithm to solve problems in NP, NP-complete, or NP-hard without incurring hyper-polynomial costs and without the need for tuning is such that the value predicate counter-asserted must not only resolve the contradiction in the counter-asserting constraint, it must also not create a contradiction in any of the constraints in the prevailing path that leads to and produces the counter-assertion, excluding constraints that provided assertions that are specifically negated by the counter-assertion.
  • This behavior requires that the decision of which value predicate to counter-assert has information about the prevailing path leading to and producing the counter-assertion.
  • any conditionally restricted term in the contradicted constraint may be counter-asserted according to the rules of implication, and that counter- assertion is guaranteed to not create contradictions in the constraints in the prevailing path that leads to and produces the counter-assertion.
  • Behavior #4 Another behavior that may be exhibited by an algorithm to solve problems in NP, NP-complete, or NP-hard without incurring hyper-polynomial costs and without being tuned is such that when multiple paths have equal potential to satisfy the expression by expelling a contradiction, the manner by which the term that is in the contradicted constraint for which a value predicate is to be counter- asserted is chosen must be such that the motion of the contradiction does not retrace paths with a hyper- polynomial number of iterations of the same path nor a hyper-polynomial number of variations of paths.
  • Embodiments of the present invention may exhibit any one or more of Behavior #1 , Behavior #2, Behavior #3, and Behavior #4, each of which may be implemented using a device, software, or automated process, in any combination.
  • Embodiments of the present invention may be implemented to improve the functioning of a computer itself by providing the benefits described above. Such embodiments achieve their beneficial results using the novel and nonobvious techniques disclosed herein, and therefore do not merely constitute an instruction to apply an abstract idea or to implement an abstract idea on a computer.
  • Embodiments of the present invention which take the form of an improved computer (or one or more components thereof, such as an improved processor) include novel and nonobvious components, such as novel and nonobvious circuits for performing the novel and nonobvious functions disclosed herein.
  • Such novel and nonobvious circuits by virtue of being novel and nonobvious, are not generic computer components, but instead are components which, as a whole, are unique to embodiments of the present invention, even if they include certain subcomponents (such as certain logic gates) which are known to those having ordinary skill in the art.
  • Counter-assertion exhibits Behavior #1. It is efficient for contradictions to be resolved in certain sequences. The resolution of one original contradiction is best followed by the resolution of the contradiction produced in a constraint that provided one of the prevailing assertions that were negated by the counter-assertion produced from the original contradicted constraint and so on. The contradictions may be resolved in other orders, but resolving them in this order reduces the number of revisions of the possible means of tracking the paths of prevailing assertions that would otherwise be necessary to providing rigorous accuracy in these tracking elements.
  • each prevailing assertion records a "full reason" that contains the value predicates of previous assertions that restricted terms in the constraints of the prevailing paths that led to and produced the current prevailing assertion, and each value in a full reason is augmented with counts.
  • One such count is the "fulfilled” count.
  • a candidate implicated prevailing assertion has a full reason that contains the union of the set of value predicates in the full reasons for all extant prevailing assertions that are not unconditional and which conjunctively converge to produce determinants that restrict terms in the constraint from which the candidate assertion derives, unioned with the set of value predicates of the assertions that are not unconditional and which restrict terms in the constraint from which the candidate assertion derives;
  • the fulfilled count is the sum of the corresponding fulfilled counts derived from previously populated full reasons
  • the fulfilled count for any value predicate in the full reason of the candidate assertion is incremented by one for each value predicate in the set of value predicates of the assertions that are not unconditional and which restrict terms in the constraint from which the candidate assertion derives.
  • the fulfilled count is a way of encoding predecessor prevailing assertions in prevailing paths that led to and produced a single resultant first prevailing assertion.
  • the counts in this encoding permit the prevailing path of a second prevailing assertion to be subtracted from the full reason of the first prevailing assertion without removing any sub-paths that may be common to the prevailing paths of other prevailing assertions that led to and produced the first prevailing assertion.
  • This capability is useful for the proper analysis of the prevailing paths of restricting prevailing assertions in order to decide which restricted terms may be counter-asserted and which counter-assertions must be unconditional.
  • Behavior #2 may be exhibited by some means that provides an ordering of the restricted terms that are in the path that leads to and produces a counter-assertion so that, when accessed in either ascending or else descending order, a candidate assertion in the path is always encountered (by way of the term ordering) before encountering any of the assertions that led to and produced that candidate assertion.
  • “Farness counts” provide such an ordering. Farness counts or some other means of providing this ordering may be employed to exhibit Behavior #2.
  • Maximum distance counts and carefully maintained prevalence numbers are considered to be farness counts. Insofar as prevalence numbers may be used as farness counts, the language used when referring to the ordering of farness counts will assume that ascending order of farness counts indicates increasing farness, even though the descending order typically provides such an ordering for prevalence numbers.
  • Each maximum distance count records the maximum distance between a resultant conditional prevailing assertion and each value predicate in the full reason of the resultant assertion, where "distance” in this context reflects the number of implicational or counter-assertion steps between value predicates and the resultant conditional prevailing assertion.
  • distance in this context reflects the number of implicational or counter-assertion steps between value predicates and the resultant conditional prevailing assertion.
  • the maximum distance counts in the full reason for a non-assumptive resultant conditional prevailing assertion are constructed as follows:
  • a non-necessary count that may be used by embodiments of the present invention is the "unfulfilled" count.
  • unfulfilled counts When unfulfilled counts are used, the manner of accruing the fulfilled count is different than described above, but the manner of accruing the maximum distance counts is the same as above.
  • bracketed statement labels such as "[U1]". These labels uniquely identify the statements and explicitly reiterate the nesting of statements relative to qualifying statements that is normally indicated by indenting of text in pseudo-code. Without an indication of nesting, the description may be interpreted ambiguously.
  • [0179] [U3b2c] Add the value predicates in the co-basis to the basis where they do not already exist, and add the fulfilled and unfulfilled counts from the co-basis to the corresponding fulfilled and unfulfilled counts in the basis, and add the value predicate of the candidate assertion to the basis with a fulfilled count of one and an unfulfilled count of zero, and the candidate assertion is ignored by further processing.
  • [0185] [U4] Use the basis as the full reason of the assertion of the given constraint. [0186]
  • the method of accruing fulfilled and unfulfilled counts described above is a means of compressing the information that is present when fulfilled counts are used and unfulfilled counts are not used and which is necessary to permit the subtraction of a portion of the path behind a prevailing assertion (when this prevailing assertion disagrees with the counter-assertion) without also subtracting sub-paths that are common to the paths of other prevailing assertions that produce the resultant counter-assertion.
  • the maximum number of bits required in order to represent each fulfilled count is equal to the number of variables in the expression.
  • the number of bits required in order to represent each fulfilled count is one, and the number of bits required in order to represent each unfulfilled count is the base-2 logarithm of the number of constraints in the expression, which is usually a significant reduction in the number of switches required to represent the counts and the costs to operate those switches.
  • prevalence numbers instead of maximum distance counts to order the subtraction of prevailing assertions from the basis, but this requires that prevalence numbers consistently act as farness counts and therefore provide an ordering of assertions that prevents the removal of prevailing assertions that appear in sub-paths that are shared between the prevailing paths of other prevailing assertions that must have their full reasons subtracted from the basis and assertions that need not have their full reasons subtracted from the basis.
  • the initial ordering of prevalence numbers is sufficient for them to perform as farness counts when accessed in descending order rather than ascending order, but prevalence numbers are reassigned when terms are counter-asserted, which disturbs the original ordering. Consequently, using prevalence numbers as farness counts usually requires significant revision of the prevalence numbers, which makes the amount of computational work required similar to that which is required when maximum distance counts are used as the farness counts.
  • branch-subtraction when a minuend full reason does not contain the value predicate of a subtrahend assertion, then the branch-subtraction difference is identical to the minuend. Otherwise, the branch-subtraction difference is the result of the following computations:
  • Embodiments of the present invention may include the ability to distinguish whether a portion of a path contains a destination in order to exhibit Behavior #2.
  • the ability to distinguish destinations and therefore count the distinct destinations in a portion of a path can also be very useful. Branch-subtraction can supply both these abilities.
  • Branch-subtraction without the use of unfulfilled counts requires multiplication for every subtracted value predicate in each full reason where branch-subtraction occurs. Multiplication has a computational cost that is the square of the number of bits being multiplied, and this represents another significant computational cost that is incurred when unfulfilled counts are not used.
  • This method ignores all terms that are restricted only by unconditional assertions, and ignores all terms that are restricted by assertions that have already been considered, and notes those terms that are destinations, including terms that are negated by loop assertions, and excluding illegitimate pseudo-assumptions (see farther below); and for each other term, stacks for consideration the conditionally restricted terms in the constraints of prevailing assertions that restrict the given term in a way that ensures depth-first traversal.
  • the value predicates asserted by constraints in a prevailing path must be consistent at the time a decision about the value predicate of a new counter-assertion is made. For disjunct phrases, no special action is necessary because such constraints either assert a pre-defined value predicate for a specific variable or do not make an assertion of that variable at all.
  • a change in a restricting value predicate may result in a change in the value predicate asserted or counter- asserted that has a prevailing path that includes the revised restriction, and these revisions need to be propagated through the prevailing path of any new counter-assertion.
  • Behavior #3 may be violated if the assertions of SOMMEs are maintained rigorously, i.e. at the time of negation; so the revision of value predicates of SOMMEs when there is no conventional mathematical analysis is best propagated lazily, as described immediately below, or not propagated except by dithering, which is explained farther below as part of the discussion of exhibiting Behavior #4.
  • the full reasons may contain value predicates that have a zero fulfilled count, even while there is a prevailing assertion of that predicate. If any such value predicates exist in a full reason, the candidate full reason should be revised by branch-adding the missing reasons so that they then have a non-zero fulfilled count. If nearness counts (see farther below) or farness counts are to be used, then they must be correct at the time they are used (in the basis and co- basis, for example), and those counts should be re-computed when prevailing assertions exist but are not recorded in the full reason of a counter-assertion.
  • an assertion that completes a loop is made to be non-prevailing, regardless of whether prevailing assertions for the same variable are extant or non- extant, but does contribute its value predicate to the determinant for the variable it represents, if the existing determinant does not represent a subset of the atomic values represented by the loop assertion.
  • a loop cannot provide destination-free reasons for its own assertions and therefore a prevailing path that depends on a loop always apparently represents a destination in that path.
  • loop assertions may be explicitly marked in other ways and treated as destinations by those other methods of marking,
  • a "teardrop" exists and Is Identified in the prevailing path of the counter-assertion.
  • the "precipitant" of a teardrop is a value predicate that is known to represent a set of atomic values such thai, if any such atomic value were asserted and the set of constraints that are In the prevailing paths of which the teardrop consists do not already contain a contradiction, the assertion would necessarily produce a contradiction In one of these teardrop constraints, regardless of the order In which assertions are propagated.
  • the precision of a precipitant depends upon the information that is available in the prevailing path of the counter-assertion.
  • a contradiction can be characterized as a disagreement of assertions between multiple rhizomatic networks that may have common network segments. By counter-asserting one of the disagreeing assertions, its network grows; and when the disagreeing assertions are negated, their networks shrink. Whether counter-assertion incorporates branch-subtraction of full reasons of the negated prevailing assertions or back-tracks through the new networks, the incorporated operation ensures that destinations that are strictly ahead of the counter-assertion are not represented as being in the network of the counter-assertion and therefore do not misinform the methods of embodiments of the present invention that exhibit Behavior #2 and Behavior #4.
  • One method of counteracting interference between parallel contradiction resolution processes is to have each process record a separate set of full reasons that can persist when one counter-assertion erases the history of another counter-assertion, but which erases existing full reasons and cross-populates a replacement full reason into the separate stores of parallel contradiction resolution processes whenever a new full reason is generated by any of these processes. Obviously, this method requires a large increase in the amount of data stored.
  • Another method of counteracting interference between parallel contradiction resolution processes is to rank the contradictions so that no counter-assertion resulting from a first contradiction will be permitted if it would erase the history of paths being used by a second contradiction of higher rank, thus effectively suspending the motion of the first contradiction.
  • This method can be improved by altering the ranks of contradictions so that suspended contradictions have their ranks lowered; otherwise a cascade of suspensions could occur, effectively reverting the algorithm to a non-parallelized condition.
  • Great care would be necessary in order to formulate a re-ranking that was guaranteed to prevent hyper-polynomial dithering. (See farther below for a discussion of dithering.)
  • Prevalence of assertions affects the efficiency of the methods that exhibit Behavior #2 positively.
  • the present invention avoids a hyper- polynomial explosion of possible paths that would need to be checked to discover whether any of those paths defined a teardrop and permitted an unconditional counter-assertion. Instead, paths are searched incrementally as long as extant contradictions that are dependent on those paths remain unresolved, in which case the unresolved contradictions provide new prevailing assertions with new paths that re-restrict terms that were formerly pseudo-assumptions. This is a form of path search that will terminate in polynomial time if Behavior #4 is exhibited.
  • each of these SOMMEs may be replaced by a collection of intermediate variables and disjunct phrases.
  • Such a supplementation may require that multiple value predicates are simultaneously revised and therefore asserted, and the nature of the relationship between SOMMES may require that some value predicates are unconditionally asserted even though assumptions exist in the prevailing path; but as long as the prevailing path is still recorded or is still reconstructable, then the present invention can successfully use conventional mathematical analysis as a black box function.
  • Behavior #4 may be exhibited by having some means by which a specific prevailing path on which the contradiction will travel can be chosen and that choice is, by the nature of the means with which it is chosen, not subject to a hyper-polynomial number of revisions.
  • a nearest destination is identified by comparing "minimum distance counts".
  • Minimum distance counts are very similar to maximum distance counts except that they represent the least count among the minimum distance counts associated with the identical value predicates being unioned rather than the greatest count among maximum distance counts.
  • restriction counts are constructed as follows:
  • a nearest destination is identified by comparing "work counts".
  • work counts over restriction counts are that they provide a better estimate of the computational work that may be incurred by moving the contradiction to its destination.
  • Work counts in the full reason for a non-assumptive resultant conditional prevailing assertion are constructed as follows:
  • Nearness counts is the name that generalizes the set of counts that are exemplified above as minimum distance counts, restriction counts, or work counts. Other kinds of nearness counts are possible, but any valid nearness count should support a Nearest Destination method by providing an ordering of directions in which to move a contradiction that persists or becomes more emphatic after the contradiction has moved if the counts are maintained rigorously, as do the example nearness counts described above.
  • the motion of the contradiction may dither when a Nearest Destination method is being used.
  • a contradiction moves toward a chosen destination and then it is revealed that the chosen destination is no longer in the path in that direction or it is actually farther to the chosen destination along this path than it appeared, and a different path to the same destination is nearer relative to the revealed distance along the current path, or a different value predicate is chosen as the destination, then the direction of motion of the contradiction changes. This change of direction could be opposite to the direction recently traversed, resulting in "dithering", meaning that the contradiction would re-traverse some of the same constraints, possibly returning to its original position before moving toward the newly preferred destination.
  • the nearness counts for the original destination and other destinations in the same path will be updated as the contradiction moves away from the point where it was revealed that the preferred destination is not most expeditiously reached along the original path.
  • any of the following strategies may be used: (1 ) explicitly indicating pseudo-assumptions that are illegitimate destinations, populating this indication at the time of making the counter-assertion that negates the precipitant for best efficiency, and allowing this indication to be recessively inherited by assertions that are led to and produced by the counter-assertion that identifies the teardrop in context, or (2) regularly comparing the value predicates for the same variable that are in the full reasons to re-identify when apparent pseudo-assumptions are not legitimate destinations, or (3) making a similar re-identification while back-tracking, or (4) modifying the method by adding a rule that the contradiction should not reverse direction unless all other possible directions of motion are restricted and those restrictions are fully supported by unconditional assertions, producing a method called Nearest Destination Ahead.
  • An explicit indication of an illegitimate destination is effectively a declaration that the pseudo- assumption will have a valid reason at any time when it is possible to counter-assert the term restricted by that value predicate within the currently recorded prevailing path and therefore it should not be treated as not having a valid reason even though a valid reason is not currently recorded.
  • the heritability of an explicit indication of an illegitimate destination should be recessive, meaning that if a first prevailing path has such an indication and a second prevailing path that is disjunctively converging or conjunctively converging with the first prevailing path does not have such an indication then the result should have no such indication.
  • the nearness count for an illegitimate destination should similarly be propagated recessively. Because the same term may appear to be an illegitimate destination in one sub- path and simultaneously appear to be a legitimate destination in another sub-path, when using backtracking to identify destinations it is necessary to keep a record of all values encountered during the search, which is best embodied by a history of elements that have been popped from the stack.
  • a method that moves a contradiction toward the nearest destination regardless of whether it is ahead or behind the most recent counter-assertion is called the Strictly Nearest Destination method.
  • a method that moves a contradiction in the direction in which a preferred destination appears nearest is called the Nearest Preferred Destination method, and there is also a Nearest Preferred Destination Ahead method.
  • Each of the methods listed are members of the class of Nearest Destination methods.
  • the Full Farthest Reversal method may include the following operations:
  • a destination is chosen for the motion of a given contradiction.
  • the manner of choosing is not important as long as the choice is legitimate and persistent. If it is revealed that the chosen destination is not in the paths that lead to the given contradiction, then another destination is chosen; but otherwise, the choice should persist as the contradiction moves through the constraints.
  • [0292] Copy the pruned co-basis for the main term as the "main basis", and eliminate the pruned co-basis for the main term.
  • the motion of contradictions may dither.
  • the number of dithers is limited by the number of constraints that may be contradicted or may provide an impetus for a change of direction of motion of an existing contradiction, and the maximum number of times a single constraint may be traversed by a contradiction in response to a dither is equal to the number of terms in that constraint, and a new set of dithers is possible whenever an assumption is introduced. Any method of choosing a direction in which to move a contradiction that limits the number of constraint traversals per dither to the number of terms in the constraint and limits the number of dithers per assumption to the number of constraints in the expression is an acceptable method.
  • a Farthest Reversal method works by consistently choosing a path that does not join the main path or joins the main path at the farthest possible point from the contradiction relative to distance as measured in the main path itself, and this prevents the motion of the contradiction from doubling-back on the main path and then redoubling-back except in cases where information about the path is lost or not previously available.
  • Nearest Destination methods may vary according to how nearness is measured, applying different ways of measuring farness to Farthest Reversal methods produces orderings of assertions in a prevailing path that are similar to one another.
  • a more substantial example of a variant of a Farthest Reversal method is one that uses stratified reasons.
  • a "stratified reason” is a kind of record of a prevailing path that is limited to constraints that provide prevailing assertions that have a specific assumption in their prevailing paths. These constraints are stratified in the sense that every constraint that produces an assertion as a result of the introduction of a first assumption may be a part of the stratified reason of another constraint in that same set, and every constraint that produces an assertion as a result of the introduction of the first assumption in combination with a second assumption may be a part of the stratified reason of another constraint in this latter set, and thus the constraints are separated into “strata” with each stratum being assigned to a specific latest assumption that is called the "source” for the assertions in its stratum.
  • a stratified reason is similar to a pruned co-basis as is described above, except that a pruned co-basis does not contain value predicates that represent restrictions from other strata and does not include paths that lead to pseudo-assumptions without also leading to the specified assumption through the same constraints, and except that stratified reasons do not have fulfilled counts, unfulfilled counts, or nearness counts but do contain prevalence numbers but the prevalence numbers are not revised to serve as rigorously maintained farness counts. As such, stratified reasons are part of the prior are where they are simply called "reasons".
  • Variants of Farthest Reversal methods may provide small reductions to the computational costs by finding a shorter path to the point of rejoining the main path or by preferring to choose a destination for which a short path to the point of rejoining the main path exists.
  • Nearest Destination methods require traveling minimum distances or traveling a path that is expected to incur minimal computational costs to expel a contradiction
  • the Farthest Reversal method requires traveling to a point that is earliest in the main path, regardless of the distance traveled or computational cost of traversing that distance, Nearest Destination methods will tend to incur lesser computational costs in order to expel a contradiction, providing Nearest Destination methods with advantages over certain alternatives.
  • One way to provide this adjustment is to associate the desired term to be counter- asserted, identified by the value predicate found in the full reason that restricts that term, with the contradiction in motion, efficiently embodied as a data structure associated with the process of resolving contradictions, rather than being associated with a variable, constraint, term, or assertion. More than one such process notation may be necessary per process, but the number of such notations cannot exceed the number of variables in the expression.
  • Embodiments of the present invention may be implemented in various ways. The choice of implementation for a particular substrate may depend on the implementational economies available to that substrate. Specifically, the production of devices typically trades a linear increase in computational time in order to save a squared cost of space for mechanisms, and the production of software often makes the opposite trade preferring to save computational time at the expense of additional memory usage.
  • One particular useful embodiment of the present invention which provides a low maximum computational cost, embodies a single-threaded dynamic variant that performs a Nearest Destination method of choosing a direction in which to move contradictions and stores compressed full reasons that include unfulfilled counts and maximum distance counts and restriction counts. The majority of the full reasons are best maintained rigorously, but the maximum distance counts and restriction counts are best maintained lazily, and SOMME value predicate revisions are best maintained lazily unless the present invention is supplemented by a process that provides conventional mathematical analysis.
  • Embodiments of the present invention use relationships between the constraints themselves to define the proximal space through which contradictions move. Consequently, the motion of contradictions is not affected by the nature of the values, whether they are well-ordered, partially-ordered, or disjoint, and whether they are mutually-exclusive or fuzzy; nor is this motion affected by the quality of the value predicates, whether they are intervals, sets, or discrete values; nor is this motion affected by the quality or shape of the extension of the constraints, whether it is continuous, bifurcated, or discrete, and whether it is convex, contiguous but non-convex, or non-contiguous, or there is no feasible extension at all.
  • the maximum computational expenditure of embodiments of the present invention is affected by the number of variables, the number of differentiated values of those variables, and the number of constraints; and because SOMMEs may operate on variables with an infinite number of values, the motion and maximum computational expenditure of embodiments of the present invention is affected by whether the constraints are disjunct phrases or other explicitly logical expressions or SOMMEs.
  • One embodiment of the present invention is a general improvement to computerized computation, providing a reduction in the costs of running the computational device while solving a problem in NP, NP-complete, or NP-hard, and a reduction in the amount of time that an operator of the computational device must wait for a result while solving a problem in NP, NP-complete, or NP-hard.
  • This embodiment of the present invention is comparable to a new arithmetic circuit in a calculator or to a software module that emulates such a circuit.
  • Embodiment #2 (Template Making)
  • One embodiment of the present invention is a device or automated process that renders templates that are used by another machine to cut parts from material or otherwise used by a machine to guide some processing of material into components of a product, whether the process is producing lumber from timber, clothing panels from cloth, leather, or plastic, or car or other machine parts from metal sheets, bars, or wire, or some other manufactured part from a refined material.
  • the technical effect of this embodiment is that templates are provided that permit optimal utilization of materials without excessive computational costs, which reduces waste of both material and computational costs.
  • This optimization typically uses variables and constraints that represent the geometric requirements of the parts to be rendered and may also include constraints that reflect the different economic values of parts that might be rendered from a particular piece of stock, as well as including constraints that summarize the utilization of materials and value of the product in order that a conservative variant of this embodiment of the present invention may force the production of a template that maximizes the utilization of stock or value produced.
  • constraints reflect the different values of parts, then an additional technical effect is the maximization of the value of the product.
  • Embodiment #3 (Cutting Machine Control)
  • One embodiment of the present invention is a part of the control mechanism of a cutting machine, drilling machine, grinding machine, or other machine that renders parts from stock material, whether the process being supplied by the machine is cutting lumber from timber, furniture parts from lumber, panels from cloth, leather, or plastic, or car or other machine parts from metal sheets, bars, or wire, or some other manufactured part from a refined material.
  • the technical effect of this embodiment is the control of the drills or cutting surfaces that provide optimal utilization of materials without excessive computational costs, which reduces waste of material, computational costs, and total cutting time.
  • This optimization typically uses variables and constraints that represent geometric requirements of the parts that are being rendered and may also include constraints that represent the different economic values of parts that might be rendered from a particular piece of stock, as well as including constraints that summarize the utilization of materials and value of the product in order that a conservative variant of this embodiment of the present invention may force a rendering of parts that maximizes the utilization of stock or value produced.
  • constraints reflect the different values of parts, then an additional technical effect is the maximization of the value of the product.
  • Embodiment #4 Robot Vehicle Control
  • One embodiment of the present invention is a part of the control mechanism of a robotic vehicle, allowing the vehicle to choose expedient paths to its destinations.
  • the technical effect of this embodiment is a minimization of travel time or cost, while reducing wait-times and computational costs associated with making the decisions that drive the vehicle.
  • This minimization typically uses variables and constraints that represent the geographic locations of destinations, the geographic paths between various positions, and physical or economic impediments associated with the various path segments, in addition to constraints that summarize the physical and economic impediments in order that a conservative variant of this embodiment of the present invention may force the choice of a path with a minimal travel time or cost.
  • One embodiment of the present invention is a device or automated process that compresses data, whether the data represents text, an image, an audio message, a video recording, an executable binary, or some other encrypted or non-encrypted unit of information, whether the data is digital or can be represented as a Fourier decomposition or other algebraic decomposition of analog data.
  • the technical effect of this embodiment is an optimization of the compression effect on a unit of information relative to the costs of computations that produce the compression.
  • This optimization typically uses variables and constraints that represent preferences about the elapsed time required to decompress the information and constraints that reflect computational costs and compressive benefits of various strategies for compression, in addition to constraints that represent a summarization of compression in order that a conservative variant of this embodiment of the present invention may force an optimally compressed result.
  • Embodiment #6 (Protein Design)
  • One embodiment of the present invention is a device or automated process that provides a sequence of amino acids that conforms to a given geometric structure.
  • the technical effect of this embodiment is a reduction of the time and computational expense associated with the production of custom proteins or models of custom proteins and a reduction in the wait-time for designers.
  • Such a device or automated process typically uses variables and constraints that represent the chemical limitations on amino acid positioning in a peptide, whether those limitations are based on hydrogen bonding, ionic interactions, Van der Waals forces, or hydrophobic packing, or other known or suspected chemical properties or environmental conditions, in addition to constraints that reflect the preferred three-dimensional shape of the protein in order that a dynamic variant of this embodiment of the present invention may produce a conforming sequence of amino acids.
  • Embodiment #7 (Telecom Traffic Routing)
  • One embodiment of the present invention is a device or automated process that optimizes the utility of a telecom network relative to cost by routing messages away from network congestion.
  • the technical effect of this embodiment is the optimization of the utility of the message routing capability of an existing telecom network while reducing wait-times and saving computational costs associated with providing that utility.
  • This optimization typically uses variables and constraints that represent the topology of the telecom network, measurements of congestion on the network, the utilitarian values of messages to be transmitted, and various costs of using and transmission speeds across various segments of the network, in addition to using constraints that summarize the costs and utility in order that a conservative variant of this embodiment of the present invention may force an optimal routing for the message load.
  • Embodiment #8 (Wavelength Division Multicasting Traffic Grooming)
  • One embodiment of the present invention is a device or automated process that produces an
  • ADM installation plan consisting of a list of wavelengths and a number of add-drop multiplexors (ADMs) per fiber that is optimal with respect to hardware cost or blocking probability.
  • the technical effect of this embodiment is the optimization of the WDM network to minimize the costs of constructing and maintaining the network or the probability of reaching a traffic-blocking condition, while saving computational costs associated with performing the optimization that results in the production of the list of wavelengths and number of ADMs.
  • This optimization typically uses variables and constraints that represent the available bandwidth of the transmission channel, the costs of optics, ADMs, and other components of the network, and possibly expected traffic demands, in addition to constraints that summarize the costs or blocking probability so that a conservative variant of this embodiment of the present invention may force an ADM installation plan that minimizes costs or blocking probability.
  • Embodiment #9 (Satellite Placement)
  • One embodiment of the present invention is a device or automated process that produces a placement specification for a set of orbital satellites that satisfies service arc requirements while minimizing the likelihood of communications interference and collision.
  • the technical effect of this embodiment is an optimization of the placement of satellites that provides a minimized cost composed of a combination of risk of destruction and degradation of service caused by communication interference, while saving computational costs associated with performing the optimization.
  • This optimization typically uses variables and constraints that represent orbital mechanics, the shell in which the set of satellites may be placed, the orbits of existing satellites and debris, the positions of base stations and other surface objects that define the value of the service arcs of each of the satellites, and the positioning costs for various locations in the shell, in addition to constraints that summarize the values and costs of the placement specification so that a conservative variant of this embodiment of the present invention may force the production of an optimal placement specification.
  • Embodiment #10 (Component Design)
  • One embodiment of the present invention is a device or automated process that produces a component design that minimizes the cost of labor and materials required to manufacture components that meet required physical specifications, whether those components are structural trusses, submarine propellers, electrical batteries, or any other kind of component.
  • the technical effect of this embodiment is the minimization of manufacturing costs of physical components, while saving computational costs associated with producing such a minimization and while saving the wait-time of component designers.
  • This minimization typically uses variables and constraints that represent the specifications of the physical requirements of the components, the available materials that may be used to construct the component and their stock specifications, the relationships that determine how the types of materials and their configuration affect the physical properties of the component, and the costs of altering stock material into parts and assembling them, in addition to constraints that summarize the costs in order that a conservative variant of this embodiment of the present invention may force a design that minimizes the manufacturing costs.
  • Embodiment #11 (Cryptanalysis)
  • One embodiment of the present invention is a device or automated process that finds multiplicative factors or inverts hashes that have been used to encrypt data.
  • the technical effect of this embodiment is the decomposition of a cypher-text into a plain-text, while saving computational costs associated with producing this decomposition.
  • Such a device or automated process typically uses variables and constraints that represent the cypher-text as well as representing known or suspected encryption algorithms that have been or may have been applied to the plain-text in order to produce the cypher-text in order that a dynamic variant of this embodiment of the present invention may produce clear-text.
  • Embodiment #12 (CPU Job Scheduling)
  • One embodiment of the present invention is a device or automated process that produces a schedule of jobs to be processed by a computer's central processing unit (CPU) that maximizes the throughput or responsiveness of the CPU under a given workload or minimizes the energy usage.
  • CPU central processing unit
  • the technical effect of this embodiment is the maximization of throughput or responsiveness of the CPU or minimization of the energy usage, while saving computational costs associated with producing the schedule, which in turn provides an additional improvement to the throughput or responsiveness of the CPU.
  • Such a device or automated process typically uses variables and constraints that represent the jobs to be executed and their urgency, the sub-steps of the jobs and their order, the resources required for each sub-step, and the resources available to the CPU, in addition to constraints that summarize the energy used or measurements that reflect the responsiveness or throughput of the CPU when executing the schedule of jobs so that a conservative variant of this embodiment of the present invention may force a maximization of throughput or responsiveness or a minimizations of energy use.
  • Embodiment #13 (IC Test Bus Development)
  • One embodiment of the present invention is a device or automated process that produces a design for an on-chip test access architecture or test access mechanism (TAM) for a system-on-chip (SOC) or other complex integrated-circuit chip (IC) that includes a test bus, where this design includes an assignment of cores to test buses, the widths of the test buses and their subdivisions, and a schedule of tests.
  • TAM on-chip test access architecture or test access mechanism
  • SOC system-on-chip
  • IC complex integrated-circuit chip
  • the technical effect of this embodiment is an optimization of the test bus that provides a maximization of the testing utility value relative to the construction costs of the test bus, while saving computational costs associated with performing the optimization.
  • This optimization typically uses variables and constraints that represent the cores and their input pins, the various tests required and their core pin access requirements, the times to complete the various tests, the value of reduced testing time, and the costs of increasing test bus widths, in addition to constraints that summarize the value of testing time required by the schedule of tests and the costs of constructing the buses in order that a conservative variant of this embodiment of the present invention may force an optimization of the testing utility value relative to the construction costs of the test bus.
  • Embodiment #14 (IC Circuit Partitioning, Floorplanninq, & Placement)
  • One embodiment of the present invention is a device or automated process that produces a circuit layout that separates a logically-defined complex behavior into multiple modules, circuit cores, cells, or blocks suitable for positioning as part of an IC, where the layout satisfies size limitations or limitations on the number or size of interconnects between the circuit cores, cells, or blocks that in turn may provide a circuit delay that is within desired limits.
  • the technical effect of this embodiment is a partitioning of the circuit that satisfies the size and circuit delay limitations, while saving computational costs associated with producing the circuit layout.
  • Such a device or automated process typically uses variables and constraints that represent the logical behavior of the circuit, the possible translations of individual logical behaviors into sub-circuits, the sizes and circuit delays of the various sub-circuits, including limitations on juxtaposition of various sub-circuit components caused by the geometry of the chip and various electrical effects, the limitations on the partition sizes and circuit delays, and a summarization of the sizes and delays of the circuit layout in order that a dynamic variant of this embodiment of the present invention may produce a satisfying layout.
  • the constraints used by such a device or automated process may also represent costs of construction and a formula that provides a trade-off between costs and performances in order that a conservative variant of this embodiment of the present invention may force a circuit layout that provides an optimization of the trade-off.
  • Embodiment #15 (IC Power, Ground, Clock, & Netlist Routing)
  • One embodiment of the present invention is a device or automated process that produces a wiring plan for an IC, whether that plan includes routing for power pins, ground pins, clock signal pins, or connecting input and output pins for the various cores, cells, or blocks of the IC, where the plan satisfies limitations on the length and width of interconnects between the cores, cells, or blocks so that the interconnects do not exceed the available space on the IC and circuit delay limitations for the IC are not violated.
  • the technical effect of this embodiment is the production of a wiring plan that satisfies size and circuit delay limitations, while saving computational costs associated with producing the wiring plan.
  • a device or automated process typically uses variables and constraints that represent the various cores, cells, or blocks and their shapes and pins, the list of connections between the output pins of each core, cell, or block to the required input pins on other cores, cells, or blocks, the list of connections of chip input pins to core, cell, or block input pins, limitations on the sizes of interconnects that are due to the geometry of the chip size and fabrication processes, limitations on juxtaposition of interconnects that are due to electrical effects such as capacitive coupling or inductive cross-talk, and the possibility of implementing clock closure techniques such as extra-wide interconnects and cloning modules, in addition to constraints that summarize the space consumed by the cores, cells, or blocks and possibly the signal delay of clock circuits in order that a dynamic variant of the present invention may force a wiring plan that satisfies the space and signal delay requirements.
  • Embodiment #16 (Advanced IC Fabrication)
  • One embodiment of the present invention is a device or automated process that produces masks for IC fabrication that satisfy size and performance requirements and a list of fabrication process that should be applied in combination with the masks in order to directly produce an IC that satisfies behavioral specifications.
  • the technical effect of this embodiment is a greatly streamlined IC design process that, while theoretically possible without the present invention, only becomes practical because of the computational cost savings provided by the present invention.
  • Such a device or automated process typically uses variables and constraints that represent all the technical limitations of IC fabrication in general, the specific limitations of the proposed fabrication facility, geometrical limitations of the various wafer sizes on which the IC may be created, coding requirements for producing the masks themselves, whether the masks are for deposition, removal, patterning, or modification of electrical properties, the desired functional behavior of the IC, required tests for the IC behavior, various implementations of components that provide identical functional behavior but differ in their electrical, magnetic, or signal propagation properties, in addition to constraints that summarize the size and performance characteristics of the IC in order that a dynamic variant of the present invention may force the production of masks and process applications that satisfy the behavioral, size, and performance requirements.
  • variables and constraints used by such a device or automated process may also represent the costs of the various component implementations, the expected value and market demand of the IC for various size and performance ranges, costs of new IC fabrication start-up, in addition to constraints that summarize the costs and market value of an IC design in order that a conservative variant of this embodiment of the present invention may force the production of masks and process applications that optimize the cost of the IC relative to expected market value and demand.
  • Embodiment #17 (Control System Design)
  • One embodiment of the present invention is a device or automated process that produces a design of a control system, such as a nuclear reactor control system, or a control system for a forge, or any other system that controls a complex process.
  • a control system such as a nuclear reactor control system, or a control system for a forge, or any other system that controls a complex process.
  • the technical effect of this embodiment is the production of an optimal design, while saving computational costs associated with producing the optimization and while saving the wait-time of designers.
  • This optimization typically uses variables and constraints that represent the available control elements, including their costs and effects, and a characterization of the control problem, including acceptable tolerances for the precision of control, in addition to constraints that summarize the cost or the precision in order that a conservative variant of this embodiment of the present invention may force a design that is optimized for cost or precision.
  • Embodiment #18 Robot Inverse Kinematics
  • One embodiment of the present invention is a device or automated process that produces a set of instructions that guide the movement of a robot so that it achieves a specified position while traversing a field of obstacles.
  • the technical effect of this embodiment is the production of the set of robotic instructions, while saving computational costs associated with producing the set of instructions and while reducing the time to bring the instructions to production.
  • a device or automated process typically uses variables and constraints that represent the desired destination position, the dimensions and positions of obstacles to be avoided, the dimensions and starting position of the robot, the possible motions of the robot, including the resultant change in position or dimensions of the robot and the cost of each motion, in addition to constraints that summarize the cost of the motion in order that a conservative variant of this embodiment of the present invention may force a set of instructions that result in motions that achieve the desired destination position with the least cost.
  • One embodiment of the present invention is a device or automated process that compiles software source code into machine code, whether the support is for register allocation, instruction selection, macro compression, loop optimization, data layout optimization, code parallelization, or any other complex compilation process.
  • the technical effect of this embodiment is the production of aggressively optimized machine code, while saving computational costs associated with the optimization and while saving the wait-time of code developers.
  • This optimization typically uses variables and constraints that represent the source code, the available registers, including their sizes, the available operations, including their computational costs and any specific register assignments, the available spill resources, including their sizes and computational costs of access, and tilings that map source code instructions to sets of machine instructions, in addition to constraints that summarize the computational costs in order that a conservative variant of this embodiment of the present invention may force the production of machine code that satisfies the source code and has minimal computational costs.
  • FIG. 2 a flowchart is shown of a method 200 performed by a computer system implemented according to one embodiment of the present invention.
  • the method 200 moves contradictions through a proximal space defined by a rhizomatic network that consists of prevailing paths of implication responsive to counter-asserting value predicates (Figure 2, operation 202).
  • the counter- assertions are assertions of value predicates that negate other assertions, which causes the prevailing paths of negated assertions to be moved from the prevailing paths of remaining assertions.
  • the remaining assertions include the counter-assertions.
  • the method 200 also produces counter-asserted value predicates that do not create a contradiction in any constraint that remains in the prevailing path of the counter-assertion ( Figure 2, operation 204).
  • the method 200 also collects first data representing the prevailing paths of implication and the prevailing paths of motion of contradictions ( Figure 2, operation 206).
  • the method 1700 also uses the first data to inform choices of direction so that contradictions move toward locations in the proximal space where no validly reasoned disagreement is recorded ( Figure 2, operation 208).
  • the method 200 also chooses contradictions to be resolved and terms to be counter-asserted in a way that excludes dithering ( Figure 2, operation 210).
  • any of the functions disclosed herein may be implemented using means for performing those functions. Such means include, but are not limited to, any of the components disclosed herein, such as the computer-related components described below.
  • the techniques described above may be implemented, for example, in hardware, one or more computer programs tangibly stored on one or more computer-readable media, firmware, or any combination thereof.
  • the techniques described above may be implemented in one or more computer programs executing on (or executable by) a programmable computer including any combination of any number of the following: a processor, a storage medium readable and/or writable by the processor (including, for example, volatile and non-volatile memory and/or storage elements), an input device, and an output device.
  • Program code may be applied to input entered using the input device to perform the functions described and to generate output using the output device.
  • Each computer program within the scope of the claims below may be implemented in any programming language, such as assembly language, machine language, a high-level procedural programming language, or an object-oriented programming language.
  • the programming language may, for example, be a compiled or interpreted programming language.
  • Each such computer program may be implemented in a computer program product tangibly embodied in a machine-readable storage device for execution by a computer processor.
  • Method steps of the invention may be performed by one or more computer processors executing a program tangibly embodied on a computer-readable medium to perform functions of the invention by operating on input and generating output.
  • Suitable processors include, by way of example, both general and special purpose microprocessors.
  • the processor receives (reads) instructions and data from a memory (such as a read-only memory and/or a random access memory) and writes (stores) instructions and data to the memory.
  • Storage devices suitable for tangibly embodying computer program instructions and data include, for example, all forms of non-volatile memory, such as semiconductor memory devices, including EPROM, EEPROM, and flash memory devices; magnetic disks such as internal hard disks and removable disks; magneto-optical disks; and CD-ROMs. Any of the foregoing may be supplemented by, or incorporated in, specially-designed ASICs (application-specific integrated circuits) or FPGAs (Field- Programmable Gate Arrays).
  • a computer can generally also receive (read) programs and data from, and write (store) programs and data to, a non-transitory computer-readable storage medium such as an internal disk (not shown) or a removable disk.
  • Any data disclosed herein may be implemented, for example, in one or more data structures tangibly stored on a non-transitory computer-readable medium. Embodiments of the invention may store such data in such data structure(s) and read such data from such data structure(s).

Landscapes

  • Engineering & Computer Science (AREA)
  • Physics & Mathematics (AREA)
  • Theoretical Computer Science (AREA)
  • General Physics & Mathematics (AREA)
  • Mathematical Physics (AREA)
  • Data Mining & Analysis (AREA)
  • General Engineering & Computer Science (AREA)
  • Software Systems (AREA)
  • Mathematical Optimization (AREA)
  • Mathematical Analysis (AREA)
  • Pure & Applied Mathematics (AREA)
  • Computational Mathematics (AREA)
  • Evolutionary Computation (AREA)
  • Databases & Information Systems (AREA)
  • Artificial Intelligence (AREA)
  • Computational Linguistics (AREA)
  • Algebra (AREA)
  • Computing Systems (AREA)
  • Operations Research (AREA)
  • Information Retrieval, Db Structures And Fs Structures Therefor (AREA)
  • Complex Calculations (AREA)
  • Computer Hardware Design (AREA)
  • Peptides Or Proteins (AREA)
  • Debugging And Monitoring (AREA)
  • Stored Programmes (AREA)
  • Architecture (AREA)
  • Measuring Or Testing Involving Enzymes Or Micro-Organisms (AREA)
  • Geometry (AREA)
  • Devices For Executing Special Programs (AREA)

Abstract

Parmi les problèmes de satisfaction ou toute décision ou autre problème qui peut être réduit à un problème de satisfaction, l'invention détecte les chemins le long desquels se propagent des implications et identifie les contradictions conditionnelles et ramène alors les contradictions au début des chemins d'implication vers des hypothèses ou autres assertions non raisonnées afin de rejeter les contradictions. L'action est terminée en moins de temps qu'avec les procédés existants et, par conséquent, l'invention apporte une amélioration des performances des dispositifs, logiciel, ou procédés qui abordent de tels problèmes. De tels problèmes sont abordés par des dispositifs, logiciel et procédés liés à de nombreux domaines techniques, notamment : le raffinage de minerai ; le tracé de canalisations ; la fabrication de fils ; la coupe de tissus ; le sciage ; la conception de composants mécaniques ; la conception structurale de systèmes de traitement de données ; la conception et l'analyse de circuits ou de masques à semi-conducteurs ; l'inspection et la protection de conteneurs, de tuyaux, et de galeries ; des opérations de réseaux de capteurs ; des opérations de satellites orbitaux ; la compression de données ; des analyses chimiques ; la conception et l'analyse de protéines.
PCT/US2015/022377 2010-06-25 2015-03-25 Résolution de problèmes non déterministes polynomiaux complets sans coût hyper polynomial WO2015148599A1 (fr)

Priority Applications (10)

Application Number Priority Date Filing Date Title
KR1020167011170A KR102341689B1 (ko) 2014-03-25 2015-03-25 하이퍼-다항식 비용 없이 np-완전 문제들을 풀이하는 것
CA2943044A CA2943044C (fr) 2014-03-25 2015-03-25 Resolution de problemes non deterministes polynomiaux complets sans cout hyper polynomial
CN201580002451.1A CN105745618A (zh) 2014-03-25 2015-03-25 在无超高多项式成本的情况下求解np完全问题
SG11201606976PA SG11201606976PA (en) 2014-03-25 2015-03-25 Solving np-complete problems without hyper polynomial cost
JP2016526262A JP6550384B2 (ja) 2014-03-25 2015-03-25 ハイパー多項式コストなしでｎｐの問題を解決するための方法及びコンピューティング装置
EP15768263.4A EP3123302A4 (fr) 2014-03-25 2015-03-25 Résolution de problèmes non déterministes polynomiaux complets sans coût hyper polynomial
US15/126,227 US10528868B2 (en) 2010-06-25 2015-03-25 Solving NP-complete problems without hyper polynomial cost
AU2015236144A AU2015236144B2 (en) 2014-03-25 2015-03-25 Solving NP-complete problems without hyper polynomial cost
MYPI2016703394A MY184777A (en) 2014-03-25 2015-03-25 Solving np-complete problems without hyper polynomial cost
IL247866A IL247866B (en) 2014-03-25 2016-09-18 Solving np-complete problems without hyper-polynomial cost

Applications Claiming Priority (2)

Application Number Priority Date Filing Date Title
US201461970291P 2014-03-25 2014-03-25
US61/970,291 2014-03-25

Publications (1)

Publication Number Publication Date
WO2015148599A1 true WO2015148599A1 (fr) 2015-10-01

Family

ID=54196327

Family Applications (1)

Application Number Title Priority Date Filing Date
PCT/US2015/022377 WO2015148599A1 (fr) 2010-06-25 2015-03-25 Résolution de problèmes non déterministes polynomiaux complets sans coût hyper polynomial

Country Status (10)

Country Link
EP (1) EP3123302A4 (fr)
JP (1) JP6550384B2 (fr)
KR (1) KR102341689B1 (fr)
CN (1) CN105745618A (fr)
AU (1) AU2015236144B2 (fr)
CA (1) CA2943044C (fr)
IL (1) IL247866B (fr)
MY (1) MY184777A (fr)
SG (1) SG11201606976PA (fr)
WO (1) WO2015148599A1 (fr)

Cited By (3)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
WO2018086761A1 (fr) * 2016-11-10 2018-05-17 Rowanalytics Ltd Appareil de commande et procédé de traitement d'entrées de données dans des dispositifs informatiques s'y rapportant
US10528868B2 (en) 2010-06-25 2020-01-07 Clayton Gillespie Solving NP-complete problems without hyper polynomial cost
US11881287B2 (en) 2016-11-10 2024-01-23 Precisionlife Ltd Control apparatus and method for processing data inputs in computing devices therefore

Families Citing this family (4)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN110914840B (zh) * 2017-07-19 2023-06-16 国立大学法人横浜国立大学 解探索设备及程序
US10503507B2 (en) * 2017-08-31 2019-12-10 Nvidia Corporation Inline data inspection for workload simplification
CN111159631B (zh) * 2019-12-31 2023-08-11 中国人民解放军国防科技大学 一种基于可编程逻辑的硬件sat求解器
CN117172473A (zh) * 2023-09-04 2023-12-05 晞德求索(北京)科技有限公司 基于动态分配的一维下料方法和装置

Citations (8)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US6038392A (en) * 1998-05-27 2000-03-14 Nec Usa, Inc. Implementation of boolean satisfiability with non-chronological backtracking in reconfigurable hardware
US20070005523A1 (en) * 2005-04-12 2007-01-04 Eagleforce Associates, Inc. System and method for evidence accumulation and hypothesis generation
US20090192968A1 (en) * 2007-10-04 2009-07-30 True Knowledge Ltd. Enhanced knowledge repository
US20100269078A1 (en) * 2009-04-17 2010-10-21 Synopsys, Inc. Automatic approximation of assumptions for formal property verification
US20110307435A1 (en) * 2010-05-14 2011-12-15 True Knowledge Ltd Extracting structured knowledge from unstructured text
US20120220276A1 (en) * 2010-02-16 2012-08-30 Thaddeus John Kobylarz Application of the invoke facility service to restrict invocation of compound wireless mobile communication services
US20130283236A1 (en) * 2012-04-23 2013-10-24 Ecole Polytechnique Federale De Lausanne (Epfl) Advantageous State Merging During Symbolic Analysis
US8577825B2 (en) * 2008-01-29 2013-11-05 Clayton Gillespie System, method and device for solving problems in NP without hyper-polynomial cost

Family Cites Families (5)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US7356519B1 (en) * 2003-02-28 2008-04-08 Cadence Design Systems, Inc. Method and system for solving satisfiability problems
WO2009097290A2 (fr) * 2008-01-29 2009-08-06 Clayton Gillespie Système de traitement de données permettant de résoudre des problèmes np sans coût hyperpolynômial
CN101848229B (zh) * 2009-03-24 2014-06-25 北京理工大学 一种解决分布式网络计算中最小生成网络问题的方法
JP2012003733A (ja) * 2010-06-12 2012-01-05 Koji Kobayashi 論理式変換プログラム、及びｓａｔ解法プログラム
CN102063643B (zh) * 2010-12-13 2014-07-30 北京航空航天大学 一种基于dna计算的智能优化仿真方法

Patent Citations (8)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US6038392A (en) * 1998-05-27 2000-03-14 Nec Usa, Inc. Implementation of boolean satisfiability with non-chronological backtracking in reconfigurable hardware
US20070005523A1 (en) * 2005-04-12 2007-01-04 Eagleforce Associates, Inc. System and method for evidence accumulation and hypothesis generation
US20090192968A1 (en) * 2007-10-04 2009-07-30 True Knowledge Ltd. Enhanced knowledge repository
US8577825B2 (en) * 2008-01-29 2013-11-05 Clayton Gillespie System, method and device for solving problems in NP without hyper-polynomial cost
US20100269078A1 (en) * 2009-04-17 2010-10-21 Synopsys, Inc. Automatic approximation of assumptions for formal property verification
US20120220276A1 (en) * 2010-02-16 2012-08-30 Thaddeus John Kobylarz Application of the invoke facility service to restrict invocation of compound wireless mobile communication services
US20110307435A1 (en) * 2010-05-14 2011-12-15 True Knowledge Ltd Extracting structured knowledge from unstructured text
US20130283236A1 (en) * 2012-04-23 2013-10-24 Ecole Polytechnique Federale De Lausanne (Epfl) Advantageous State Merging During Symbolic Analysis

Non-Patent Citations (4)

* Cited by examiner, † Cited by third party
Title
ABITEBOUL ET AL.: "Deduction in the Presence of Distribution and Contradictions.", WEBDB, May 2012 (2012-05-01), Scottsdale, United States, XP055227591, Retrieved from the Internet <URL:https://hal.inria.fr/hal-00809300/file/p5.pdf> [retrieved on 20150813] *
GRIFFIN ET AL.: "An Algorithm for Constructing and Searching Spaces of Alternative Hypotheses.", IEEE TRANSACTIONS ON SYSTEMS, MAN, AND CYBERNETICS?PART B: CYBERNETICS, vol. 41, no. 3, June 2011 (2011-06-01), XP011408990, Retrieved from the Internet <URL:http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=5659971&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F3477%2F5767816%2F05659971.pdf%3Famumber%3D5659971> [retrieved on 20150813] *
JOHNSON ET AL.: "A Polynomial Algorithm for the Source Location Problem in Digraphs.", CDAM RESEARCH REPORT LSE-CDAM-2004- 02., February 2004 (2004-02-01), XP055227590, Retrieved from the Internet <URL:http://www.cdam.lse.ac.uk/Reports/Files/cdam-2004-02.pdf> [retrieved on 20150813] *
See also references of EP3123302A4 *

Cited By (4)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US10528868B2 (en) 2010-06-25 2020-01-07 Clayton Gillespie Solving NP-complete problems without hyper polynomial cost
WO2018086761A1 (fr) * 2016-11-10 2018-05-17 Rowanalytics Ltd Appareil de commande et procédé de traitement d'entrées de données dans des dispositifs informatiques s'y rapportant
US10948887B2 (en) 2016-11-10 2021-03-16 Precisionlife Ltd Control apparatus and method for processing data inputs in computing devices therefore
US11881287B2 (en) 2016-11-10 2024-01-23 Precisionlife Ltd Control apparatus and method for processing data inputs in computing devices therefore

Also Published As

Publication number Publication date
SG11201606976PA (en) 2016-09-29
JP6550384B2 (ja) 2019-07-24
CA2943044C (fr) 2023-05-16
IL247866B (en) 2021-05-31
CA2943044A1 (fr) 2015-10-01
EP3123302A1 (fr) 2017-02-01
JP2017513076A (ja) 2017-05-25
MY184777A (en) 2021-04-21
IL247866A0 (en) 2016-11-30
CN105745618A (zh) 2016-07-06
KR20160136270A (ko) 2016-11-29
EP3123302A4 (fr) 2017-12-20
AU2015236144A1 (en) 2016-11-03
KR102341689B1 (ko) 2021-12-20
AU2015236144B2 (en) 2020-04-30

Similar Documents

Publication Publication Date Title
AU2015236144B2 (en) Solving NP-complete problems without hyper polynomial cost
US10528868B2 (en) Solving NP-complete problems without hyper polynomial cost
Shoukry et al. SMC: Satisfiability modulo convex optimization
CN104603784A (zh) 相对定时表征
Bos et al. Formal specification and analysis of industrial systems
EP3903180A1 (fr) Code d&#39;automatisation de grande taille
Benelallam et al. Efficient model partitioning for distributed model transformations
Finger et al. Metatem at work: Modelling reactive systems using executable temporal logic
Luque et al. Parallel genetic algorithms
Margaria et al. Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change: 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part I
Lee et al. Implication of Optimizing NPU Dataflows on Neural Architecture Search for Mobile Devices
Kwon Machine Learning for AI-Augmented Design Space Exploration of Computer Systems
Martin Genetic programming in hardware
Neubauer Model-based symbolic design space exploration at the electronic system level: a systematic approach
Wu et al. PaRS: Parallel and near-optimal grid-based cell sizing for library-based design
Koutsoukos et al. Computational issues in intelligent control: Discrete-event and hybrid systems
Roozbehani Optimization of Lyapunov invariants in analysis and implementation of safety-critical software systems
Fodor et al. Transaction logic with defaults and argumentation theories
JP2005085112A (ja) 情報分類システム及びプログラム
Duan Extended Moore machine network model for discrete event control of flexible manufacturing systems
Incer et al. Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and Design
Ziegler et al. The Interplay of Online and Offline Machine Learning for Design Flow Tuning
Thomas Developing Fpgas as an Acceleration Platform for Data-Intensive Applications
Mahdoum CAD of Circuits and Integrated Systems
Miroshnik et al. Solving of SAT-Problems of artificial intelligence with the help of local elimination algorithms

Legal Events

Date Code Title Description
121 Ep: the epo has been informed by wipo that ep was designated in this application

Ref document number: 15768263

Country of ref document: EP

Kind code of ref document: A1

ENP Entry into the national phase

Ref document number: 2016526262

Country of ref document: JP

Kind code of ref document: A

ENP Entry into the national phase

Ref document number: 20167011170

Country of ref document: KR

Kind code of ref document: A

REEP Request for entry into the european phase

Ref document number: 2015768263

Country of ref document: EP

WWE Wipo information: entry into national phase

Ref document number: 2015768263

Country of ref document: EP

WWE Wipo information: entry into national phase

Ref document number: 15126227

Country of ref document: US

ENP Entry into the national phase

Ref document number: 2943044

Country of ref document: CA

WWE Wipo information: entry into national phase

Ref document number: 247866

Country of ref document: IL

NENP Non-entry into the national phase

Ref country code: DE

ENP Entry into the national phase

Ref document number: 2015236144

Country of ref document: AU

Date of ref document: 20150325

Kind code of ref document: A