Short UNSAT Certificates for X3SAT

Question

Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause contains exactly one literal from the set. $X3SAT$ is NP-Complete even when the instance is monotone and linear. Monotone means all literals are positive. Linear means no two clauses share more than one variable in common. The rest of this question assumes a monotone, linear instance of X3SAT clauses.

A variable is unique if it only appears once in the entire instance.

A conflict cluster has an inner or conflict clause with no unique variables. For each literal in the inner clause there is one outer clause in the cluster that shares that literal. Because we assume the instance is linear, the number of clauses in a conflict clause equals the number of literals in the inner clause plus one.

Assuming all the clauses in the conflict cluster are X3SAT clauses then a conflict cluster has four clauses and from 6 to 9 variables. Conflict clusters with 6 or 7 variables have three satisfying assignments. Clusters with 8 variables has six satisfying assignments. Clusters with 9 variables have twelve satisfying assignments.

A satisfying assignment for a conflict cluster is blocked if the assignment causes a conflict when applied to the entire instance and unit clause propagation is performed.

A conflict cluster is completely blocked if all the satisfying assignments for the conflict cluster are blocked.

Do all unsatisfiable, monotone, linear X3SAT instances have a completely blocked conflict cluster?

If this conjecture is true then it proves NP=co-NP.

I don’t think the conjecture is true. However, all unsatisfiable X3SAT instances I have looked at have many completely blocked conflict clusters.

A worked example.

This instance has 13 variables and 10 clauses:

$(a,c,k) (a,i,l) (b,j,m) (c,d,e) (c,f,g) (e,g,k) (e,h,l) (f,k,l) (g,j,l) (i,k,m)$

Conflict cluster with 8 variables and 6 satisfying assignments:

$(f,k,l) (c,f,g) (e,g,k) (a,i,l)$

Six satisfying assignments:

$a e f \bar{c} \bar{g} \bar{i} \bar{k} \bar{l}$

$e i f \bar{a} \bar{c} \bar{g} \bar{k} \bar{l}$

$a k \bar{e} \bar{f} \bar{g} \bar{i} \bar{l}$

$i k \bar{a} \bar{e} \bar{f} \bar{g} \bar{l}$

$c e l \bar{a} \bar{f} \bar{i} \bar{k} \bar{l}$

$g l \bar{a} \bar{c} \bar{e} \bar{f} \bar{i} \bar{k}$

All these assignments are blocked:

$a e f \bar{c} \bar{g} \bar{i} \bar{k} \bar{l}$

makes $j=true$ in unit clause $(g,j,l)$ causing $(i,k,m)$ to block.

$(i,k,m) (A,i,l) (A,c,k) (b,J,m)$

$e i f \bar{a} \bar{c} \bar{g} \bar{k} \bar{l}$ causes $(a,c,k)$ to block

$(a,c,k) (a,I,l) (c,F,g) (F,k,l)$

$a k \bar{e} \bar{f} \bar{g} \bar{i} \bar{l}$ causes $(A,c,K)$ to block

$i k \bar{a} \bar{e} \bar{f} \bar{g} \bar{l}$ causes $(I,K,m)$ to block

$c e l \bar{a} \bar{f} \bar{i} \bar{k} \bar{l}$ causes $(C,d,E)$ to block

$g l \bar{a} \bar{c} \bar{e} \bar{f} \bar{i} \bar{k}$ causes $(G,j,L)$ to block

Some of the other completely blocked conflict clusters in this instance.

$(e,g,k) (e,h,l) (g,j,l) (f,k,l)$

$(e,g,k) (c,d,e) (c,f,g) (a,c,k)$

$(g,j,l) (e,g,k) (b,j,m) (e,h,l)$

$(i,k,m) (a,i,l) (a,c,k) (b,j,m)$

Answer 1

I can now prove my conjecture is false. The unsatisfiable 4 Pigeons in 3 Holes problem, when converted to linear, monotone X3SAT, does not have any completely blocked Conflict Clusters.

