On the expressive power of unit resolution
Olivier Bailleux

TL;DR
This paper investigates the expressive capabilities of unit resolution in propositional logic, characterizing computable functions and revealing limitations in polynomial-time computability due to exponential clause requirements.
Contribution
It introduces the concept of propagatable functions, linking them to monotone circuits, and highlights the exponential complexity in certain polynomial-time functions when using unit resolution.
Findings
Propagatable functions are characterized and linked to monotone circuits.
Some polynomial-time functions require exponential clauses in unit resolution.
Results inform CNF encoding strategies for NP-complete problems.
Abstract
This preliminary report addresses the expressive power of unit resolution regarding input data encoded with partial truth assignments of propositional variables. A characterization of the functions that are computable in this way, which we propose to call propagatable functions, is given. By establishing that propagatable functions can also be computed using monotone circuits, we show that there exist polynomial time complexity propagable functions requiring an exponential amount of clauses to be computed using unit resolution. These results shed new light on studying CNF encodings of NP-complete problems in order to solve them using propositional satisfiability algorithms.
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
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Constraint Satisfaction and Optimization
