Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
534
questions
2
votes
0answers
18 views
Necessary condition for 3-CNF unique satisfiability
I need to iterate through all formulas of 7 variables in 3-CNF which have unique satisfying assignment (1,1,1,1,1,1,1).
I could iterate through all formulas which are true under that assignment -- ...
-4
votes
0answers
54 views
Are approximations to $#P$ gibberish? [closed]
approximations to #P are gibberish
the model count in satisfiability (#P) implies straightforward
access to a vast empire inside the logic of truth including
N Boolean variables in a formula with N ...
3
votes
2answers
48 views
Compact representation for quantified boolean formula
I got black-box (too big to analyze) boolean formula f(...) with 3 sets of input arguments: $x_1... x_i, y_1... y_j, z_1... z_k$. And I want to find such values for x-arguments that for every y-...
5
votes
1answer
80 views
Reduction from the SAT problem to the NAE-SAT problem
I study complexity and computation independently.
I have a problem that I can not solve.
That's the problem:
For the SAT problem, there is a version in which we receive as input phrase $\varphi$ in ...
1
vote
0answers
50 views
How to design an unbounded Monte Carlo algorithm for SAT(Boolean Satisfiability Problem) problem?
I want the algorithm to be in polynomial time and the correct answer rate is 0.5 or more. (True / false judgment is polynomial time)
All the methods I think of take exponential time(2^n).
Can anyone ...
1
vote
1answer
19 views
SAT formula for connected graphs on the grid
In the answer to an earlier question "SAT algorithm for determining if a graph is disjoint" a formula is constructed that is satisfiable iff a given graph is connected.
The formula uses a ...
2
votes
1answer
46 views
Number of queries for $NP^{NP}$
So a few days ago my lecturer told us that for every nondeterministic polynomial time oracle
machine $M$, there is a nondeterministic polynomial time oracle machine $N$ that gives us $L(N^{3-SAT}) = L(...
2
votes
1answer
29 views
Is there a $L$-complete variant of SAT?
Many complete problem of different class of complexity has SAT variant. Like 3-SAT or $k$-SAT is $NP$-complete, Horn-SAT is $P$-complete, 2-SAT is $NL$-complete, and so on. So I was wondering if there ...
2
votes
1answer
96 views
Why is it useful to transform 0-1 integer programming problem into SAT problem?
There are several researches studying translating 0-1 integer programming into CNF form. For example, this paper and this C++ library. As the lecture notes here goes, translating 0-1 integer ...
1
vote
1answer
25 views
Computational complexity of dividing a set of constraints into a minimum number of satisfiable clusters
I am looking for the computational complexity of the following problem.
Divide a given set of constraints into a minimum number of satisfiable clusters such that the constraints within the same ...
0
votes
0answers
49 views
Prove that following 3-CNF is SAT
Let $\phi$ be a 3-CNF expression with the properties
Every variable can be used at most 3 times
No Variable can be used twice in a term
Show that you can always choose the truth-value of the ...
1
vote
0answers
46 views
Incomplete definition of function- first order logic
Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations.
Let $\Sigma_2=\{c,g^2,R_1^1,...,R_k^1\}$ where $c$ is constant, $g$ is two ...
2
votes
1answer
24 views
NP-Hardness of Half-SAT (at least half clauses)
I'm solving Problem 14.14 of What can be computed?.
14.14 Consider the computational problem HALFSAT defined as follows. The
input is a Boolean formula B in CNF. If it is impossible to satisfy at ...
0
votes
1answer
37 views
NP Reduction - Dominating set to SAT
Given a graph G and an integer k , recognize whether G contains dominating set X with no more than k vertices. And that is by finding a propositional formula ϕG,k that is only satisfiable if and only ...
1
vote
1answer
27 views
Is there CIRCUIT-SAT algorithms that slightly depends on gates count?
For 3CNF-SAT problems exists a lot of algorithms that still have exponential complexity, but work faster than brute force. The complexity of this algorithm based on a number of variables or the number ...
0
votes
1answer
31 views
NP-completeness of variant SAT: SAT-5Clauses
I'm solving Problem 14.4 of What can be computed?.
14.4 Define the decision problem SAT-5CLAUSES as follows. The input is a Boolean formula B in CNF. The solution is “yes” if it is possible to ...
2
votes
1answer
31 views
Proving satisfiability using resolution and variable elimination
I don't 100% understand this. But I have a entailment, and I want to prove whether it is satisfiable or not, and I will do this using resolution and variable elimination.
Here is the formula:
$$
(x_1 \...
0
votes
2answers
28 views
Is the following problem NP-Complete? [closed]
3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
3
votes
1answer
32 views
Has it been shown or can we show that if $SAT \in P$ then SAT can't be in any complexity class C so that $C \subsetneq P$?
I'm already guessing that the answer is no because we cannot know whether there is a class "in between" already known classes? Or can we?
I am very new to complexity theory.
Thanks for any ...
2
votes
1answer
37 views
How to represent bottom element (integer domains) in SMT formula
I'm doing some work with static analysis and need to represent local variables as SMT formulas. In general this is fairly straight forward, depending on the domain of the static analysis. However, ...
0
votes
0answers
15 views
Multi-Objective Implicit Hitting Set for Multi-Objective MaxSAT
MaxSAT is a problem related to SAT where there is a finite collection of hard and soft clauses which share boolean variables. The hard clauses must be satisfied while the soft clauses have a weight. ...
1
vote
1answer
55 views
Complexity of All-SAT
All-SAT is the problem of enumerating all satisfying assignments of a boolean formula.
All-SAT is different from #SAT, where it suffices to find the number of satisfying assignments without ...
0
votes
0answers
19 views
Looking for prior occurrences of $k$-CNF efficiently translated to coloring?
Has anyone else ever translated 3-cnf (4-cnf) on $N$ variables and $M$ clauses
into 4 coloring on $O(M)$ vertices? By taking two variables from a clause,
the four boolean combinations correspond to ...
0
votes
1answer
31 views
Is clause learning in SAT parsimonius?
I have a model counting program bob. On some graph coloring formulas, bob got the right answer only after removing clause learning. That is to say, with clause learning, bob sometimes counts ...
1
vote
0answers
14 views
What is the difference between NP and co-NP? [duplicate]
I'm trying to understand the very simple concept of co-NP but I can't figure it out. On wikipedia, it gives the example of SAT and its complement:
The complement of any problem in NP is a problem in ...
2
votes
1answer
83 views
How is this reduction of 3-SAT to Half-SAT not valid? [duplicate]
I am studying algorithms and there is a question in CLRS called the Half-SAT problem
We are given a 3-CNF formula with n variables and m clauses where m is even. We wish to determine whether there ...
1
vote
1answer
56 views
Minimal unsatisfiable core algorithm
Wikipedia says that
There are several practical methods of computing minimal unsatisfiable cores.
but I cannot find any. I suppose that “practical methods” means polynomial algorithms. Be careful, a ...
2
votes
1answer
223 views
NOT satisfiable 3SAT instance certificate
Given a NOT satisfiable 3SAT instance, that we say $S$. Suppose that $M$ is a minimal subset of clauses of $S$ such that $M$ is NOT satisfiable. Say $X$ the subset of variables of $S$ that belong to ...
1
vote
0answers
91 views
Which features can be considered for neural network based SAT solving?
I'm trying to implement SAT solver, based on backtracking algorithm and BCP. This SAT solver is trying to pick one literal from each clause, from 3-CNF SAT instances. I've implemented a neural network ...
1
vote
1answer
54 views
Not satisfiable 3SAT instance implications
Suppose we have an instance of 3SAT that is NOT satisfiable and we say $S$.
If in $S$ there are the following $8$ clauses
$\left(a\vee b\vee c\right)\wedge\left(a\vee\bar{b}\vee c\right)\wedge\left(a\...
0
votes
0answers
47 views
Can anyone explain the pigeon-hole encoding method in proportional logic
Someone there who worked with cardinal contraindications within the framework of propositional logic? I have a problem understanding the pigeon-hole method. It is a method of satisfaction. I have been ...
0
votes
0answers
44 views
IF satisfiability problem belonged to P, can the certificate be found efficiently?
IF SAT(satisfiability problem) belongs to P, then is it possible for a certificate of an arbitrary instance of SAT to be found efficiently?
1
vote
0answers
97 views
Reduction between Parity-SAT and approximate counting
Consider two problems as defined here.
Approximate counting: Given a Boolean function $f(x)$, for $x \in \{0, 1\}^{n}$, distinguish between the two cases:
The number of satisfying assignments for $f(...
0
votes
2answers
43 views
Oracle that can only definitively say if an instance is unsatisfiable
Assuming I have an Oracle that takes as input a strictly 3SAT Boolean instance and states whether the instance is satisfiable or not. If it says instance is unsatisfiable then the instance is ...
5
votes
6answers
2k views
Can anyone give me an instance of 3SAT with exactly one solution?
I need an instance of 3SAT with exactly one solution but I cannot think of or find one anywhere. Can anyone please give me an example?
1
vote
0answers
52 views
How often can a learned clause cause this solver to backtrack?
The is an improvement to the X3SAT solver I described in What is wrong with this simple proof of P=NP? I have fixed the flaw found in that solver. Now, I want to know how often the solver described ...
2
votes
2answers
174 views
Is there a Zero-Knowledge proof for SAT?
I know that SAT can be reduced to (3 vertex) Graph colouring, and there is a Zero-knowlegde protocol (ZKP) for graph colouring. However, I am interested in a ZKP that can be performed directly on a ...
26
votes
4answers
5k views
Why is SAT so important in theoretical computer science?
In my Computability and Complexity class, we are focusing on P, NP,
NP-complete, and NP-hard problems and the one thing that keeps coming up
is the SAT problem, in the context of reduction from one ...
0
votes
1answer
57 views
Complementary for $SAT$
I have tried to find a definition of complementary language to $SAT$, I mean $\overline{SAT}$.
But I still confused, in case of $L\in \overline{SAT}$ is it mean:
if $\varphi\in L$ then all ...
2
votes
1answer
43 views
Solving largely monotone SAT formulas
I just wonder if solving largely monotone SAT formulas (meaning most clauses do not contain negated literals, but some do) is in any way easier than general SAT formulas? In other words, are there ...
2
votes
1answer
67 views
$k$-SAT completeness proof when $k$ is linear in number of variables
I'm looking at a special version of SAT in which each clause has exactly $n/2$ literals, where $n$ is the number of variables. Can we prove NP-completeness of SAT in this case?
I tried reducing 3-SAT ...
2
votes
0answers
49 views
Test suite for SAT solvers
I'm looking for a collection of SAT problems that are usable for a test suite, i.e.:
are small/easy to solve, that is, this is not a benchmark but a correctness test suite
some satisfiable, some ...
0
votes
1answer
41 views
Show that if $SAT \in P/klog(n)$ then $SAT \in P$
Show that if $SAT \in P/klog(n)$ then $SAT \in P$
Assuming that there is a a constant $k \in \mathbb{N}$ such that $SAT \in P/klog(n)$, I need to prove that $SAT \in P$.
Since $SAT \in P/klog(n)$, ...
1
vote
0answers
23 views
Different definitions of Exponential Time Hypothesis
I am reading basics of Exponential Time Hypothesis (ETH). There are two statements for it:
Statement 1
There exists no $2^{o(n)}$ algorithm for $3$-SAT, where $n$ is the number of variables.
Statement ...
0
votes
1answer
32 views
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
a. Decidable
b. At least expressive as propositional logic
c. NP-complete
a) Decidable: no, some first order ...
2
votes
1answer
16 views
What is a disequality path in the context of equality graphs?
A path consisting of a number of disequality edges and a single equality edge
A path consisting of equality edges
A path consisting of a number of equality edges and a single disequality edge
A ...
1
vote
2answers
114 views
Is there any algorithm for 3SAT problem that is fast and relatively easy to implement?
Here is the description for 3SAT satisfiability problem. I already know about the DPLL algorithm, but it's implementation is pretty complex. I would like some algorithm that is relatively simpler but ...
1
vote
1answer
47 views
1-OR-3-SAT is in P
1-OR-3-SAT:
Input: 3-CNF formula $\varphi$
Question: whether there is an assignment $x$ such that in each clause there are one or three true literals.
I need to show that this problem is in $P$. I ...
0
votes
1answer
72 views
Reduce Subset-Sum to Sat
Is there a reduction from SUBSET-SUM to SAT?
Just general SAT, not 3-SAT.
Also the given multiset S only has positive integers.
SUBSET-SUM is defined as follows:
Input: a multiset S = { x1 , ... , xn }...
1
vote
1answer
96 views
Showing resolution algorithm for 2SAT is polynomial time
I don't quite understand why the resolution algorithm completes in polynomial time for 2SAT but not 3SAT.
I'm looking at slide 42 of these slides for reference. It is clear that given two clauses of ...
