Nested satisfiability
Donald E. Knuth
TL;DR
This paper introduces a special hierarchical form of the satisfiability problem that can be solved efficiently in linear time with proper clause representation.
Contribution
It demonstrates that nested satisfiability, a hierarchical variant, is solvable in linear time, unlike general SAT problems.
Findings
Nested satisfiability is solvable in linear time.
Proper clause representation is crucial for efficiency.
Hierarchical structure simplifies the satisfiability problem.
Abstract
A special case of the satisfiability problem, in which the clauses have a hierarchical structure, is shown to be solvable in linear time, assuming that the clauses have been represented in a convenient way.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Constraint Satisfaction and Optimization · Formal Methods in Verification