Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

115 questions
Filter by
Sorted by
Tagged with
99 views

Find a list of actions that result in desired state

I have a problem that I need to solve, and I'm looking for which area of computer science (algorithms. etc) would be appropriate to solve this problem. In the system we have a list of actions that a ...
37 views

Seeking CNF Encoding with Exponential Lower Bound in Propagation Redundancy [migrated]

I'm exploring the possibility of encoding a proposition in CNF that might have an exponential lower bound for the number of steps needed to prove it unsatisfiable using propagation redundancy. While ...
14 views

Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
1 vote
13 views

Are there ASICs optimized to solve the SAT problem?

Are there ASICs (application-specific integrated circuits) optimized to solve the SAT problem, such as by the DPLL algorithm?
148 views

SAT solvers for counting the number of solutions

Are there existing SAT solver libraries that can count the number of solutions of a boolean formula? Can you give examples? I mean implementations more efficient than the naive approach, i.e. each ...
1 vote
90 views

Sat solvers with backdoor set

I have large cnf with thousands of variables, but with known compact backdoor set. I think this set can be used by CDCL solvers to choose assignment variables to simplify formula much faster, but I ...
1 vote
323 views

1 vote
2k 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 ...
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...