Skip to main content
Download PDF
- Main
Finding all solutions if you can find one
Abstract
We address the problem of enumerating (producing) all models of a given theory. We show that the enumeration task can be performed in time proportional to the product of the number of models and the effort needed to generate each model in isolation. In other words, the requirement of generating a new solution in each iteration does not in itself introduce substantial complexity. Consequently, it is possible to decide whether any tractably satisfiable formula has more than K solutions in time polynomial in the size of the forumla and in K. In the special cases of Horn formulas and 2-CNFs, although counting is #P-complete, to decide whether the count exceeds K, is polynomial in K.
Main Content
For improved accessibility of PDF content, download the file to your device.
Enter the password to open this PDF file:
File name:
-
File size:
-
Title:
-
Author:
-
Subject:
-
Keywords:
-
Creation Date:
-
Modification Date:
-
Creator:
-
PDF Producer:
-
PDF Version:
-
Page Count:
-
Page Size:
-
Fast Web View:
-
Preparing document for printing…
0%