arxiv: 2605.09347 · v1 · submitted 2026-05-10 · 💻 cs.AI · cs.LO

Recognition: 2 theorem links

· Lean Theorem

Dsat: A Native SAT Solver for Discrete Logic

Yaofang Zhang , Ken Zhou , Adnan Darwiche

Authors on Pith no claims yet

Pith reviewed 2026-05-12 03:53 UTC · model grok-4.3

classification 💻 cs.AI cs.LO

keywords discrete logicSAT solverunit resolutionclause learningCSP solverbinarizationconjunctive normal formsymbolic reasoning

0 comments

The pith

A native SAT solver extends unit resolution and clause learning to operate directly on discrete variables.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a SAT solver that works natively on discrete logic, where variables can take arbitrary values rather than being restricted to true or false. This avoids the standard practice of binarizing discrete variables into Boolean ones, which introduces both computational overhead and potential loss of semantic information in domains such as planning and probabilistic reasoning. The solver adapts core Boolean SAT techniques like unit resolution and clause learning to function directly on discrete domains while preserving a similar overall design. Empirical comparisons position the native solver against CSP solvers on discrete CNFs, Boolean SAT solvers on binarized CNFs, and hybrid approaches.

Core claim

We develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables.

What carries the argument

Native unit resolution and clause learning that operate directly on discrete variables within CNF formulas.

Load-bearing premise

The native discrete versions of unit resolution and clause learning can be implemented efficiently enough to outperform CSP solvers on discrete CNFs and Boolean SAT solvers on binarized versions.

What would settle it

A set of discrete-logic benchmark problems on which the native solver is slower than both CSP solvers applied directly and Boolean SAT solvers applied to binarized versions would falsify the performance claim.

read the original abstract

Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper builds a native SAT solver for discrete variables by generalizing unit resolution and clause learning, but the efficiency advantage over binarization remains unproven without implementation details.

read the letter

The core contribution is a direct lift of CDCL-style mechanisms to finite-domain variables instead of encoding them as Booleans. Unit resolution and clause learning are redefined to operate on value sets rather than true/false, which sidesteps the semantic distortions that binarization can introduce in planning or probabilistic tasks. The design stays close enough to Boolean solvers that the same learning heuristics and data structures can be reused with modest changes. That is the part worth paying attention to if you work in SAT-based AI reasoning. The empirical section runs the right comparisons: against CSP solvers on native discrete CNFs, against Boolean SAT on binarized versions, and against a couple of hybrids. Those baselines make the results interpretable. If the reported speedups hold, the approach could reduce variable blow-up in applications where domain sizes are moderate. The main soft spot is the lack of concrete evidence on overhead. For domain size d greater than 2, maintaining reduced domains or generalizing watched literals is likely to cost more than the constant-time Boolean case, and the abstract gives no data structures, complexity statements, or per-instance timings to show the net gain. Without those, it is difficult to tell whether the native version actually beats a well-tuned binarized solver on larger problems. The paper also does not include a formal argument that the new rules preserve soundness and completeness, which is standard for solver papers. This work is aimed at people who already use SAT or CSP solvers inside AI systems and want to avoid encoding tricks. A reader who needs a new primitive for discrete reasoning will find the idea useful even if the current experiments are preliminary. It is worth sending to referees because the algorithmic idea is coherent and the motivation is real; the review process can press for the missing implementation and scaling details.

Referee Report

2 major / 2 minor

Summary. The paper introduces Dsat, a native SAT solver for discrete logic that directly extends Boolean SAT to variables taking values from arbitrary finite domains. It adapts core Boolean SAT techniques such as unit resolution and clause learning to operate natively on discrete variables rather than requiring binarization, and illustrates the approach via empirical comparisons against CSP solvers on discrete CNFs, Boolean SAT solvers on binarized CNFs, and hybrid solvers.

Significance. If the native discrete operations can be implemented with efficiency comparable to Boolean SAT (without hidden O(d) overheads for domain size d), the work could meaningfully advance symbolic reasoning in domains such as planning, probabilistic inference, and explainable AI by preserving semantics and avoiding binarization artifacts. The reuse of established SAT architecture (unit propagation, clause learning) is a clear strength that facilitates adoption.

major comments (2)

