lambda-sat-solver/CITATION.cff at main · jesusvilela/lambda-sat-solver · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
cff-version: 1.2.0
message: "If you use this software or its research notes, please cite it as below."
title: "λSAT — certified λ-logic SAT middleware and a research harness for frame-structured SAT hardness"
abstract: >-
  A headless, certified Boolean-satisfiability middleware: it decides formulas via
  three sound, engine-independent frames (implication/2-SAT, parity/GF(2),
  counting/cardinality) and their coupling, falling back to a DRAT-certified CDCL
  engine only when no frame applies. Every verdict is independently checked (SAT by
  model replay, UNSAT by a sound frame refutation or a drat-trim proof). On top sits
  a research program on the intrinsic geometry of SAT hardness — a hyperbolic
  instance-manifold, a game-theoretic dispatcher, and an explicit proven/measured/
  speculative claim ledger.
type: software
authors:
  - family-names: "Vilela Franco"
    given-names: "Jesús"
repository-code: "https://github.com/jesusvilela/lambda-sat-solver"
url: "https://github.com/jesusvilela/lambda-sat-solver"
license: MIT
version: "0.1.0"
message: "If you use this software, please cite it using the metadata from this file."
title: "lambda-sat-solver: Certified SAT middleware and frame-structured hardness research harness"
authors:
  - family-names: "Vilela Jato"
    given-names: "Jesus"
repository-code: "https://github.com/jesusvilela/lambda-sat-solver"
license: "MIT"
type: software
abstract: >-
  A certified SAT middleware around external CDCL engines, with SAT verdicts checked by
  model replay and UNSAT verdicts checked by sound frame refutation or independent DRAT
  proof replay. The repository also contains a research harness for frame-structured SAT
  hardness, including implication, parity, counting, coupled-frame routing, and scoped
  benchmark reports.
keywords:
  - SAT
  - satisfiability
  - certified solving
  - DRAT proof checking
  - computational complexity
  - resolution width
  - Nullstellensatz degree
  - lambda calculus
references:
  - type: article
    authors:
      - family-names: "Ben-Sasson"
        given-names: "Eli"
      - family-names: "Wigderson"
        given-names: "Avi"
    title: "Short proofs are narrow — resolution made simple"
    year: 2001
  - type: article
    authors:
      - family-names: "Clegg"
        given-names: "Matthew"
      - family-names: "Edmonds"
        given-names: "Jeffery"
      - family-names: "Impagliazzo"
        given-names: "Russell"
    title: "Using the Groebner basis algorithm to find proofs of unsatisfiability"
    year: 1996
  - type: article
    authors:
      - family-names: "Gomes"
        given-names: "Carla P."
      - family-names: "Selman"
        given-names: "Bart"
    title: "Heavy-tailed phenomena in satisfiability and constraint satisfaction problems"
    year: 2000
  - DRAT
  - CDCL
  - proof checking
  - SAT hardness
  - portfolio solving