sarsko/CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

Language: Rust - Size: 111 MB - Last synced at: 11 months ago - Pushed at: about 1 year ago - Stars: 591 - Forks: 10

SRI-CSL/yices2

The Yices SMT Solver

Language: SMT - Size: 25.9 MB - Last synced at: 1 day ago - Pushed at: 6 days ago - Stars: 396 - Forks: 55

welchbj/tt

a Pythonic toolkit for working with Boolean expressions

Language: Python - Size: 577 KB - Last synced at: 5 months ago - Pushed at: 6 months ago - Stars: 218 - Forks: 12

circuitgraph/circuitgraph

Tools for working with circuits as graphs in python

Language: Verilog - Size: 10.5 MB - Last synced at: 2 days ago - Pushed at: over 1 year ago - Stars: 115 - Forks: 14

shnarazk/splr

A modern (trail saving, clause subsumption/vivification, learning-rate based selecting, rephrase) CDCL SAT solver in Rust

Language: Rust - Size: 5.06 MB - Last synced at: 11 days ago - Pushed at: 19 days ago - Stars: 91 - Forks: 9

audemard/glucose

The glucose SAT solver

Language: C++ - Size: 387 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 77 - Forks: 15

meelgroup/approxmc

Approximate Model Counter

Language: C++ - Size: 944 KB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 76 - Forks: 26

MatthiasNickles/diff-SAT

Probabilistic Answer Set Programming and Probabilistic SAT solving, based on Differentiable Satisfiability

Language: Scala - Size: 2.24 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 61 - Forks: 3

google/kiwi-solver 📦

Kiwi is a minimalist and extendable Constraint Programming (CP) solver.

Language: Java - Size: 96.7 KB - Last synced at: 4 days ago - Pushed at: almost 6 years ago - Stars: 50 - Forks: 8

biotomas/ipasir

The Standard Interface for Incremental Satisfiability Solving

Language: C++ - Size: 2.18 MB - Last synced at: 12 months ago - Pushed at: almost 3 years ago - Stars: 47 - Forks: 14

triska/clpb

Boolean Constraint Solving in Prolog

Language: Prolog - Size: 305 KB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 39 - Forks: 6

sukrutrao/SAT-Solver-DPLL

A simple SAT solver that implements the DPLL algorithm with unit resolution

Language: C++ - Size: 1.59 MB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 37 - Forks: 20

sukrutrao/Timetabler

A customizable timetabling software for educational institutions that encodes timetabling constraints as a SAT formula and solves them using a MaxSAT solver

Language: C++ - Size: 756 KB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 35 - Forks: 7

NationalSecurityAgency/XORSATFilter

A library for building efficient set-membership filters and dictionaries based on the Satisfiability problem.

Language: C - Size: 57.6 KB - Last synced at: 19 days ago - Pushed at: over 2 years ago - Stars: 33 - Forks: 17

meelgroup/ganak

The first scalable probabilistic exact counter

Language: C++ - Size: 18.9 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 31 - Forks: 9

vsklad/cgen

CGen is a tool for encoding SHA-1 and SHA-256 hash functions into CNF in DIMACS format, also into ANF polynominal system in PolyBoRi output format.

Language: C++ - Size: 234 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 21 - Forks: 5

Thinklab-SJTU/HardSATGEN

[SIGKDD 2023] HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline

Language: Python - Size: 25.9 MB - Last synced at: 15 days ago - Pushed at: almost 2 years ago - Stars: 20 - Forks: 0

maxtuno/slime-sat-solver

A Free World Class High Performance SAT Solver

Language: JavaScript - Size: 285 MB - Last synced at: 3 months ago - Pushed at: almost 4 years ago - Stars: 20 - Forks: 1

hellman/Quine-McCluskey

DenseQMC: A bit-slice implementation of the Quine-McCluskey algorithm

Language: C++ - Size: 5.4 MB - Last synced at: 1 day ago - Pushed at: over 1 year ago - Stars: 15 - Forks: 1

Kapilhk/SatPie

SAT solver based on CDCL in Python with Conflict Driven Clause Learning, clever Heuristics - VSIDS, 2 - Literal watch advanced data structure, Random restarts with restart probability decay