[Abstract / Solver Design] Abstract and solver-design description: the central claim that native unit resolution and clause learning outperform both CSP solvers on discrete CNFs and Boolean SAT on binarized versions rests on the assumption that these operations incur no new semantic or computational overhead. No complexity analysis or data-structure details (e.g., representation of allowed value sets or generalization of watched literals) are supplied, leaving open the possibility that domain maintenance costs O(d) per step and negates the claimed advantage.
[Empirical Evaluation] Empirical evaluation: the abstract states that merits are illustrated by comparisons, yet no concrete performance numbers, instance characteristics (domain sizes, number of variables), or statistical significance tests are referenced. Without these, the load-bearing claim of practical superiority cannot be assessed.

minor comments (2)

[Abstract] Clarify in the abstract and introduction that 'arbitrary values' are restricted to finite discrete domains; the current phrasing risks misinterpretation.
[Related Work] Ensure the related-work section explicitly positions the contribution relative to existing multi-valued SAT or generalized CSP solvers to avoid overlap claims.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thoughtful and constructive report. We address each major comment below and describe the revisions we will undertake.

read point-by-point responses

Referee: [Abstract / Solver Design] Abstract and solver-design description: the central claim that native unit resolution and clause learning outperform both CSP solvers on discrete CNFs and Boolean SAT on binarized versions rests on the assumption that these operations incur no new semantic or computational overhead. No complexity analysis or data-structure details (e.g., representation of allowed value sets or generalization of watched literals) are supplied, leaving open the possibility that domain maintenance costs O(d) per step and negates the claimed advantage.

Authors: We agree that the abstract and the high-level solver-design description do not supply the requested complexity analysis or low-level data-structure details. This is a fair observation. In the revised manuscript we will add a dedicated subsection (placed after the current solver-design section) that (i) specifies the representation of allowed value sets, (ii) describes the generalization of watched literals to discrete domains, and (iii) provides a formal complexity argument showing that the core propagation and learning steps remain O(1) amortized per operation with no hidden linear dependence on domain size d. revision: yes
Referee: [Empirical Evaluation] Empirical evaluation: the abstract states that merits are illustrated by comparisons, yet no concrete performance numbers, instance characteristics (domain sizes, number of variables), or statistical significance tests are referenced. Without these, the load-bearing claim of practical superiority cannot be assessed.

Authors: We acknowledge that the abstract itself contains no numerical results or instance statistics. The full experimental section already reports runtime tables, domain sizes, variable counts, and the benchmark suite used. To improve accessibility we will (a) insert a short summary sentence with representative numbers into the abstract and (b) add an explicit statement on statistical significance testing in the evaluation section. revision: partial

Circularity Check

0 steps flagged

No significant circularity in the native discrete SAT solver design

full rationale

The paper presents the development of a native SAT solver for discrete logic as a direct algorithmic extension of Boolean SAT solvers, featuring unit resolution and clause learning adapted to operate on discrete variables rather than through binarization. This is framed as a design contribution whose merits are illustrated via empirical comparisons to CSP solvers, Boolean SAT on binarized instances, and hybrids. No load-bearing derivation chain, equations, fitted parameters renamed as predictions, or self-citations that reduce the central claims to prior inputs by construction are present. The approach relies on new native operations whose efficiency is an open empirical question, not a self-referential definition or imported uniqueness theorem.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the assumption that discrete logic is a straightforward semantic extension of Boolean logic and that standard SAT ingredients can be lifted without new foundational axioms. No free parameters or invented entities are described in the abstract.

axioms (2)

domain assumption Discrete logic is a direct extension of Boolean logic where variables take arbitrary discrete values.
Stated in the abstract as the basis for the native solver design.
domain assumption Unit resolution and clause learning can be adapted to operate natively on discrete variables while preserving soundness.
Core design claim of the solver; no proof or reference supplied in abstract.

pith-pipeline@v0.9.0 · 5445 in / 1458 out tokens · 49468 ms · 2026-05-12T03:53:38.258700+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

A lazy algorithm... each literal that is being watched must also watch one of its states... pruning a state s of some variable X amounts to removing s from all X-literals

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

57 extracted references · 57 canonical work pages

[1]

SAT and SMT technology for many-valued logics

Carlos Ans \'o tegui, Miquel Bofill, Felip Many \`a , and Mateu Villaret. SAT and SMT technology for many-valued logics. Journal of Multiple-Valued Logic & Soft Computing , 2015

work page 2015
[2]

Mapping CSP into many-valued SAT

