Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Filter by
Sorted by
Tagged with
2
votes
0answers
124 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
1
vote
1answer
123 views

Complexity of 1-in-3 SAT variant with restrictions on “unique” variables per clause

I'm interested in the complexity of a particular variant of 1-in-3 SAT. Assume, as is usual, that clauses are allowed to be of length 1, 2, or 3. Then add the restriction that for any clause of length ...
3
votes
1answer
50 views

Maximize the number of satisfied disjunctions

I have ~4000 variables that are used in ~5000 logical formulas, where each formula consists only of conjunctions of the (non-negated) variables. I want to find the maximum number of satisfied formulas,...
2
votes
1answer
144 views

If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?

If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?
2
votes
1answer
150 views

What is the complexity of determining Satisfiability of a CNF containing both Horn and Dual Horn clauses?

If a CNF contains both horn and dual horn clauses and does not contain clauses of other types, then can its Satisfiability always be determined in polynomial time? If the answer to the above problem ...
3
votes
3answers
643 views

How does the number of clauses affect the difficulty of a 3-SAT problem? [closed]

What is the relationship between the number of clauses and the difficulty of a 3-SAT problem?
1
vote
1answer
89 views

How to adapt DPLL to solve HORNSAT?

This question wask asked in a homework of Computer Theory in Rome, Italy. How to simplify the DPLL algorithm in order to solve HORNSAT? My Approach: I know that an Horn clause is an OR of ...
1
vote
0answers
132 views

DPLL algorithm for 3SAT [closed]

This question is from my complexity theory course. How to change the standard DPLL algorithm for SAT in order to solve 3-SAT instances? The general DPLL algorithm for SAT is defined: ...
2
votes
1answer
109 views

Solving SAT correctly on all but $poly(m)$ formulas

The question is to show that there is no deterministic polynomial time algorithm that solves SAT correctly on all but $poly(m)$ formulas of size $m$, for every $m \geq 0$ unless $P \ne NP$. I know ...
0
votes
0answers
150 views

Proving SAT is in L

How to prove that SAT is in L if and only if NP=L? I know that reducing SAT in cook-levin theorem is computable in deterministic linear space . How to do it in log space? Any reference will also help.
1
vote
3answers
105 views

NP-hardness of an extention of 2 sat

a 2 sat instance which is unsatisfiable and an integer k are given, decision problem is that: is it possible to delete k variables, also remove clauses contain them, in order to satisfy the 2-sat ...
1
vote
1answer
146 views

Is it possible to reduce a SAT problem to it's simplest form with no assumed variables in P time? [closed]

So as you read in the title I want to know if it is possible in polynomial time to reduce a SAT problem to it's simplest version in CNF format with no assumed variables? The simplest form is with ...
1
vote
1answer
40 views

Checking large number of configurations with multiple constraints

I have a very large number of constraints such as: $ A1 \land B1 \land C1 \land D1 \land E1 \land F1$ $ A2 \land B2 \land C2 \land D2 \land E2 \land F2$ $ A3 \land B3 \land C3 \land D3 \land E3 \land ...
2
votes
1answer
931 views

Bit Blasting Algorithm

I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example: Assume our bit-...
4
votes
2answers
583 views

How could an SMT solver be implemented as simple as possible?

I'm trying to figure out how an SMT solver works as simple as possible. Let's assume we have a simple input program with symbolic values x and ...
2
votes
2answers
76 views

Do we know something about this refutation method for SAT?

Let we have a formula $\varphi(x_1,x_2...x_k)$. Now we apply a refutation method: $\varphi(x_1,x_2...x_k)\Leftrightarrow(\varphi(x_1=1,x_2...x_k)\lor\varphi(x_1=0,x_2...x_k))$. Latter formula seems to ...
3
votes
1answer
334 views

Even, Itai & Shamir's limited backtracking algorithm for 2-SAT: is it really linear?

I have read in Wikipedia (and other sources) about the limited backtracking algorithm of Even, Itai & Shamir for solving 2-SAT problem in a linear time, but the approach doesn't seem to be linear, ...
0
votes
0answers
119 views

When to use SAT vs solving?

Are there any guidelines for how to recognize, for a given problem, which approach is more likely to yield good results? SAT solver or SMT solver? Is there any guidance anyone can offer about which ...
1
vote
1answer
37 views

