SAT solver (original) (raw)
In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently.
| Property | Value |
|---|---|
| dbo:abstract | In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently. By a result known as the Cook–Levin theorem, Boolean satisfiability is an NP-complete problem in general. As a result, only algorithms with exponential worst-case complexity are known. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints. SAT solvers often begin by converting a formula to conjunctive normal form. They are often based on core algorithms such as the DPLL algorithm, but incorporate a number of extensions and features. Most SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution with an output such as "unknown". Often, SAT solvers do not just provide an answer, but can provide further information including an example assignment (values for x, y, etc.) in case the formula is satisfiable or minimal set of unsatisfiable clauses if the formula is unsatisfiable. Modern SAT solvers have had a significant impact on fields including software verification, program analysis, constraint solving, artificial intelligence, electronic design automation, and operations research. Powerful solvers are readily available as free and open-source software and are built into some programming languages such as exposing SAT solvers as constraints in constraint logic programming. (en) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Cube_and_Conquer_example.svg?width=300 |
| dbo:wikiPageID | 15409192 (xsd:integer) |
| dbo:wikiPageLength | 21419 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1124843134 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Program_optimization dbr:Electronic_design_automation dbr:Boolean_data_type dbr:Algorithm dbr:Resolution_(logic) dbr:DPLL_algorithm dbr:Free_and_open-source_software dbr:Conflict-driven_clause_learning dbr:Conjunctive_normal_form dbr:Constraint_logic_programming dbr:Constraint_satisfaction_problem dbr:Cook–Levin_theorem dbr:Load_balancing_(computing) dbr:Logical_conjunction dbr:Stochastic dbr:Computer_program dbr:Computer_science dbr:Parallel_algorithm dbr:Distributed_memory dbr:Divide-and-conquer_algorithm dbr:GRASP_(SAT_solver) dbr:Local_search_(constraint_satisfaction) dbr:Central_processing_unit dbr:Formal_methods dbr:Logical_disjunction dbr:Logical_equivalence dbc:Satisfiability_problems dbr:Backjumping dbr:Artificial_intelligence dbc:Formal_methods dbc:Logic_in_computer_science dbr:Binary_decision_diagram dbr:Heuristic dbr:Boolean_Pythagorean_triples_problem dbr:Boolean_satisfiability_problem dbr:OR-Tools dbr:Operations_research dbc:SAT_solvers dbr:Chaff_algorithm dbr:Satisfiability dbr:Satisfiability_modulo_theories dbr:Random_seed dbr:Software dbr:Hardware_verification dbr:Software_verification dbr:Program_analysis dbr:NP-completeness dbr:Shared_memory dbr:Manycore_processors dbr:WalkSAT dbr:Random_number_generation dbr:Hardware_design dbr:Davis–Putnam–Logemann–Loveland_algorithm dbr:"two-watched-literals"_unit_propagation dbr:Chronological_backtracking dbr:Cube-and-Conquer dbr:File:Cube_and_Conquer_example.svg |
| dbp:wikiPageUsesTemplate | dbt:Citation_needed dbt:Main dbt:Reflist dbt:Short_description dbt:Clarify_span |
| dcterms:subject | dbc:Satisfiability_problems dbc:Formal_methods dbc:Logic_in_computer_science |
| rdfs:comment | In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently. (en) |
| rdfs:label | SAT solver (en) |
| owl:sameAs | wikidata:SAT solver https://global.dbpedia.org/id/GEtzK |
| prov:wasDerivedFrom | wikipedia-en:SAT_solver?oldid=1124843134&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Cube_and_Conquer_example.svg |
| foaf:isPrimaryTopicOf | wikipedia-en:SAT_solver |
| is dbo:wikiPageDisambiguates of | dbr:SAT_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Distributed_SAT-solver dbr:SAT-solver dbr:SAT_Solver |
| is dbo:wikiPageWikiLink of | dbr:Belief_revision dbr:Proof_complexity dbr:Propositional_calculus dbr:Proof_compression dbr:Algorithm_selection dbr:DPLL_algorithm dbr:Davis–Putnam_algorithm dbr:Computational_complexity_theory dbr:ZYpp dbr:Hadwiger–Nelson_problem dbr:Hamiltonian_path_problem dbr:Action_model_learning dbr:Lam's_problem dbr:Alt-Ergo dbr:Unsatisfiable_core dbr:Marijn_Heule dbr:Grigori_Tseitin dbr:SAT_(disambiguation) dbr:Distributed_SAT-solver dbr:Multi-agent_pathfinding dbr:Solver dbr:SAT-solver dbr:Twin-width dbr:SAT_Solver |
| is rdfs:seeAlso of | dbr:Proof_complexity |
| is foaf:primaryTopic of | wikipedia-en:SAT_solver |