Carlos Ans \' o tegui, Maria Luisa Bonet, Jordi Levy, and Felip Many \` a . Mapping CSP into many-valued SAT . In Jo \ a o Marques - Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings , volume 4501 of Lecture Notes in Computer Sci...

work page doi:10.1007/978-3-540-72788-0 2007
[3]

On the computational intelligibility of Boolean classifiers

Gilles Audemard, Steve Bellart, Louenas Bounia, Fr \' e d \' e ric Koriche, Jean - Marie Lagniez, and Pierre Marquis. On the computational intelligibility of Boolean classifiers. In KR , pages 74--86, 2021

work page 2021
[4]

On tractable XAI queries based on compiled representations

Gilles Audemard, Fr \' e d \' e ric Koriche, and Pierre Marquis. On tractable XAI queries based on compiled representations. In KR , pages 838--849, 2020

work page 2020
[5]

Proceedings of the 2023 XCSP3 competition

Gilles Audemard, Christophe Lecoutre, and Emmanuel Lonca. Proceedings of the 2023 XCSP3 competition. CoRR , abs/2312.05877, 2023

work page arXiv 2023
[6]

Predicting learnt clauses quality in modern sat solvers

Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In IJCAI , volume 9, pages 399--404, 2009

work page 2009
[7]

Refining restarts strategies for sat and unsat

Gilles Audemard and Laurent Simon. Refining restarts strategies for sat and unsat. In Michela Milano, editor, Principles and Practice of Constraint Programming , pages 118--126, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg

work page 2012
[8]

On the glucose sat solver

Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools , 27(01):1840001, 2018. https://doi.org/10.1142/S0218213018400018 doi:10.1142/S0218213018400018

work page doi:10.1142/s0218213018400018 2018
[9]

a ckstr \

Christer B \"a ckstr \"o m and Bernhard Nebel. Complexity results for sas+ planning. Computational Intelligence , 11(4):625--655, 1995

work page 1995
[10]

Sat race 2015

Tomáš Balyo, Armin Biere, Markus Iser, and Carsten Sinz. Sat race 2015. Artificial Intelligence , 241:45--65, 2016. https://doi.org/10.1016/j.artint.2016.08.007 doi:10.1016/j.artint.2016.08.007

work page doi:10.1016/j.artint.2016.08.007 2015
[11]

The SAT problem of signed CNF formulas

Bernhard Beckert, Reiner H \"a hnle, and Felip Manya. The SAT problem of signed CNF formulas. In Labelled Deduction , pages 59--80. Springer, 2000

work page 2000
[12]

CaDiCaL 2.0

Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0 . In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I , volume 14681 of Lecture Notes in Computer Science , pages 133--152. ...

work page doi:10.1007/978-3-031-65627-9 2024
[13]

Cadical, gimsatul, isasat and kissat entering the sat competition 2024

Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical, gimsatul, isasat and kissat entering the sat competition 2024. Proc. of SAT Competition , 8, 2024

work page 2024
[14]

Gimsatul , IsaSAT and Kissat entering the SAT Competition 2022

Armin Biere and Mathias Fleury. Gimsatul , IsaSAT and Kissat entering the SAT Competition 2022 . In Tomas Balyo, Marijn Heule, Markus Iser, Matti J \"a rvisalo, and Martin Suda, editors, Proc. of SAT Competition 2022 -- Solver and Benchmark Descriptions , volume B-2022-1 of Department of Computer Science Series of Publications B , pages 10--11. University...

work page 2022
[15]

On probabilistic inference by weighted model counting

Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artif. Intell. , 172(6-7):772--799, 2008

work page 2008
[16]

On symbolically encoding the behavior of random forests

Arthur Choi, Andy Shih, Anchal Goyanka, and Adnan Darwiche. On symbolically encoding the behavior of random forests. CoRR , abs/2007.01493, 2020

work page arXiv 2007
[17]

A logical approach to factoring belief networks

Adnan Darwiche. A logical approach to factoring belief networks. In KR , pages 409--420. Morgan Kaufmann, 2002

work page 2002
[18]

Logic for explainable AI

Adnan Darwiche. Logic for explainable AI . In LICS , pages 1--11, 2023

work page 2023
[19]

On the computation of necessary and sufficient explanations

Adnan Darwiche and Chunxi Ji. On the computation of necessary and sufficient explanations. In AAAI , pages 5582--5591. AAAI Press, 2022

work page 2022
[20]

Complete algorithms