A conflict cluster has an inner “conflict” clause. For each literal in the inner clause there is one outer clause that has that literal. A conflict cluster of linear X3SAT clauses has four clauses, one inner and three outer. Linear, monotone X3SAT conflict clusters can have from 6 to 9 variables. A cluster with 6 or 7 variables always has three satisfying “cluster” assignments. Clusters with 8 variables have 6 cluster assignments, and clusters with 9 variables have 12 cluster assignments.

A conflict cluster with 9 variables has 2^9 possible assignments. Only 12 of these will satisfy the cluster. It is simple to generate the valid cluster assignments using a few simple rules.

(a,b,c)(a,x1,y1)(b,x2,y2)(c,x3,y3)

Note that exactly one of (a,b,c) can be true. Choosing a to be true satisfies two of the clauses and reduces the other two clauses to disjoint X2SAT:

a = true / b,c,x1,y1 = false

(x2,y2)( x3,y3)

There are 4 satisfying assignments for the disjoint X2SAT clauses. a ,b, and c each have 4 satisfying assignments where they are true for a total of 12.

A cluster assignment is “blocked” if the assignment causes a contradiction when it is applied to the entire X3SAT instance and unit clause resolution is performed. A conflict cluster is completely blocked if all of the cluster assignments are blocked. If the clauses in the conflict cluster can’t be satisfied then the entire X3SAT instance is unsatisfiable. A completely blocked conflict cluster can be used as an UNSAT certificate that can be checked using only unit clause resolution in a polynomial number of steps.

I used standard methods to convert the 2+SAT 4 Pigeons in 3 Holes problem into a linear, monotone X2+SAT instance. The original 2+SAT instance has 12 variables, 4 3SAT clauses, and 18 2SAT clauses. The linear, monotone X2+SAT instance has 108 variables, 34 X3SAT clauses, and 54 X2SAT clauses. Half of the variables and all of the X2SAT clauses were added when the instance was converted to monotone. No processing was required to make the instance linear. The standard 3SAT to X3SAT conversion creates linear instances.

The X2+SAT instance only has 4 X3SAT conflict clusters. All four clusters come from converting the 4 3SAT clauses to X3SAT. I find it interesting that the standard method for converting 3SAT to X3SAT will always create a conflict cluster. All of the conflict clusters are similar. All of the clusters have 9 variables and 12 cluster assignments. 9 of the cluster assignments are blocked for each cluster. None of the 4 clusters are completely blocked.

The X2+SAT instances also has 36 conflict clusters where the inner clause is X2SAT. None of these clusters are completely blocked, either.

I wanted to find an XSAT instance with no completely blocked conflict clusters to use as a test for my DPLL like X2+SAT solver. My solver searches for conflict clusters and backtracks when it finds one. The solver creates a new type of learned clause I call an “assignment clause” that prevents the solver from visiting the same conflict cluster more than once.

Most DPLL solvers must backtrack through an entire instance to prove the instance is unsatisfiable. This is not true for my solver. My solver seems to always find a completely blocked conflict cluster. It does so with this 4 Pigeons in 3 Holes instance.

It is possible to reduce variables if a conflict cluster has a small number of unblocked cluster assignments. For example, if a variable is False in every unblocked cluster assignment then it must be False in any satisfying assignment for the entire instance. Similarly, if two variables are equal in every unblocked cluster assignment they must be equal in any satisfying assignment.

My algorithm will reduce variables and restart when possible. The four X3SAT conflict clusters in the pigeonhole instance only have 3 unblocked assignments each. This allows my algorithm to reduce 6 of the 9 variables in the cluster and restart. This reduction creates a new conflict cluster which is completely blocked.

There are UNSAT certificates consisting of 8 clauses for this 108 variable, 88 clause Pigeonhole X2+SAT instance. We can prove the instance is unsatisfiable by performing unit clause resolution on 24 cluster assignments and applying a few, simple reduction rules.

I can provide the entire X2+SAT Pigeonhole instance if anyone is interested,