Language: Jupyter Notebook - Size: 1.09 MB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 14 - Forks: 3

sukrutrao/SAT-Solver-CDCL

A simple SAT solver based on the CDCL algorithm

Language: C++ - Size: 91.8 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 14 - Forks: 3

meelgroup/barbarik

The first efficient procedure to test whether a sampler is uniform

Language: Python - Size: 48.3 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 12 - Forks: 1

cipherboy/hash_framework

Framework for studying cryptographic hash functions using SAT.

Language: Python - Size: 923 KB - Last synced at: about 1 hour ago - Pushed at: over 3 years ago - Stars: 10 - Forks: 2

ANU-HPC/dagster

Dagster - Parallel Structured Search for Boolean Satisfiability (SAT) problems

Language: HTML - Size: 31.7 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 9 - Forks: 1

private-yusuke/sat-d 📦

A small SAT solver implementation. 2020年度の情報科学特別演習にて書いたプログラム

Language: D - Size: 1.17 MB - Last synced at: 5 days ago - Pushed at: over 3 years ago - Stars: 9 - Forks: 0

fkutzner/JamSAT

A fast, clean IPASIR SAT solver

Language: C++ - Size: 1.91 MB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 9 - Forks: 0

cipherboy/cmsh

High-level interfaces over @msoos's CryptoMiniSat.

Language: Python - Size: 357 KB - Last synced at: about 4 hours ago - Pushed at: about 1 year ago - Stars: 8 - Forks: 0

sgomber/CDCL-SAT

A SAT Solver based on CDCL (Conflict Driven Clause Learning) implemented in python

Language: Jupyter Notebook - Size: 13.9 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 3

weaversa/MPHF

An efficient minimal perfect hash function generator for small sets

Language: C - Size: 86.9 KB - Last synced at: 14 days ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 2

ZaydH/spur

SAT'18 Paper: SPUR - Satisfying Perfectly Uniform Random sampler (Winner Best Student Paper)

Language: C++ - Size: 127 KB - Last synced at: 11 months ago - Pushed at: about 1 year ago - Stars: 7 - Forks: 1

saeednj/SAT-encoding

Encoding different problems into Boolean satisfiability

Language: C++ - Size: 54.7 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 4

dirkschumacher/rpicosat

PicoSAT bindings for R

Language: R - Size: 90.8 KB - Last synced at: 8 days ago - Pushed at: over 3 years ago - Stars: 7 - Forks: 1

jacky860226/JinkelaSat

A Header-Only CDCL SAT Solver based on MiniSat (Fast and only 500 lines)

Language: C++ - Size: 931 KB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 7 - Forks: 0

ermongroup/streamline-vi-csp

Language: C - Size: 2.32 MB - Last synced at: 23 days ago - Pushed at: over 6 years ago - Stars: 7 - Forks: 2

Daikon-Sun/FRAIG

Functionally Reduced And-Inverter Graph

Language: C++ - Size: 14.3 MB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 6 - Forks: 0

meelgroup/breakid

BreakID, a CNF symmetry-breaking library and tool

Language: C++ - Size: 439 KB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 5 - Forks: 3

fkutzner/PyCSCL

A lightweight CNF SAT constraint encoder library

Language: Python - Size: 221 KB - Last synced at: 2 days ago - Pushed at: over 2 years ago - Stars: 5 - Forks: 1

DevonFulcher/Proof-of-SAT

Generate and solve random instances of MAX-SAT and instances of MAX-SAT that are deterministically and pseudo-randomly generated from the solutions of previous MAX-SAT instances. This is a prototype of how a proof of work algorithm can be derived from a relevant problem.

Language: Python - Size: 11.7 KB - Last synced at: 23 days ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 0

lip6/cosy

Language: C++ - Size: 2.54 MB - Last synced at: 12 days ago - Pushed at: about 4 years ago - Stars: 5 - Forks: 0

MatiasBrizzio/EstiMate

EstiMate 🦉: A fast and accurate modelcounter tool for estimating the number of models for LTL formulas using transfer matrices.

Language: Java - Size: 99.5 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 4 - Forks: 0

marcluque/YASER

Yet Another Sat solvER

Language: C - Size: 23.9 MB - Last synced at: 5 days ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 0

meelgroup/mis