Adnan Darwiche and Knot Pipatsrisawat. Complete algorithms. In Handbook of Satisfiability , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 101--132. IOS Press, 2021

work page 2021
[21]

Towards a better understanding of the functionality of a conflict-driven sat solver

Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. Towards a better understanding of the functionality of a conflict-driven sat solver. In Jo \ a o Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing -- SAT 2007 , pages 287--293, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg

work page 2007
[22]

Effective preprocessing in sat through variable and clause elimination

Niklas E \'e n and Armin Biere. Effective preprocessing in sat through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing , pages 61--75, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg

work page 2005
[23]

An extensible sat-solver

Niklas E \'e n and Niklas S \"o rensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing , pages 502--518, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg

work page 2004
[24]

The silent (r) evolution of sat

Johannes K Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r) evolution of sat. Communications of the ACM , 66(6):64--72, 2023

work page 2023
[25]

data mining: Practical machine learning tools and techniques

Eibe Frank, Mark A Hall, and Ian H Witten. The weka workbench. online appendix for" data mining: Practical machine learning tools and techniques". 2016

work page 2016
[26]

Increasing tree search efficiency for constraint satisfaction problems

Robert M Haralick and Gordon L Elliott. Increasing tree search efficiency for constraint satisfaction problems. Artificial intelligence , 14(3):263--313, 1980

work page 1980
[27]

The fast downward planning system

Malte Helmert. The fast downward planning system. Journal of Artificial Intelligence Research , 26:191--246, 2006

work page 2006
[28]

From contrastive to abductive explanations and back again

Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Jo \ a o Marques - Silva. From contrastive to abductive explanations and back again. In AI*IA , volume 12414 of Lecture Notes in Computer Science , pages 335--355. Springer, 2020

work page 2020
[29]

Abduction-based explanations for machine learning models

Alexey Ignatiev, Nina Narodytska, and Jo \ a o Marques - Silva. Abduction-based explanations for machine learning models. In Proceedings of the Thirty-Third Conference on Artificial Intelligence ( AAAI ) , pages 1511--1519, 2019

work page 2019
[30]

Towards universally accessible sat technology

Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible sat technology. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) , pages 16--1. Schloss Dagstuhl--Leibniz-Zentrum f \"u r Informatik, 2024

work page 2024
[31]

A complete multi-valued SAT solver

Siddhartha Jain, Eoin O'Mahony, and Meinolf Sellmann. A complete multi-valued SAT solver. In David Cohen, editor, Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings , volume 6308 of Lecture Notes in Computer Science , pages 281--296. Springer, 2...

work page doi:10.1007/978-3-642-15396-9 2010
[32]

A new class of explanations for classifiers with non-binary features

Chunxi Ji and Adnan Darwiche. A new class of explanations for classifiers with non-binary features. In JELIA , volume 14281 of Lecture Notes in Computer Science , pages 106--122. Springer, 2023

work page 2023
[33]

Circuit representations of random forests with applications to xai

Chunxi Ji and Adnan Darwiche. Circuit representations of random forests with applications to xai. In The 4th World Conference on Explainable Artificial Intelligence . Springer Nature Switzerland, 2026. https://arxiv.org/abs/2602.08362 arXiv:2602.08362

work page arXiv 2026
[34]

Kautz and Bart Selman

Henry A. Kautz and Bart Selman. Planning as satisfiability. In Bernd Neumann, editor, 10th European Conference on Artificial Intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings , pages 359--363. John Wiley and Sons, 1992

work page 1992
[35]

A cardinality solver: more expressive constraints for free

Mark H Liffiton and Jordyn C Maglalang. A cardinality solver: more expressive constraints for free. In International Conference on Theory and Applications of Satisfiability Testing , pages 485--486. Springer, 2012

work page 2012
[36]

Moskewicz

Cong Liu, Andreas Kuehlmann, and Matthew W. Moskewicz. CAMA: A multi-valued satisfiability solver. In 2003 International Conference on Computer-Aided Design, ICCAD 2003, San Jose, CA, USA, November 9-13, 2003 , pages 326--333. IEEE Computer Society / ACM , 2003. https://doi.org/10.1109/ICCAD.2003.1257732 doi:10.1109/ICCAD.2003.1257732

work page doi:10.1109/iccad.2003.1257732 2003
[37]

An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers *

Mao Luo, Chu-Min Li, Fan Xiao, Felip Many \`a , and Zhipeng L \"u . An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers * . In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI-17) , pages 703--711, Melbourne, Australia, August 2017. URL: https://hal.science/hal-04321762

work page 2017
[38]

Marques Silva and K.A

J.P. Marques Silva and K.A. Sakallah. Grasp-a new search algorithm for satisfiability. In Proceedings of International Conference on Computer Aided Design , pages 220--227, 1996. https://doi.org/10.1109/ICCAD.1996.569607 doi:10.1109/ICCAD.1996.569607

work page doi:10.1109/iccad.1996.569607 1996
[39]

Chaff: Engineering an efficient sat solver

Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference , pages 530--535, 2001

work page 2001
[40]

Chronological backtracking

Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In International Conference on Theory and Applications of Satisfiability Testing , pages 111--121. Springer, 2018

work page 2018
[41]

Minizinc: Towards a standard cp modelling language

Nicholas Nethercote, Peter J Stuckey, Ralph Becket, Sebastian Brand, Gregory J Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In International conference on principles and practice of constraint programming , pages 529--543. Springer, 2007

work page 2007
[42]

The CP-SAT-LP solver (invited talk)

Laurent Perron, Fr \' e d \' e ric Didier, and Steven Gay. The CP-SAT-LP solver (invited talk). In CP , volume 280 of LIPIcs , pages 3:1--3:2. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2023

work page 2023
[43]

Laurent Perron and Frédéric Didier. Cp-sat. URL: https://developers.google.com/optimization/cp/cp_solver/

work page
[44]

Vivifying propositional clausal formulae

C \'e dric Piette, Youssef Hamadi, and Lakhdar Sais. Vivifying propositional clausal formulae. In ECAI , volume 178, pages 525--529, 2008

work page 2008
[45]

A lightweight component caching scheme for satisfiability solvers

Knot Pipatsrisawat and Adnan Darwiche. A lightweight component caching scheme for satisfiability solvers. In SAT , volume 4501 of Lecture Notes in Computer Science , pages 294--299. Springer, 2007

work page 2007
[46]

A new clause learning scheme for efficient unsatisfiability proofs

Knot Pipatsrisawat and Adnan Darwiche. A new clause learning scheme for efficient unsatisfiability proofs. In AAAI , pages 1481--1484. AAAI Press, 2008

work page 2008
[47]

Choco-solver

Charles Prud’homme and Jean-Guillaume Fages. Choco-solver. Journal of Open Source Software , 7(78):4708, 2022

work page 2022
[48]

Planning and sat

Jussi Rintanen. Planning and sat. In Handbook of Satisfiability: Second Edition , pages 765--789. IOS Press, 2021

work page 2021
[49]

A symbolic approach to explaining bayesian network classifiers

Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In IJCAI , pages 5103--5111. ijcai.org, 2018

work page 2018
[50]

Minimizing learned clauses

Niklas S \"o rensson and Armin Biere. Minimizing learned clauses. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009 , pages 237--243, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg

work page 2009
[51]

Peter J. Stuckey. Lazy clause generation: Combining the power of SAT and CP (and mip?) solving. In CPAIOR , volume 6140 of Lecture Notes in Computer Science , pages 5--9. Springer, 2010

work page 2010
[52]

Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer

Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. The minizinc challenge 2008-2013. AI Mag. , 35(2):55--60, 2014

work page 2008
[53]

An efficient algorithm for unit propagation

Hantao Zhang and Mark Stickel. An efficient algorithm for unit propagation. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics , 96, 1996

work page 1996
[54]

Madigan, Matthew W

Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in boolean satisfiability solver. In ICCAD , pages 279--285. IEEE Computer Society, 2001

work page 2001
[55]

The picat-sat compiler

Neng - Fa Zhou and H kan Kjellerstrand. The picat-sat compiler. In PADL , volume 9585 of Lecture Notes in Computer Science , pages 48--62. Springer, 2016

work page 2016
[56]

Optimizing SAT encodings for arithmetic constraints

Neng - Fa Zhou and H kan Kjellerstrand. Optimizing SAT encodings for arithmetic constraints. In CP , volume 10416 of Lecture Notes in Computer Science , pages 671--686. Springer, 2017

work page 2017
[57]

Constraint Solving and Planning with Picat

Neng - Fa Zhou, H kan Kjellerstrand, and Jonathan Fruhman. Constraint Solving and Planning with Picat . Springer Briefs in Intelligent Systems. Springer, 2015

work page 2015