=Paper=
{{Paper
|id=Vol-2650/paper3
|storemode=property
|title=The BWConverter Toolchain: An Incomplete Way to Convert SAT Problems into Directed Graphs
|pdfUrl=https://ceur-ws.org/Vol-2650/paper3.pdf
|volume=Vol-2650
|authors=Tamás Balla,Csaba Biró,Gábor Kusper
|dblpUrl=https://dblp.org/rec/conf/icai3/BallaBK20
}}
==The BWConverter Toolchain: An Incomplete Way to Convert SAT Problems into Directed Graphs==
https://ceur-ws.org/Vol-2650/paper3.pdf
Proceedings of the 11th International Conference on Applied Informatics
Eger, Hungary, January 29–31, 2020, published at http://ceur-ws.org
The BWConverter Toolchain: An
Incomplete Way to Convert SAT Problems
into Directed Graphs∗
Tamás Balla, Csaba Biró, Gábor Kusper
Eszterházy Károly University, Faculty of Informatics
{balla.tamas,biro.csaba,kusper.gabor}@uni-eszterhazy.hu
Abstract
In our previous works we showed, how to convert a directed graph into a
SAT problem. We showed that if the directed graph is strongly connected,
then the converted SAT problem is Black-and-White. A SAT problem is
Black-and-White if it has exactly two solutions, the black assignment, where
each variable is false, and the white one, where each variable is true. In
this paper, we study the other way: How to convert a SAT problem into a
directed graph. This direction seems to be very difficult, so we introduce
the BWConverter toolchain which helps us to create Black-and-White SAT
instances, and convert them to directed graphs using different strategies. The
toolchain consist of two tools: the BWConverter and the NPP tool. As a first
step, one has to use the BWConverter tool, which creates a Black-and-White
SAT problem from any UNSAT problems. The resulting SAT problem is
Black-and-White if the input was UNSAT . As a second step, we generate
a directed graph using our NPP tool. This tool generates edges from clauses
which contain either exactly one positive literal, or exactly one negative one
using the observations of our previous models.
Keywords: SAT, Strongly Connected Directed Graphs, BWConverter
MSC: 03B05, 05C20
1. Introduction
The propositional satisfiability problem, for short the SAT problem, is the problem
to find an assignment to the the Boolean variables of the input formula which
∗ This research was supported by the grant EFOP-3.6.1-16-2016-00001 “Complex improvement
of research capacities and services at Eszterházy Károly University”.
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License
Attribution 4.0 International (CC BY 4.0).
24
makes it true. The formula is given in conjunctive normal form (CNF) which is
represented as a clause set. If each clause consists of at most 𝑘 literals, then it is a
𝑘-SAT problem. We know that the 2-SAT problem is solvable in linear time [1]. On
the other hand 3-SAT is NP-complete [7]. So, there is a big the gap between the
easiness of 2-SAT and hardness of 3-SAT. We know some classes which are between
them:
Horn SAT is the restriction to instances where each clause has at most one
positive literal. Horn SAT is solvable in linear time [9], as are a number of gen-
eralizations such as renamable Horn SAT [2], extended Horn SAT [6] and q-Horn
SAT [5].
The hierarchy of tractable satisfiability problems [8], which is based on Horn
SAT and 2-SAT, is solvable in polynomial time. An instance on the 𝑘-th level of
the hierarchy is solvable in 𝑂(𝑛𝑘+1 ) time.
𝑟,𝑟-SAT, where 𝑟,𝑠-SAT is the class of problems in which every clause has
exactly 𝑟 literals and every variable has at most 𝑠 occurrences. All 𝑟,𝑟-SAT problems
are satisfiable in polynomial time [15].
A formula is SLUR (Single Lookahead Unit Resolution) solvable if, for all possible
sequences of selected variables, algorithm SLUR does not give up. Algorithm SLUR
is a non-deterministic algorithm based on unit propagation. It eventually gives
up the search if it starts with, or creates, an unsatisfiable formula with no unit
clauses. The class of SLUR solvable formulae was developed as a generalization
including Horn SAT, renamable Horn SAT, extended Horn SAT, and the class of
CC-balanced formulae [14].
In this paper we restrict the general SAT problem such that each clause should
contain at least one positive and one negative literal. We study how can we generate
a directed graph from this kind of problem. Our goal is to give tools which help to
do this work.
In our previous works we showed, how to convert a directed graph into a SAT
problem [3, 12]. We have presented two SAT solvers [4, 10, 11] and introduced
several models [13]. We showed that if the directed graph is strongly connected,
then the converted SAT problem is Black-and-White.
A SAT problem is Black-and-White if it has exactly two solutions, the black
assignment, where each variable is false, and the white one, where each variable is
true. In this paper, we study the other way: How to convert a SAT problem into a
directed graph.
This direction seems to be very difficult, because if we would have a complete
converter from SAT to directed graphs, then we could use our previous result to
convert it to 2-SAT, i.e., we would have a SAT to 2-SAT converter. What we present
is just an incomplete converter, so we do not attack the P = NP question.
The BWConverter toolchain contains two tools: the BWConverter and the
NPP tool. As a first step, one has to use the BWConverter tool, which creates a
Black-and-White SAT problem from UNSAT problems.
The BWConverter makes sure that its output has the same set of solutions as the
input, except the black and the white assignment. To do so, we have implemented
25
several algorithms.
The most interesting one introduces two new variables, 𝑥 and 𝑦; then it adds
(¬𝑦) to each clause which contains only positive literals; then it adds (𝑥) to each
clause which contains only negative ones; finally, it adds (¬𝑥 ∨ 𝑦) as a new clause
to the output. The resulting SAT problem is Black-and-White if the input was
UNSAT.
As a second step, we generate a directed graph using our NPP tool. This tool
generates edges from clauses which contain either exactly one positive literal, or
exactly one negative one using the observations of our previous models.
From example from the clause (¬𝐴 ∨ 𝐵 ∨ 𝐶) it generates the edges: 𝐴 → 𝐵
with weight 50%, and 𝐴 → 𝐶 with weight 50%. From the clause (¬𝐴 ∨ ¬𝐵 ∨ 𝐶)
it generates the edges (the weights are in ()): 𝐴 → 𝐶 (50%), 𝐵 → 𝐶 (50%),
𝐴 → 𝐵 (50%), and 𝐵 → 𝐴 (50%). This conversation is too eager, because it creates
a strongly connected graph even if the input was not a Black-and-White SAT
problem. As a solution, we attach to each edge a weight number which indicates,
how likely is that the edge is important. Then we iteratively remove the edges with
the smallest and / or with the highest weight until we would have a non strongly
connected directed graph in the next iteration. We call this directed graph to be
the directed graph representation of the input SAT problem.
We studied where this state transition point is in case of unsatisfiable random
3-SAT problems.
2. The BWConverter tool
The BWConverter tool can create a Black-and-White SAT problem from an UNSAT
problem. It has 3 main switches:
BWConverter -nooverlap num | BWConverter -n num
BWConverter -overlap num | BWConverter -o num
BWConverter -pigeonholeeater | BWConverter -p
After the first two ones we give a number, which shows how smart do we use
these strategies. If the number is 0, then we do not use other input clauses to
generate less clauses. 1 means that we use always the same clause to generate less
clauses. 2 means that we use one of the best clause in order to generate as few
clauses as possible.
They remove the black and the white clauses from each input clause. We
introduce them by examples. Let us assume that the input has 6 variables: from 𝑎
to 𝑓 , these clauses was already processed: {𝑎, 𝑑, 𝑒}, {𝑏, 𝑐, 𝑑}, and the current clause
is {𝑎, 𝑏, 𝑐}. Then:
-n 0 generates: {𝑎, 𝑏, 𝑐, ¬𝑑}, {𝑎, 𝑏, 𝑐, 𝑑, ¬𝑒}, {𝑎, 𝑏, 𝑐, 𝑑, 𝑒, ¬𝑓 }.
-n 1 generates: {𝑎, 𝑏, 𝑐, ¬𝑑}, {𝑎, 𝑏, 𝑐, 𝑑, ¬𝑒}.
-n 2 generates: {𝑎, 𝑏, 𝑐, ¬𝑑}.
-o 0 generates: {𝑎, 𝑏, 𝑐, ¬𝑑}, {𝑎, 𝑏, 𝑐, ¬𝑒}, {𝑎, 𝑏, 𝑐, ¬𝑓 }.
-o 1 generates: {𝑎, 𝑏, 𝑐, ¬𝑑}, {𝑎, 𝑏, 𝑐, ¬𝑒}.
-o 2 generates: {𝑎, 𝑏, 𝑐, ¬𝑑}.
26
Note, that in case of -n there is no such full-length clause which is subsumed
by the generated clauses, so they do not overlap.
-p introduces two new variables 𝑥 and 𝑦; then it adds (¬𝑦) to each clause which
contains only positive literals; then it adds (𝑥) to each clause which contains only
negative ones; finally, it adds (¬𝑥 ∨ 𝑦) as a new clause to the output. The resulting
SAT problem is Black-and-White if the input was UNSAT.
An example for -p is the following: Let us assume that the input is (𝑎 ∨ 𝑏) ∧ (𝑐 ∨
𝑑) ∧ (𝑒 ∨ 𝑓 ) ∧ (¬𝑎 ∨ ¬𝑐) ∧ (¬𝑎 ∨ ¬𝑒) ∧ (¬𝑐 ∨ ¬𝑒) ∧ (¬𝑏 ∨ ¬𝑑) ∧ (¬𝑏 ∨ ¬𝑓 ) ∧ (¬𝑑 ∨ ¬𝑓 ),
which is actually the Pigeon Hole problem1 with 3 pigeons and 2 holes. Then the
output is: (¬𝑦 ∨ 𝑎 ∨ 𝑏) ∧ (¬𝑦 ∨ 𝑐 ∨ 𝑑) ∧ (¬𝑦 ∨ 𝑒 ∨ 𝑓 ) ∧ (𝑥 ∨ ¬𝑎 ∨ ¬𝑐) ∧ (𝑥 ∨ ¬𝑎 ∨ ¬𝑒) ∧
(𝑥 ∨ ¬𝑐 ∨ ¬𝑒) ∧ (𝑥 ∨ ¬𝑏 ∨ ¬𝑑) ∧ (𝑥 ∨ ¬𝑏 ∨ ¬𝑓 ) ∧ (𝑥 ∨ ¬𝑑 ∨ ¬𝑓 ) ∧ (¬𝑥 ∨ 𝑦).
There are some more minor switches:
-nob means that the output will not subsume the black clause.
-now means that the output will not subsume the white clause.
-bw means that the generated output will be a black-and-what SAT problem, if
the input was an UNSAT problem. This is the same as -nob -now, and this is a
default switch.
-same means that the output problem will have the same set of solutions as the
input, because it adds the black and the white clauses at the end of the output.
-help prints the help.
3. The NPP Tool
The NPP tool work as follows: it reads a CNF file in DIMACS format. For each
clause 𝐶 it adds the edges (𝑛, 𝑝, 𝑤) to the graph, where 𝑛 is a negative literal, 𝑝
is a positive literal, and 𝑤 is 1/𝑝𝑜𝑠, where 𝑝𝑜𝑠 is the number of positive literals in
𝐶. It also adds the edges (𝑛1 , 𝑛2 , 𝑛𝑤) to the graph, where 𝑛1 and 𝑛2 are different
negative literals, and 𝑛𝑤 = 1/𝑛𝑒𝑔, where 𝑛𝑒𝑔 is the number of positive literals in
𝐶.
For example if 𝐶 = {¬𝑎, ¬𝑏, ¬𝑐, 𝑑, 𝑒}, then the following edges is added to the
graph: (𝑎, 𝑑, 0.5), (𝑏, 𝑑, 0.5), (𝑐, 𝑑, 0.5), (𝑎, 𝑒, 0.5), (𝑏, 𝑒, 0.5), (𝑐, 𝑒, 0.5), (𝑎, 𝑏, 0.33),
(𝑎, 𝑐, 0.33), (𝑏, 𝑎, 0.33), (𝑏, 𝑐, 0.33), (𝑐, 𝑎, 0.33), (𝑐, 𝑏, 0.33).
The tool has the following switches:
NPP -autominlimit | NPP -a
NPP -automaxlimit | NPP -A
NPP -setminlimit num | NPP -s num
NPP -setmaxlimit num | NPP -S num
NPP -normalized | NPP -N
-a finds the biggest limit, such that by deleting edges with weight ≤ limit the
directed graph is still strongly connected. -A finds the lowest limit, such that by
deleting edges with weight ≥ limit the directed graph is still strongly connected.
-s sets the lower limit to num, i.e., it deletes all edges where the weight ≤ num.
1 https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/PHOLE/descr.html
27
-S sets the upper limit to num, i.e., it deletes all edges where the weight ≥ num.
The most typical usage is NPP -a -A which finds automatically both limits.
The output of the NNP tool is the adjency matrix of the constructed and
modified graph. If 𝑀𝑖𝑗 = −1 that means that there is no directed vertex from 𝑖 to
𝑗, otherwise the value is the weight of vertex from 𝑖 to 𝑗. If we use -N switch the
tool will normalize the weight values to [0; 1] interval before it removes any edge
from graph.
4. An Example
The initial UNSAT 3-SAT formula let be as follows: (¬𝑎 ∨ 𝑏 ∨ 𝑑) ∧ (𝑎 ∨ ¬𝑐 ∨ 𝑑) ∧
(𝑎 ∨ ¬𝑏 ∨ ¬𝑑) ∧ (𝑏 ∨ ¬𝑐 ∨ ¬𝑑) ∧ (¬𝑎 ∨ 𝑐 ∨ ¬𝑑) ∧ (𝑎 ∨ 𝑏 ∨ 𝑐) ∧ (¬𝑎 ∨ ¬𝑏 ∨ ¬𝑐).
After running the BWConverter tool, the modified formula is as follows: (¬𝑎 ∨
𝑏∨𝑑)∧(𝑎∨¬𝑐∨𝑑)∧(𝑎∨¬𝑏∨¬𝑑)∧(𝑏∨¬𝑐∨¬𝑑)∧(¬𝑎∨𝑐∨¬𝑑)∧(𝑎∨𝑏∨𝑐∨¬𝑑)∧(¬𝑎∨
¬𝑏 ∨ ¬𝑐 ∨ 𝑑). Note, that this is not UNSAT any more, it is Black-and-White.
a a
133,33 % 66,66 % 133,33 %
133,33 % 133,33 %
d 66,66 % b d b
133,33 % 66,66 % 133,33 %
c c
Result of using the tool with
The generated graph from the formula -a -A (NPP -a -A)
5. Usage and Conclusion
The toolchain can be found here: http://fmv.ektf.hu/tools.html. It consists
of two tools: BWConverter, and NPP. Its typical usage is the following:
• java BWConverter -o 2 unsat.cnf bw.cnf
• java NPP -a -A -N bw.cnf
This work was an inner project, because we used to need a tool to test our
theories. For us the toolchain was very useful, so we decided to publish it. As future
work we should prove the lemmas what we found by the help of this toolchain.
References
[1] B. Aspvall, M. F. Plass, R. E. Tarjan, A Linear-Time Algorithm For Testing
The Truth Of Certain Quantified Boolean Formulas, Information Processing Letters,
pp. 121–123, 1979.
28
[2] B. Aspvall, Recognizing Disguised NR(1) Instances of the Satisfiability Problem, J.
of Algorithms, 1, pp. 97–103, 1980.
[3] Cs. Biró, G. Kusper, Equivalence of Strongly Connected Graphs and Black-and-
White 2-SAT Problems, Miskolc Mathematical Notes, Vol. 19, No. 2, pp. 755-768,
2018.
[4] Cs. Biró and G. Kusper, BaW 1.0 - A Problem Specific SAT Solver for Effective
Strong Connectivity Testing in Sparse Directed Graphs, CINTI-2018, pp. 137-142,
2018.
[5] E. Boros, P. L. Hammer, X. Sun, Recognition of q-Horn Formulae in Linear
Time. Discrete Applied Mathematics, v. 55, pp. 1–13, 1994.
[6] V. Chandru, J. Hooker, Extended Horn Sets in Propositional Logic, J. of the
ACM, 38(1), pp. 205–221, 1991.
[7] S. A. Cook, The Complexity of Theorem-Proving Procedures, Proc of STOC’71, pp.
151–158, 1971.
[8] M. Dalal, D. W. Etherington, A Hierarchy of Tractable Satisfiability Problems.
Information Processing Letters, v.44, pp. 173–180, 1992.
[9] W. F. Dowling, J. H. Gallier, Linear-Time Algorithms for Testing the Satisfia-
bility of Propositional Horn Formulae. J. of Logic Programming, 1(3), pp. 267–284,
1984.
[10] G. Kusper and Cs. Biró, Solving SAT by an Iterative Version of the Inclusion-
Exclusion Principle, SYNASC 2015, IEEE Computer Society Press pp. 189–190,
2015.
[11] G. Kusper, Cs. Biró, Gy. B. Iszály, SAT solving by CSFLOC, the next generation
of full-length clause counting algorithms, Future IoT 2018, pp.1–9, 2018.
[12] G. Kusper, Cs. Biró, Convert a Strongly Connected Directed Graph to a Black-
and-White 3-SAT Problem by the Balatonboglár Model, submitted to Theory of Com-
puting, 17 pages, arrived on 24.08.2019, status: under review.
[13] G.Kusper, Cs. Biró, T. Balla, Representing Directed Graphs as 3-SAT Problems
Using The Simplified Balatonboglár Model, The 11th International Conference on
Applied Informatics to be held in Eger, Hungary January 29–31, 2020.
[14] J. S. Schlipf, F. Annexstein, J. Franco, R. P. Swaminathan, On finding
solutions for extended Horn formulas, Information Processing Letters, v. 54, pp.
133–137, 1995.
[15] C. A. Tovey, A Simplified NP-complete Satisfiability Problem, Discrete Applied
Mathematics, v. 8, pp. 85–89, 1984.
29