Minimal Independent Set Finder for CNFs

Language: C++ - Size: 1.52 MB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 4 - Forks: 2

ronmrdechai/dimple

A simple SAT solver written in Java

Language: Java - Size: 40 KB - Last synced at: about 1 year ago - Pushed at: almost 6 years ago - Stars: 4 - Forks: 0

MatthiasNickles/Diff-ASP-Propagators

Proof of concept approach to Differentiable Answer Set Programming and Differentiable Satisfiability, for sampling and multimodel optimization. For Clingo (https://potassco.org/) + Python

Language: Answer Set Programming - Size: 24.4 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 3 - Forks: 0

ML-KULeuven/ocus-explain

Efficient Explaining CSPs with Unsatisfiable Subset Optimization

Language: Jupyter Notebook - Size: 14 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 3 - Forks: 0

flopp/gol-sat

A SAT-based forward/backwards solver for Conway's "Game of Life".

Language: C++ - Size: 18.6 KB - Last synced at: about 1 month ago - Pushed at: 11 months ago - Stars: 3 - Forks: 0

MatthiasNickles/fol2asp

A tool for the translation of First-Order Logic (FOL) theories to Answer Set programs (logic programs)

Language: Scala - Size: 66.4 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0

simewu/SAT-solver

A web-based boolean satisfiability solver.

Language: HTML - Size: 1.67 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0

vaibhavkarve/graphsat

A python package that recognizes clauses, Cnfs, graphs, hypergraphs, and multi-hypergraphs. The package implements local graph-rewriting, graph-satchecking, calculation of graph disjunctions, as well as checking of new reduction rules.

Language: Jupyter Notebook - Size: 1.65 MB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 3 - Forks: 2

m1010j/boolean-logic

A lightweight package for evaluating formulas of Boolean logic

Language: JavaScript - Size: 1.04 MB - Last synced at: 3 days ago - Pushed at: almost 5 years ago - Stars: 3 - Forks: 0

dakk/osat

OCaml experimental sat3 solver

Language: OCaml - Size: 51.8 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 3 - Forks: 0

tamura70/taocp-sat

Language: CWeb - Size: 11.6 MB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 0

schwering/sat

SAT solver for education

Language: TeX - Size: 13.1 MB - Last synced at: about 2 months ago - Pushed at: over 6 years ago - Stars: 3 - Forks: 0

aperrault/stable-matching-suite

SAT implementation of stable matching problem with couples and reference implementations of deferred acceptance algorithms.

Language: C++ - Size: 112 KB - Last synced at: about 2 years ago - Pushed at: about 7 years ago - Stars: 3 - Forks: 1

hellman/optisolveapi

Optimization & Solving common API (SAT, MILP, etc.)

Language: Python - Size: 122 KB - Last synced at: 1 day ago - Pushed at: 10 months ago - Stars: 2 - Forks: 0

hellman/optimodel

A suite for minimizing constraint systems (CNF/DNF/MILP inequalities)

Language: Python - Size: 157 KB - Last synced at: 1 day ago - Pushed at: 10 months ago - Stars: 2 - Forks: 1

shnarazk/sudoku_sat

Solving Sudoku variants with SAT solvers

Language: Rust - Size: 211 KB - Last synced at: 11 months ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 0

apurva91/SAT-Solver

CDCL SAT Solver implementation for babies

Language: Jupyter Notebook - Size: 328 KB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 2 - Forks: 0

MatiasBrizzio/N-AI

🧩 Solver for N-Puzzle & N-Queens using Genetic Algorithms, A*, and more in Python

Language: Python - Size: 384 KB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 1 - Forks: 1

toda-lab/pygplib

Pygplib: Python First-Order Graph Property Library

Language: Python - Size: 4.88 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

vvvvvvvector/SAT-solver-graphical-interface-client

SAT-solver graphical interface for Web [client-side]

Language: TypeScript - Size: 21.1 MB - Last synced at: 5 days ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0

jamestiotio/DigiAlpha

Optimized 32-Bit Full Adder, CEC-SAT Verifier & 2-SAT Solver

Language: C++ - Size: 6.96 MB - Last synced at: 12 months ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

JBourton/SatSolver

Implementation of a basic SAT solver, completed as coursework for Durham University

Language: Python - Size: 229 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

os12345678/SAT_DPLL

An implementation of the DPLL algorithm for solving SAT problems

Language: Python - Size: 2.76 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

jeffrey-hokanson/SATyrn

An interface to SAT solvers

Language: C - Size: 87.9 KB - Last synced at: 3 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

vinciusb/proof-visualizer Fork of ufmg-smite/proof-visualizer

A visualizer for proof certificate generated by CVC5, a SMT solver. This website provides customizable views through graphs and tables that allow a better understanding of certificates and the operation of SMT solvers.

Language: TypeScript - Size: 41.4 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

opensat/LovaszSAT

A naive implementation of Algorithmic Lovász local lemma.

Language: Python - Size: 1.95 KB - Last synced at: 12 months ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

Arvind-kumar-M-08/AI-CS-312-lab

Artificial Intelligence Lab

Language: Python - Size: 1.67 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 2

DerEasy/Propositional-Calculator

Console application for calculating propositional calculus formulas. Can create truth tables, show steps to result, check for validity, etc. Programmed in C#.

Language: C# - Size: 7.04 MB - Last synced at: almost 2 years ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0

mrtkp9993/MathProg

Automated theorem proving, Logic Programming, Optimization examples.

Language: Python - Size: 24.4 KB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0

pgphi/Logic-based-SAT-Clause-Creater

This algorithms computes the clauses needed, to solve Minesweeper and check for satisfiability

Language: Python - Size: 1.98 MB - Last synced at: over 1 year ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0

fkutzner/IncrementalMonkey

A random testing tool for IPASIR SAT solvers

Language: C++ - Size: 436 KB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0

prateekkumarweb/sat-verifier

Verifies SAT solver output. Uses drat-trim proof checker for UNSAT instances.

Language: C - Size: 19.5 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0

GavinPHR/SAT-with-Haskell

Haskell Implementation of DPLL + Sudoku with SAT

Language: Haskell - Size: 2.22 MB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0

Groenbech96/SAT

Satisfiability solver

Language: C++ - Size: 9.52 MB - Last synced at: 10 months ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

ben-marshall/sat-solver

A simple combinatorial boolean sat solver based on the AC-3 Algorithm

Language: C - Size: 156 KB - Last synced at: about 1 month ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 1

SleekPanther/3-sat-certifier

A Certifier algorithm to check a particular solution to the NP-Complete 3-Sat problem

Language: Java - Size: 16.6 KB - Last synced at: about 2 months ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 1

NikhilGupta1997/SAT-Graph-Mapping

Check to see if a mapping exists between 2 graphs (subgraph-isomorphism) by developing optimised SAT clauses and solving them using MINISAT.

Language: C++ - Size: 67.4 KB - Last synced at: almost 2 years ago - Pushed at: over 8 years ago - Stars: 1 - Forks: 1

fisherlyon/SAT_SeniorProject

Work in progress...

Language: Racket - Size: 24.5 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 0 - Forks: 0

lumusit/lumusit

Contate-nos: [email protected]

Size: 1000 Bytes - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 0 - Forks: 0

tchaumeny/satisfaction

Investigate phase transitions in k-SAT problems

Language: Rust - Size: 87.9 KB - Last synced at: about 1 month ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

calebnwokocha/Satisfier

This project is a satisfiability checker that works with formulas in conjunctive normal form.

Language: Go - Size: 3.16 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

afifabroory/SudokuAreEz-SAT

SudokuAreEz-SAT are project implement Mathematics Logic using Boolean Satisfiability to solve Sudoku puzzle.

Language: Python - Size: 297 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0

fkutzner/lingeling-cmake Fork of arminbiere/lingeling

Lingeling SAT Solver fork with CMake build

Language: C - Size: 268 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

leabrodyheine/Mosaic-Game-Logical-Agents

This project implements an intelligent agent to solve the Mosaic logic puzzle using strategies such as Single Point Strategy, Satisfiability Test Reasoning (with DNF and CNF encoding), and Probabilistic Reasoning. It utilizes frameworks and libraries including Java, LogicNG, and SAT4J for logical reasoning and satisfiability problems.

Language: Java - Size: 1.77 MB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

vvvvvvvector/SAT-solver-graphical-interface-server

SAT-solver graphical interface for Web [server-side]

Language: Python - Size: 36.1 KB - Last synced at: 5 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

centauri2718/estsat

Converts a CNF formula into a mathematical formula so that numerical and algebraic operations can be preformed on it.

Language: C++ - Size: 241 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

MatthiasNickles/Satalyzer

A lightweight tool for the visualization and analysis of event log files (JSON format) generated by SAT, ASP, SMT and other kinds of constraint solvers

Language: Scala - Size: 479 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

Jakob-Bach/Predicting-SAT

Code and text for the suspended paper/project "Predicting Satisfiability of Benchmark Instances".

Language: TeX - Size: 52.7 KB - Last synced at: 12 months ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

lou1306/plancksat

Just good ol' minisat with some quality of life improvements and weak/strong assumptions

Language: C++ - Size: 132 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

oliverdantzer/CISC204_project Fork of ajsib/CISC204_project

Model the card game Yaniv in predicate logic. Project for Queen's University course CISC/CMPE 204: Logic for Computing Science.

Language: Python - Size: 4.51 MB - Last synced at: 12 months ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0

lucasferreiraz/logisat

🧠 Classification of pathologies column using propositional logic satisfiability algorithms.

Language: Java - Size: 144 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

dgerod/CBTs-Checker Fork of EGiunchiglia/CBTs-Checker

Tool to check if a conditional behavior tree (CBT) is valid

Language: C++ - Size: 16.2 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

EnricoPittini/Two-dimensional-strip-packing-problem

Solving the two-dimensional strip packing problem, using several combinatorial decision making and optimization approaches: Constraint Programming, Boolean SATisfiability, Satisfiability Modulo Theory; Integer Linear Programming.

Language: Python - Size: 22.3 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 1

noahbass/scheduler-sat

Using a SAT solver to prove correctness of schedules given a list of constraints.

Language: Python - Size: 17.6 KB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

ablanco1950/BFS-no-conventional

BFS-no-conventional Search according to the BFS algorithm according to an "unconventional" method, meaning the conventional one that is downloaded from http://www.paulgraham.com/acl.html link to code file acl2.lisp. In this "unconventional" version, all the paths that lead to the objective are obtained following the BFS strategy, not only the first path, which will be the shortest. Since there may be several paths that are the shortest, apart from facilitating the case in which the branches are weighted and only the shortest path is not decisive. A program BFS-no-conventional-only-first-path.cl is also provided that obtains only the first path that reaches the target (actually it is the same program in which the value of the option parameter has been modified). The result is an increase in time but a significant reduction in the memory occupied, which is useful in the case of large graphs. The code has some lack of "orthodoxy", such as the use of global variables. Requirements: Allegro CL 10.1 Free Express Edition The programs are loaded, the code is selected and Tools Incremental Evaluation is given. The test cases are then selected and Tools Incremental Evaluation is given again. References: ANSI Common Lisp by Paul Graham. http://www.paulgraham.com/acl.html link to code, file acl2.lisp Diverse material of practices of the subject of Artificial Intelligence of the Polytechnic School Superior, Computer Engineering, of the Autonomous University of Madrid.

Language: Common Lisp - Size: 6.84 KB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

ablanco1950/SAT_propositional_logical_inference

SAT_propositional_logical_inference Obtaining the satisfaction of a knowledge base by a different procedure from the conventional one. Currently, it is usually passed from an expression in FBF (well-formed formula with literals separated by the connectors =>, <=> , v, ^, ¬ and parentheses) to an expression in FNC composed of clauses (literals separated by the or v operator) joined by the and ^ operator, following many steps: substitution of expressions joined by the => connectors by their equivalent Boolean expression, application of Morgan's laws ... etc. The method followed in this application is: A new variable PPNIL is “created”, which the application considers as NIL but which prevents Lisp from considering it as NIL with the consequences it has in handling lists of considering it as an end of list. The values of each literal are substituted for T or PPNIL as they correspond to True or Nil in the composition of literals to be tested. The following rules apply. Connector separated literals => The expressions are True: T => T PPNIL => T PPNIL => PPNIL And Nil the rest. Literals separated by connector  The expressions are True: TT PPNILPPNIL And Nil the rest In the case of expressions joined by the v (or) connector, it is enough that one of the elements is T for it to consider the expression a T. In the case of connector ^ (and), it is enough that one of the variables is PPNIL for the expression to be considered false, that is, PPNIL. All this is done in the function valora-proposición-reducida-T-NIL (propos) function that determines whether a statement reduced to values T and PPNIL is true or false. As soon as it finds a list, it makes a recursive call to itself to obtain the T or PPNIL evaluation of the list. The function encuentra-modelos-p (kb) is the most important since it not only determines if the expression Kb that is passed to it is true or false, but it also gives the list of variables (interpretations) with T or PPNIL values that satisfy them . To do this, it uses the function extrae-simbolos( kb), which generates a list with all the possible values of the variables of the expression; genera-lista-interpretaciones, which generates all the possible combinations of variable values that can be given with T and PPNIL; and explora-todas-interpretaciones , listB kb, that successively calls interpretacion-modelo-p to check if it meets the interpretation of variable values to be passed. It is a "brute force" calculation system, it checks all the possibilities of assigning variables, so it is slower than systems that use DPLL (https://github.com/ablanco1950/DPLL_propositional_logical_inference) By using string handling functions in Lisp, the slowness is increased. Another notable function is reduce-T-NIL-proposicion (propos lst-reductor) function that receives expressions and converts variables to T or PPNIL values instead of variables. Use string handling functions in Lisp. If there is a list, it is called recursively to see the values in T or PPNIL of each of the variables. It uses the ls-reductor list that assigns each variable a T or PPNIL value TESTS: The tests have been implemented based on the examples that appear in the README.md, section 7, of https://github.com/bertuccio/inferencia-logica-proposicional Also based on the examples that appear in a link to netlogo that appears in http://www.cs.us.es/~fsancho/?e=120. Requirements: Allegro CL 10.1 Free Express Edition References: https://github.com/bertuccio/inferencia-logica-proposicional by Adrián Lorenzo Mateo (Bertuccio) who uses material from the Artificial Intelligence practices at the Higher Polytechnic School of the Autonomous University of Madrid. Informatics Engineering. http://www.cs.us.es/~fsancho/?e=120 by Fernando Sancho Caparrini. Higher Technical School of Computer Engineering of the University of Seville. https://github.com/ablanco1950/DPLL_propositional_logical_inference

Language: Common Lisp - Size: 11.7 KB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

ablanco1950/DPLL_propositional_logical_inference

DPLL_propositional_logical_inference: Starting from a FNC (Conjunctive Normal Form), that is, a series of clauses (literals joined by the or operator) joined by an and operator. Apply the DPLL algorithm and determine the values ​​of the literals that give a solution to the FNC. A clear explanation of the DPLL algorithm can be found at http://www.cs.us.es/~fsancho/?e=120. The tests have been implemented based on the examples that appear in a link to netlogo on that page. If you have an expedition in FBC (with connectors => and <=>) you can switch to an FNC, which would be the entrance to this project, downloading the https://github.com/bertuccio/inferencia-logica-proposicional project. This project can be completed with the DPLL algorithm by adding the instructions given from the definition of the DPLL function to the end. And activating the instructions that appear in the function pasa-lista-FBF-to-lista-FNC that would serve as an interface between both projects. In fact, DPLL_propositional_logical_inference is intended to complete Propositional Logical Inference, with the DPLL algorithm and share functions. Requirements: Allegro CL 10.1 Free Express Edition References: https://github.com/bertuccio/inferencia-logica-proposicional by Adrián Lorenzo Mateo (Bertuccio) who uses material from the Artificial Intelligence practices at the Higher Polytechnic School of the Autonomous University of Madrid. Informatics Engineering. http://www.cs.us.es/~fsancho/?e=120 by Fernando Sancho Caparrini. Higher Technical School of Computer Engineering of the University of Seville.

Language: Common Lisp - Size: 8.79 KB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

AnsgarKlein/DPLL-SAT-Solver

Implementation of the DPLL algorithm for solving the satisfiability problem of propositional logic

Language: C - Size: 175 KB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0

solhop/msat 📦

MaxSAT Solver

Language: Rust - Size: 13.7 KB - Last synced at: 11 months ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0