For any ( k , d )-CNF formula with a variable set V, is a proper subset of V, if a truth assignment set on exists such that only a literal in each clause is true, then it is the regular partial exact ( k , d )-SAT problem. When , it is the regular exact ( k , d )-SAT problem. It is necessary to analyze the complexity of these two classes of regular exact ( k , d )-SAT problems and the relationships between them.
To solve the problems, a research team led by Guoxia Nie published their new research on 15 Feb 2024 in Frontiers of Computer Science co-published by Higher Education Press and Springer Nature.
The team constructed satisfying assignments of formulas from the perspective of factor graphs, and also found that a formula can be partial exactly satisfied, but it does not have to be exactly satisfiable. As shown in Figure, the formula is 2-partial exactly satisfiable but not 2-exactly satisfiable.
The phase transition points of two kinds of regular exact ( k , d )-SAT problems are obtained by first and second moment methods. Through the experimental simulation, it is found that the theoretical results are consistent with the experimental results. By comparing the results of two experiments, with an increasing problem scale, the upper and lower bounds of the instances that are satisfied and unsatisfied became clearer.
DOI: 10.1007/s11704-023-3402-4
Frontiers of Computer Science
Experimental study
Not applicable
Exact satisfiability and phase transition analysis of the regular (k,d)-CNF formula
15-Feb-2024