As a mental exercise I have been playing around with the 3-SAT problem, but I am having difficulty proving or disproving the usefulness of a current idea that I am playing around with.
My current exploration of the problem was based off of the question: Would it be possible to create an algorithm for 3-SAT that has a runtime which is polynomial with the input size and the number of accepting solutions? (Probably not, but it makes for an interesting exercise.)
It is obvious that, if such an algorithm existed, then 3-SAT could be solvable by using the input size to compute the maximum number of steps the algorithm would run assuming that the input was not satisfiable (guaranteed to be polynomial with the input size, because the number of accepting solutions would be 0) and running the algorithm for that many steps. If the algorithm had not rejected by that point, then the input can be accepted because we know the algorithm will not reject at all.
As a first attempt at this, I have defined a datatype
SatisfactionSet which contains the following:
- A list of the clauses that must be satisfied by every possible solution in the set
- A set of the variables that are covered by the
SatisfactionSet. Every variable must appear in at least one of the clauses listed and if a variable appears in one of the clauses it must appear here.
- A list containing all possible assignments of the variables in the above set that would satisfy the listed clauses. In other words, if the above set contains
mvariables, this list would contain at most
2^massignments and every one of them must be able to satisfy all clauses
SatisfactionSets can be joined by concatenating their lists of clauses, taking the union of their variable sets, and iterating through to match each assignment from the first
SatisfactionSet with as many compatible assignments from the second
SatisfactionSet as possible. Every matching of assignments takes the union of the two assignments and makes it into an assignment in the joined
The object produced by joining two
SatisfactionSets always replaces the two objects being joined in the list of all
SatisfactionSets are only eligible to be joined if their variable sets have at least one variable in common.
Our algorithm initializes by creating one
SatisfactionSet for each clause in the input.
SatisfactionSet is ever created (either initially or by joining) that has an empty list of satisfying assignments, then our algorithm rejects the input, saying that it is not satisfiable.
Our algorithm runs until it either rejects or there are no remaining pairs of
SatisfactionSets that are eligible to be joined together. If there are no remaining pairs eligible to be joined and we haven't rejected, we accept.
I will not go into a proof of correctness here, but it is not too hard to show that this will correctly solve the 3-SAT problem. So now we begin work on trying to bring the runtime into a polynomial bound based on the input size and the number of satisfying solutions (or at least polynomial if there is no satisfying assignment).
Setting aside the issue of maintaining a list of valid join operations (since that can be done in polynomial time per join with just a little tweaking to the setup), it is readily apparent that the runtime of the algorithm can be encapsulated by observing the total number of unique assignments/assignment parts discovered by all of the
SatisfactionSets over the duration of the algorithm. Therefore, we will let a variable
C represent this total.
This is where I would like assistance. I would like to perform a sanity check on this approach.
Suppose we have a polynomial time algorithm
A which, for any input, will produce an optimal ordering of join operations such that following them will take our algorithm from initialization to termination and
C will be minimal.
We will represent the value of
C obtained when running our algorithm on input
x using the ordering provided by
The sanity check is thus:
I would like to prove or disprove that for any non-satisfiable input
x, the value of
C_A(x) is polynomial to the input size.
I would like to prove or disprove that there exists a fixed polynomial function
f of the input size, as well as a base input size n_0, such that, for all inputs
x such that
x not being satisfiable implies that
Any help or insight that could be provided on this would be greatly appreciated. Additionally, if it would simplify the proof, I do not mind if variations of 3-SAT are used instead so long as following conditions hold for the variations used:
- The variation is still a recognizable and valid variation of 3-SAT (i.e. You can't use SAT with a single really large clause that covers most variables right at the start as a disproof. It would not be recognized as a valid instance of 3-SAT.)
- The variation can still be correctly solved using the algorithm described above.
- The variation is still NP-complete.
For instance, the 3-SAT variant where each literal can appear at most two times would be a valid variant to use instead.