Skip to content

plotnick/minuet

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

48 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Minuet: An Answer Set Programming System

🎼 Minuet is an early-stage (not yet α quality) Answer Set Programming (ASP) system, roughly similar to (a small subset of) clingo. It takes as input a logic program, expressed in either a modern, Python-inspired syntax or (eventually) the ASP-Core-2 syntax, grounds it, and computes the stable models (aka "answer sets"), which are like the solutions to a Prolog query. The program is expressed as a set of rules that may include disjunctive heads, choice rules, aggregates, etc. See the resources at Potassco or Lifschitz's book for a thorough introduction to answer set programming.

The program may be parsed from a string as usual, or (for the native Minuet syntax only) embedded in Rust code via a procedural macro that parses it at Rust compile-time. The proc macro preserves input spans, so parse errors in your embedded Minuet programs can often be precisely indicated by your IDE via rust-analyzer.

After parsing, the program is grounded, in which all variables are replaced with the constant values that they may be bound to. This is currently the weakest part of Minuet: it grounds using the most naïve strategy possible (viz., bind every variable to every possible constant), which severely limits the size and kinds of logic programs that it can handle. A new grounder based on Kaminski & Schaub is in progress as of June 2024.

After grounding, a few other meaning-preserving preprocessing steps are performed to bring the program into a useful normal form, and then it is compiled into an exact cover problem (again, naïvely; lots of low hanging fruit there, too) and handed off to the solver to generate solutions, which are checked for model stability and finally translated back into answer sets. This effectively "evaluates" the original logic program, but without anything resembling a traditional evaluator in sight.

The solver is implemented using Don Knuth's beautiful Dancing Cells exact cover algorithm, a sort of sequel to his original Dancing Links. It has been stress-tested using the "extreme XC" problem of Knuth 7.2.2.1-(82): take all 2^n - 1 possible options on n primary items. For n = 17, it found 82,864,869,804 solutions in about 200 hours on one core of an Intel i9-13900K.

Intended (Future) Use Cases

  • Authorization, à la Oso
  • Planning, specifically for updates to the Oxide rack
  • Interactive REPL for experimentation
  • General purpose embedded logic language

About

An Answer Set Programming System

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages