Data processing: artificial intelligence – Neural network – Learning task
Reexamination Certificate
2000-03-08
2003-04-29
Davis, George B. (Department: 2121)
Data processing: artificial intelligence
Neural network
Learning task
C706S021000
Reexamination Certificate
active
06556978
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Field of the Invention
This invention pertains in general to Boolean satisfiability algorithms and in particular to an improvement in the searching steps inherent in such algorithms.
2. Description of Related Art
The last few years bave seen extraordinary improvements in the effectiveness of general-purpose Boolean satisfiability (SAT) algorithms. This work began with the application of the Walk-SAT (WSAT) algorithm to “practical” problems in a variety of domains, such as generative planning and circuit layout, by translating the problems into propositional logic and then solving them using WSAT.
Although WSAT is unchallenged in its ability to find models for randomly generated satisfiable theories, systematic methods have closed the gap on theories corresponding to practical problems. The algorithm of choice appears to be Relevance-bounded Learning (RELSAT), an extension of an idea from dynamic backtracking. RELSAT is systematic and can therefore deal with both satisfiable and unsatisfiable theories; for theories arising from practical problems, its performance is comparable to that of WSAT.
The applicability of propositional algorithms to practical problems is anything but straightforward, however. As the problems become more interesting, the problems' sizes grow enormously due primarily to occurrences of constraint axioms containing universally quantified parameters. A single axiom such as
∀
xyz. [a
(
x,y
)&Lgr;
b
(
y,z
)→
c
(
x,z
)] (1)
has d
3
ground instances if d is the size of the domain from which x, y and z are taken. The prior art has dealt with this difficulty by increasing computer memory and by finding clever axiomatizatidns for which ground theories remain manageably sized. In general, memory and cleverness are both scarce resources and a more natural solution is desired.
BRIEF SUMMARY OF THE INVENTION
The above needs are met by a method, computer program product, and computer system for using a procedure, such as a search procedure, to solve a constraint problem. The method, computer program product, and computer system, according to embodiments of the present invention, define a set of constraints for the constraint problem. The set of constraints includes one or more lifted constraints with universally quantified parameters. The procedure is formulated in terms of subsearch problems on the one or more lifted constraints. A search procedure, such as WSAT or Davis-Putnam, searches for a satisfying assignment and encounters the subsearch problems. Then, intelligent subsearch is used to answer the subsearch problems. Intelligent subsearch includes using backtracking searches to find relevant assignments to the universally quantified parameters within the one or more lifted constraints. One embodiment of the present invention performs intelligent subsearch on each lifted constraint and merges the results. From the results of the intelligent subsearch, it is possible to supply the information needed by the search procedure to make its decisions. The goal of the search procedure is to find an assignment Q satisfying the defined set of constraints.
One embodiment of the present invention formulates the search procedure in terms of subsearch problems on S(C,P,u,s), where S(C,P,u,s) represents a subset of grounded clauses that would be obtained by grounding a set of clauses C obtained from the defined set of constraints for the constraint problem and restricting the subset of clauses having u literals unvalued by an assignment P and s literals satisfied by the assignment P. In alternative embodiments, C can be the set of one or more lifted clauses, a set of clauses in a set of possibly lifted clauses produced using a literal 1, clauses learned by a search procedure, and clauses learned by the search procedure and restricted using a literal l.
In one embodiment of the present invention, at least one lifted constraint is a pseudo-Boolean constraint.
REFERENCES:
patent: 5636328 (1997-06-01), Kautz et al.
patent: 6031984 (2000-02-01), Walser
Folino et al, “Combining Cellular Genetic Algorithm and Local Search for Solving Statisfiability Problems”, IEEE Conference on Tools with Artificial Intelligence, Nov. 1998.*
Nemer et al., “A Non-Deterministic Scheduling and Allocation Model for Mapping Algorithm on Configurable Architectures”, IEEE Conference on Electrical and Computer Engineering, May 1997.*
Kautz, H. et al., “Planning as Satisfiability,” Proceedings of the 10thEuropean Conference on Artificial Intelligence (ECAI 92), Vienna, Austria, Aug. 1992. 1-12.
Sebastiani, R., “Applying GSAT to Non-Clausal Formulas,” J. Artificial Intelligence Research 1 (1994) 309-314.
Selman, B. et al., “Local Search Strategies for Satisfiability Testing,” Second DIMACS Challenge on Cliques, Coloring, and Satisfiability, Oct. 1993 1-17.
Selman, B. et al., “Noise Strategies for Improving Local Search,” Proceedings of AAAI-94, Seattle, WA, Jul. 1994, 7 pp.
Papadimitriou, “On Selecting a Satisfying Truth Assignment,”Proc. 1991 FOCS, IEEE Computer Society Press, pp. 163-169.
Ginsberg Matthew L.
Parkes Andrew J.
Davis George B.
Fenwick & West LLP
The State of Oregon acting by and through the State Board of Hig
LandOfFree
Satisfiability algorithms and finite quantification does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Satisfiability algorithms and finite quantification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Satisfiability algorithms and finite quantification will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3109511