Paired resolution and $\mathsf{NP}$ vs. $\mathsf{coNP}$?

Let we resolve only two clauses at time and then get rid of them. Such resolution clearly takes $O(n)$ steps. Sequence is a set of instructions in the form $(C_{S_1}\cup C_{S_2},v\cup\overline v),...$...
0
votes
1answer
115 views

Another way to solve SAT. Was it known?

Theorem. If and only if SAT instance $\varphi$ is satisfiable, there is a way to negate variables in $\varphi$ and get $\varphi'$ where all clauses have at least one positive literal. Also we can ...
3
votes
2answers
300 views

Is boolean validity a harder problem than satisfiability?

I am aware that satisfiability is NP complete and unsatisfiability is co-NP complete. But somehow I feel that labeling satisfiability as NP-complete and unsatisfiability as co-NP complete is papering ...
2
votes
1answer
88 views

Unrolling closures into SAT boolean formula

I need to verify some assertions about the minimalist Turing-complete language Jot. Many of the assertions I want to investigate are semi-deciable (co-recursively enumerable). So far it's been fairly ...
1
vote
1answer
77 views

Is it an open problem if generalized resolution is always possible?

Let we have a 3CNF under following restriction: each variable occurs 3 times. Then I apply generalized resolution (GR) (I don't know which name would fit more) technique (number of clauses can be ...
1
vote
1answer
448 views

SAT to knapsack vs. ETH

Theorem states that every problem in $\mathsf{NP}$ can be reduced to another $\mathsf{NP}$-complete problem in polynomial time. Also you can only make a problem polynomially longer using polynomial ...
1
vote
0answers
107 views

Correct implication for 3SAT from this theorem?

Theorem. Let none of the assignments of length $\log n$ make a set of unsatisfiable 2-clauses. Then formula is satisfiable. $n$ is input length here. Let we name an assignment that make the formula ...
2
votes
1answer
101 views

Number of minimal unsatisfiable partial assignments in 2-SAT/3-SAT

A minimal unsatisfiable partial assignment for 3-CNF is a partial assignment that: There exist a clause where all variables are unsatisfied. Unfixing any variable make every clause contain at least ...
1
vote
1answer
151 views

Is generating MIN-3-UNSAT $\mathsf{NP}$-hard?

Input: amount of variables (with minimum of $10$ since otherwise problem is unsolvable). Output: unsatisfiable formula. Restrictions: Every clause contains exactly 3 variables. Every clause differs ...
3
votes
0answers
52 views

What is complexity class for #XOR-2-SAT?

I know that given problem is in $\mathsf{FP}$: if given formula is satisfiable, then it is only needed to find out how many connected components equality (undirected) graph has. In fact problem is to ...
1
vote
1answer
50 views

How 2-QCNF algorithm works?

Suppose we have following 2-QCNF problem: $$\forall x_1...\forall x_m\exists y_1...\exists y_k:\varphi(x_1,...,y_k)$$ where $\varphi$ is 2-CNF. When the formula is false? Rules that I found: $\...
1
vote
1answer
521 views

Is this possible to solve boolean satisfiablility by using karnaugh maps to simplify the whole given boolean formula by simplifying subformulas?

Building karnaugh map for the whole given boolean formula always costs Θ(2n) both time and space complexities, where $n$ is the number of boolean variables in the given boolean formula. It is ...
1
vote
1answer
184 views

monotone min 3-sat polynomial algorithm?

I know that 3SAT is npc but i wonder why my little algorithm won't solve this problem: given positive 3SAT - meaning: each of the m clauses is a disjunction of 3 literals over the variables x1,…,xnx1,...
0
votes
1answer
464 views

Is this possible to solve SAT in polynomial time by reducing it to the problem of solving system of nonlinear equations?

Every conjunctive normal form (CNF) formula can be converted to nonlinear system of equations, where each clause becomes an equation in the system and: If A and B are logical/boolean variables and ...
0
votes
2answers
257 views

monotone min-3-sat polynomial algorithm?

I know that 3SAT is npc but i wonder why my little algorithm won't solve this problem: given positive 3SAT - meaning: each of the m clauses is a disjunction of 3 literals over the variables $x_1,\...
0
votes
1answer
37 views

A Question on SAT

A logical formula is unsatisfiable if and only if for the formula to be true, at least one of its variables must be both true and false. I discovered SAT today, and wanted to try my hands at ...
2
votes
1answer
363 views

Binarization of Constraints

I am trying to solve a Constraint Satisfaction Problem that involves lots of n-ary constraints. But the solver I have implemented only works with algorithms for binary constraints. I've been reading ...
1
vote
1answer
373 views

What is the complexity of determining whether or not conjunction of positive CNF and negative CNF is satisfiable?

Definitions: positive CNF is a conjunctive normal form formula, where all literals are positive, i.e. the unary connective ¬ does not exist in the formula. negative CNF is a conjunctive normal ...
0
votes
1answer
233 views

Proving unsatisfiability of a propositional formula

I have a propositional formula $F$ and an assignment of truth variables $A$. The assignment $A$ assigns a truth value to each variable in $F$ and then it can be evaluated. I have a function which for ...
3
votes
2answers
1k views

CSP Forward checking with n-ary (and binary) constraints

I have implemented my own CSP solver using a Backtracking algorithm. Within the Backtracking algorithm I apply a Forward Checking algorithm (reducing domains of connected, unnasigned variables) that ...
1
vote
1answer
115 views

MAX-2-XOR-SAT: Why does the special case work?

I'm a new user so I cannot respond directly to this post here. I'm confused about the answers to the question, namely that MAX-2-XOR-SAT is in $P$ iff each clause is of the form $(x_i \oplus \neg ...
1
vote
1answer
411 views

Is this possible to solve 4SAT in polynomial time? [closed]

I know and admit that this is long, but please read it slow and understand everything. I think that this is one of the most interesting questions asked in computer science ever. I don't expect for ...
1
vote
4answers
989 views

Is this possible to solve 3SAT in O(n^24) time and O(1) space?

Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different. That means that for each clause, each literal can be either positive ...
3
votes
1answer
417 views

3-SAT and Systems of Nonlinear Modular Equations

How is the 3-SAT problem reduced to solving for a system of nonlinear modular equations? I have read https://stackoverflow.com/questions/4294270/how-to-prove-that-a-problem-is-np-complete in how to ...
0
votes
0answers
95 views

These sample CNF formulas in DIMACS files are in P? (Schaefer's dichotomy theorem)

Here is my earlier question. But there was no full answer. I've decided to include specific DIMACS files: http://jarvis2.hmcloud.pl/sat/cnf.formula.10 (15.8MB) http://jarvis2.hmcloud.pl/sat/cnf....
3
votes
1answer
287 views

Satisfiabililty sufficient condition?

The conjecture itself: k-SAT formula is satisfiable if no pair of unit assignment $l$ and $\overline l$ imply the formula to contain unsatisfiable (k-1)-SAT. Example (XOR-SAT has no edges and cycles ...
6
votes
1answer
57 views

Small world theorem for set constraints

Let $S_1,\dots,S_n$ be variables representing unknown sets. A set expression has the form $S_i$, $\overline{E}$ (the complement of $E$), or $E \cap E'$, where $E,E'$ are set expressions. A ...
1
vote
2answers
1k views

Unique SAT complexity clarification

Unique SAT is defined as: Given any SAT problem, does the SAT problem have exactly 1 solution? As I understand it is co-NPHard. I am unclear how it is in co-NP Assuming the problem has more than 1 ...
1
vote
1answer
62 views

Correctness of following algorithm for 3-QCNF?

Let I have 3-QCNF formula. Classic recursive algorithm for TQBF takes exponential time. However, following divide & conquer modification allows to do it in quadratic time (not sure about ...
3
votes
1answer
45 views

“Insensitive” CNF/DNF SAT always satisfying same number of clauses

I came across this paper, which mentions an interesting variation on SAT: We call a CNF formula F insensitive if every total assignment α satisfies the same number of clauses of F. I hadn't come ...
2
votes
1answer
260 views

Reduction from 2-SAT to 2-XOR-SAT?

2-SAT is unsatisfiable iff it contains unsatisfiable XOR-2-SAT. So, first, we just need to combine every clause that contains share same variables (both of them). Then, all of those which remain ...
0
votes
1answer
54 views

Is following SAT case in $\mathsf{P}$?

...

1 2 3
4
5
9