3
$\begingroup$

If we suppose that we'd like to convert an instance of 3-SAT to an instance of 4-SAT, by how much can we reduce the amount of variables?

CONVERSION METHODS FOR PRODUCTS OF SUMS

If we are given a 3-SAT clause $(A \lor B \lor C)$, we can readily convert this to 4-SAT by rewriting it as $(A \lor B \lor C \lor x) \land (A \lor B \lor C \lor \overline{x})$, where $x$ is a free variable. In other words, $x$ can be any one of the existing variables, or a completely new variable. This entails that we can gaurantee that 3-SAT can be converted to 4-SAT without adding any new variables.

Additionally, we can convert 3-SAT into 4-SAT and eliminate one variable, given a special set of clauses. The 3-SAT clauses

$$(x \lor B \lor D) \land (\overline{A} \lor \overline{C} \lor x) \land (A \lor C \lor \overline{x}) \land (A \lor \overline{C} \lor x) \land (\overline{A} \lor C \lor x)$$

readily "reduce" to $(A \lor B \lor C \lor D)$. This eliminates the free variable $x$, assuming it only appears in these clauses, and also greatly reduces the number of clauses. The significance of this is that we may be able to eliminate some variables using this technique.

THE MAIN QUESTION

What are some other techniques for reducing the number of variables when converting from 3-SAT to 4-SAT?

Note that converting from product-of-sums to sum-of-products form may also be useful.

$\endgroup$
2
$\begingroup$

The paper Effective Preprocessing in SAT through Variable and Clause Elimination covers the variable elimination techniques used in Minisat. Broadly, variables can be eliminated by

  1. Substitution, in which a variable to be removed is defined in terms of other variables in the formula and the definition is substituted everywhere in place of the variable. Automatic Extraction of Functional Dependencies describes how to efficiently find (some of) these variable definitions.

  2. Distribution, in which all clauses containing a negated literal of $x$ are resolved against all clauses containing a positive literal of $x$. The produced resolvents are kept (minus any tautological clauses) and the original clauses containing $x$ are discarded. The resulting formula is satisfiable iff the original formula was satisfiable.

The overall goal of the techniques described in the Minisat paper is to optimize the formula for exploration by a CDCL solver by reducing the total number of clauses and strengthening (decreasing the length of) the clauses that remain. You could of course (with exponential effort) eliminate all the variables, eliminating all the clauses as well if the formula was satifiable or leaving one or more empty clauses if formula was unsatisfiable.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.