Stack Overflow
Stack Overflow

Questions tagged [2-satisfiability]

The Boolean 2-satisifiability problem asks whether there is a solution to a given collection of paired constraints on Boolean variables. 2SAT, as it is commonly known, is solvable in polynomial time.

The Boolean 2-satisifiability problem asks whether there is a solution to a given collection of paired constraints on Boolean variables. 2SAT, as it is commonly known, is solvable in polynomial time.

21 questions
4
votes
2 answers

How to get 2-Sat values

Whenever I search for an algorithm for 2-Sat, I get back the algorithm for the decision form of the problem: Does there exist a legal set of values that satisfy all the clauses. However, that does not allow me to easily find a set of satisfying…
user108088
  • 1,128
  • 2
  • 16
  • 29
3
votes
1 answer

How exactly does a Max 2 Sat reduce to a 3 Sat?

I've been reading this article which tries and explains how the max 2 sat problem is essentially a 3-sat problem and is NP-hard. However, if you see the article, I'm not able to understand why, after ci is satisfied, 7 out of 10 clauses are…
gabbar0x
  • 4,046
  • 5
  • 31
  • 51
3
votes
1 answer

Implication Graph Assignment

An implication graph is a directed graph where each node is assigned either true or false and any edge u -> v implies that if u is true then v is true. I know a straightforward O(n^2) algorithm to find an assignment in a general implication graph…
Corei13
  • 401
  • 2
  • 9
3
votes
2 answers

Implementation issues in 2-Satisfiability problem

I want to implement 2-SAT problem for 100000 literals. So there would be 200000 vertices. So I am stuck on having a array of all reachable vertices from each vertex, space complexity of O(200000^2) which is infeasible So please suggest a solution…
avd
  • 13,993
  • 32
  • 78
  • 99
2
votes
1 answer

I understand 2 SAT can be solved in Polynomial time finding out Strongly Connected Components. What about doing the same for 3SAT?

In case of 3SAT instead of getting 2 implications for one clause, we'd get 12(3C2*2*2) maybe.and which will form a graph of 12m edges when m is the number of clauses in 3 CNF and we can still find out the Strongly Connected Components in that…
FindersKeeper
  • 23
  • 8
2
votes
1 answer

Has anyone seen a 2-Sat implementation

I have been looking for a while, but I just can't seem to find any implementation of the 2-Sat algorithm. I am working in c++ with the boost library (which has a strongly connected component module) and need some guidance to either create an…
user108088
  • 1,128
  • 2
  • 16
  • 29
1
vote
1 answer

How does constant inputs affect SAT formulation of a problem?

Lets say I have a black box circuit with N inputs and 1 output. I want to fix the value of M inputs and find the value of rest of the inputs (N-M) for which the circuit is satisfiable. If I manually fix the M inputs in the verilog RTL, and convert…
Harshit Kumar
  • 47
  • 8
1
vote
1 answer

2 satisfiability strongly connected components topological ordering

I'm solving a two-satisfiability problem with SCCs, and have a question about topological sorting. The algorithm I'm basing this on is to process SCCs in reverse topological order, which is fine when they're all connected. My algorithm is breaking…
jimboweb
  • 4,362
  • 3
  • 22
  • 45
1
vote
1 answer

Converting Not All Equal 2-Sat Pr0blem to an equivalent 2-SAT pr0blem

I'm looking over previous exam papers, and have come across this question which has confused me. Question: Convert the Not-All-Equal 2-SAT problem given by the clauses {x1, x2}, {x2, x3}, {x3, x4}, {x4, x5}, {x5, x1} to an equivalent 2-SAT…
user6227505
  • 19
  • 2
1
vote
1 answer

Polynomial algo for 2-SAT related algorithm

I read many algorithm for finding the 2-SAT problem, i.e. given expression is satisfiable or not, which can be solved in polynomial time. example(algorithm). For Krom's procedure(Wikipedia),I construct graph from which I can easily verify its…
piyush-balwani
  • 524
  • 3
  • 15
1
vote
1 answer

2-Satisfiability problem-Whether a unique truth assignment exists or not

I have a problem which is an extension of 2-SAT problem. In standard 2-SAT problem, we can find any of the truth assignments which depends on the ordering of vertices we choose. I want to check whether there exists one and only one truth…
avd
  • 13,993
  • 32
  • 78
  • 99
0
votes
1 answer

Derivation in the Resolution Proof System

The clauses of our problem: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z} How can we conclude from these clauses to {}? I can see that this cannot be satisfied, but I am unable to find a solution in the Resolution Proof System as it seems that…
NightOwl
  • 3
  • 2
0
votes
1 answer

Dimacs cnf expression not satisfiable, why?

I am a new cs student and I have a hard time understanding satisfiability fully. I have made 2 expressions for a SAT solver. Seperately, they are satisfiable, but together they're not. I don't understand it, because i actually thought they meant the…
Karim Loberg
  • 31
  • 4
0
votes
1 answer

2-SAT variable values

2-SAT problem, finding value for variables I'm using this solution for finding satisfiability for given formula. (by checking SCC). Is there any efficient way (efficient means not worse than polynomial time in my case) how to find value for each…
Michalides
  • 152
  • 1
  • 8
0
votes
1 answer

2-Satisfiability and Strongly connected components

I know that applying Strongly connected components in a Digraph we can check 2-SAT boolean satisfiability if the problem is solvable in polynomial time. Let's assume the problem is satisfiable. The question: is there a general algorithm to…
Ivan Voroshilin
  • 5,233
  • 3
  • 32
  • 61
1
2