Comments (8)
I am very much in favour of this. Both imperfect indexing and unification (or maybe some unification-like thing - UWA?) can be implemented very efficiently and concisely, but perfect indexing is much trickier. I'm also not convinced that perfect indexing pays off.
It would be interesting to try replacing these with fewer indices that contain more terms each. Inferences then share indices and carry out post-procesing to filter out unwanted terms.
Could you expand on this a little? Maybe an example? I think there's two separate things to try here:
- imperfect indexing techniques like discrimination trees
- coalescing multiple indices into one and filtering out unwanted items
I think both are worth exploring, to be clear.
from vampire.
Do we know of some papers evaluating indexing techniques in the past? Let's avoid common pitfalls and not try to reinvent the wheel ;)
from vampire.
I am not suggesting abandoning substitution trees. The suggestion is to combine similar indices (your #2). For example, instead of having a substitution tree that indexes only left-hand sides for demodulation, and another that indexes only left-hand sides for superposition, we have a tree that contains both sets of terms.
When performing a query on the index from demodulation, we may receive extra left-hand sides (those suitable for superposition, not demodulation) which will then need filtering out.
Looking into discrimination trees and other techniques is also interesting, but an even more radical departure from the current code base.
from vampire.
The suggestion, is to combine similar indices (your #2). For example, instead of having a substitution tree that indexes only left-hand sides for demodulation, and another that indexes only left-hand sides for superposition, we have a tree that contains both sets of terms.
I see. This seems like a good idea. My only concern is that the performance win from combining indices (mostly spatial locality and reduced index maintenance, right?) will be lost by increased query time resulting a larger index. But it's worth a try!
from vampire.
Do we know of some papers evaluating indexing techniques in the past? Let's avoid common pitfalls and not try to reinvent the wheel ;)
Here are a couple:
https://www.sciencedirect.com/science/articl/pii/B978044450813350028X?via%3Dihub
https://link.springer.com/content/pdf/10.1007/3-540-45744-5_18.pdf
from vampire.
And of course:
https://people.mpi-inf.mpg.de/~hillen/compit/evaluation.pdf
from vampire.
from vampire.
from vampire.
Related Issues (20)
- Suboptimal job distribution on multicore HOT 4
- Join the two mechanisms that do "Unification with abstraction" around in substitution trees HOT 1
- Possible issue in substitution trees - check whether _nextVar really needs to keep growing forever HOT 3
- A bug with fmbswo was fixed by disabling the option
- Sorts in FMB are unsigned
- FMB max sort size detection via X = t_1 | ... | X = t_n HOT 4
- smt2 input not satisfiable, but preprocessed & fixed up input is HOT 7
- Parse errors for polymorphic problems HOT 4
- Skolem type in same block as term causes assertion violation. HOT 10
- Hey
- Hey
- Question about bitvector HOT 2
- Question answering HOT 10
- Lost sort information in quantifier blocks causes problems later.
- RobSubstitution::match is unsound HOT 4
- Time-out with satisfiable problems in SMT-LIB2 HOT 2
- `(expt 2 8)` induction? HOT 7
- Polymorphism and Z3 not playing nicely HOT 5
- Incorrect saturations for problems containing FOOL HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from vampire.