Relating Search Abstractions to Actual Search

From International Center for Computational Logic
Toggle side column

Relating Search Abstractions to Actual Search

Topic no longer available
Modern SAT solver are highly complex systems with many integrated techniques and heuristics. To make this technology available for teaching, we developed an abstraction: finding an exit in a maze. The task of this project is to find example formulas that are related to the special situations in the maze, such that a SAT solver behaves exactly like the agent in the maze.