Solve signed-CNF (Many Valued SAT).

[michael-veksler]

Relevant publications:

1. There is a nice overview of signed-CNF in The SAT Problem of Signed CNF Formlas by Bernhard Beckert, Reiner Hähnle, and Felip Manyà.

   They define a signed literal as $S:q$, where S is a set of values and q is a variable, so that the literal is satisfied if $L$, the interpretation of $q$, assigns a value to $q$, such that $L(q) \in S$. They also define special cases of $S$ such as $i\uparrow$ and $j\downarrow$, which for numeric ordering of \le mean $\{ k\in N\vert k\ge i\}$ and $\{k\in N\vert k\le j\}$.

2. This is a also a CDCL based algorithm for unrestricted signed-CNF in A Proof-Producing CSP Solver by Michael Veksler and Ofer Strichman.

To support mvSAT efficiently, implement 4 types of signed-clauses.

1. The most generic clause - Each literal is a variable + set of legal values.
2. Faster signed-clause: each literal is a pair of $lb<=ub$ values, with the semantics of $S=\{k\vert lb\le k \le ub\}$
3. Fastest signed-clause - each literal is a variable and a single allowed, or banned value.
4. Binary-clause - for the fastest case of false,true values.

[michael-veksler]

First step is to implement a poly-time translation from mvSAT to Bool-SAT. The complexity if the translation (to bool-sat and back) is O(N+M), where N is the sum of domain sizes of all variables and M is the sizes of all signed-literals of all clauses. The size of a literal $q\in S$ (or $S:q$ in the notation of the first citation) is the size of the set S.

The translation goes this way:

• A domain D of a variable $q$ is a set of all legal values $q$ may be assigned with. This set is represented in bool-CNF using 2 sets of binary variables:
  1. One-hot: A bool variable $p_{k,i}$ is 1 if and only if $q_k=i$ .
  2. Ordering: A bool variable $r_{k,i}$ is 1 if and only if $i \le qk$. This variable plays an important role in keeping one-hot constraints. NOTE: $r{k,\min(Dk)} \equiv 1$ and $r{k,\max(Dk)}\equiv p{k,\max(D_k)}$ . In the code, I will not create these variables.
• Constraints to keep the variables in a valid state:
  1. $r{k,i}$ are ordered, i.e., $(r{k,i}\wedge i > \min(Dk)) \rightarrow r{k,i-1}$ . For $i\in D_k \setminus \{min(D_k)\}$ bool clauses $\neg r{k,i} \vee r{k,i-1}$ . Note that if there are gaps in $D_k$, like in $D_7=\{1,2,4\}$, then we avoid defining the values in the gap. In this example we get $\neg r{7,4}\vee r{7,2}$ . For such cases, for $(i\in D_k) \wedge i > \min(D_k) \wedge prev(D_k,i) > \min(D_k)$ the bool-clause becomes $\neg r{k,i} \vee r{k,prev(D_k, i)}$, where $prev(D_k, i)\triangleq \max(\{j\in D_k\vert j < i\})$ . Reminder: $r_{k,\max(Dk)}\equiv p{k,\max(D_k)}$ .
  2. For each $q_k$ there is at least one true $i\in Dk \wedge p{k,i}$ :
     bool-clause $\bigvee_{i\in Dk}. p{k,i} $
  3. For each $qk$ there is at most one true $p{k,i}$ for each $i\in Dk$. Since there can be only one falling edge in the ordering variables, $r{k,i}$, then we can use that edge to make sure only one $p_{ki}$ is set. bool clauses: $\neg p{ki}\vee r{k,i}$ and $\neg p_{ki}\vee \neg r{k,next(D_k, i)}$ where $next(D_k,i)\triangleq \min(\{j\in D_k\vert j > i\})$ .
• Constraints to keep signed-clauses in a valid state:
  1. For each signed-clause $C_m = \bigveej. q{v{m,j}} \in S{m,j}$ and for each $i \in S{m,j}$ we generate the clause $\bigvee{1\le j \le \vert Cm \vert} \bigvee{i\in S_{m,j}.} p_i $